Proof of Theorem fnres
Step | Hyp | Ref
| Expression |
1 | | ancom 253 |
. . 3
⊢ ((∀x ∈ A ∃*y x𝐹y ∧ ∀x ∈ A ∃y x𝐹y) ↔ (∀x ∈ A ∃y x𝐹y ∧ ∀x ∈ A ∃*y x𝐹y)) |
2 | | vex 2554 |
. . . . . . . . . 10
⊢ y ∈
V |
3 | 2 | brres 4561 |
. . . . . . . . 9
⊢ (x(𝐹 ↾ A)y ↔
(x𝐹y ∧ x ∈ A)) |
4 | | ancom 253 |
. . . . . . . . 9
⊢
((x𝐹y ∧ x ∈ A) ↔
(x ∈
A ∧
x𝐹y)) |
5 | 3, 4 | bitri 173 |
. . . . . . . 8
⊢ (x(𝐹 ↾ A)y ↔
(x ∈
A ∧
x𝐹y)) |
6 | 5 | mobii 1934 |
. . . . . . 7
⊢ (∃*y x(𝐹 ↾ A)y ↔ ∃*y(x ∈ A ∧ x𝐹y)) |
7 | | moanimv 1972 |
. . . . . . 7
⊢ (∃*y(x ∈ A ∧ x𝐹y)
↔ (x ∈ A →
∃*y
x𝐹y)) |
8 | 6, 7 | bitri 173 |
. . . . . 6
⊢ (∃*y x(𝐹 ↾ A)y ↔
(x ∈
A → ∃*y x𝐹y)) |
9 | 8 | albii 1356 |
. . . . 5
⊢ (∀x∃*y x(𝐹 ↾ A)y ↔ ∀x(x ∈ A → ∃*y x𝐹y)) |
10 | | relres 4582 |
. . . . . 6
⊢ Rel
(𝐹 ↾ A) |
11 | | dffun6 4859 |
. . . . . 6
⊢ (Fun
(𝐹 ↾ A) ↔ (Rel (𝐹 ↾ A) ∧ ∀x∃*y x(𝐹 ↾ A)y)) |
12 | 10, 11 | mpbiran 846 |
. . . . 5
⊢ (Fun
(𝐹 ↾ A) ↔ ∀x∃*y x(𝐹 ↾ A)y) |
13 | | df-ral 2305 |
. . . . 5
⊢ (∀x ∈ A ∃*y x𝐹y ↔
∀x(x ∈ A →
∃*y
x𝐹y)) |
14 | 9, 12, 13 | 3bitr4i 201 |
. . . 4
⊢ (Fun
(𝐹 ↾ A) ↔ ∀x ∈ A ∃*y x𝐹y) |
15 | | dmres 4575 |
. . . . . . 7
⊢ dom
(𝐹 ↾ A) = (A ∩
dom 𝐹) |
16 | | inss1 3151 |
. . . . . . 7
⊢ (A ∩ dom 𝐹) ⊆ A |
17 | 15, 16 | eqsstri 2969 |
. . . . . 6
⊢ dom
(𝐹 ↾ A) ⊆ A |
18 | | eqss 2954 |
. . . . . 6
⊢ (dom
(𝐹 ↾ A) = A ↔
(dom (𝐹 ↾ A) ⊆ A
∧ A
⊆ dom (𝐹 ↾
A))) |
19 | 17, 18 | mpbiran 846 |
. . . . 5
⊢ (dom
(𝐹 ↾ A) = A ↔
A ⊆ dom (𝐹 ↾ A)) |
20 | | dfss3 2929 |
. . . . . 6
⊢ (A ⊆ dom (𝐹 ↾ A) ↔ ∀x ∈ A x ∈ dom (𝐹 ↾ A)) |
21 | 15 | elin2 3121 |
. . . . . . . . 9
⊢ (x ∈ dom (𝐹 ↾ A) ↔ (x
∈ A ∧ x ∈ dom 𝐹)) |
22 | 21 | baib 827 |
. . . . . . . 8
⊢ (x ∈ A → (x
∈ dom (𝐹 ↾ A) ↔ x
∈ dom 𝐹)) |
23 | | vex 2554 |
. . . . . . . . 9
⊢ x ∈
V |
24 | 23 | eldm 4475 |
. . . . . . . 8
⊢ (x ∈ dom 𝐹 ↔ ∃y x𝐹y) |
25 | 22, 24 | syl6bb 185 |
. . . . . . 7
⊢ (x ∈ A → (x
∈ dom (𝐹 ↾ A) ↔ ∃y x𝐹y)) |
26 | 25 | ralbiia 2332 |
. . . . . 6
⊢ (∀x ∈ A x ∈ dom (𝐹 ↾ A) ↔ ∀x ∈ A ∃y x𝐹y) |
27 | 20, 26 | bitri 173 |
. . . . 5
⊢ (A ⊆ dom (𝐹 ↾ A) ↔ ∀x ∈ A ∃y x𝐹y) |
28 | 19, 27 | bitri 173 |
. . . 4
⊢ (dom
(𝐹 ↾ A) = A ↔
∀x
∈ A ∃y x𝐹y) |
29 | 14, 28 | anbi12i 433 |
. . 3
⊢ ((Fun
(𝐹 ↾ A) ∧ dom (𝐹 ↾ A) = A) ↔
(∀x
∈ A ∃*y x𝐹y ∧ ∀x ∈ A ∃y x𝐹y)) |
30 | | r19.26 2435 |
. . 3
⊢ (∀x ∈ A (∃y x𝐹y ∧ ∃*y x𝐹y) ↔ (∀x ∈ A ∃y x𝐹y ∧ ∀x ∈ A ∃*y x𝐹y)) |
31 | 1, 29, 30 | 3bitr4i 201 |
. 2
⊢ ((Fun
(𝐹 ↾ A) ∧ dom (𝐹 ↾ A) = A) ↔
∀x
∈ A
(∃y
x𝐹y ∧ ∃*y x𝐹y)) |
32 | | df-fn 4848 |
. 2
⊢ ((𝐹 ↾ A) Fn A ↔
(Fun (𝐹 ↾ A) ∧ dom (𝐹 ↾ A) = A)) |
33 | | eu5 1944 |
. . 3
⊢ (∃!y x𝐹y ↔
(∃y
x𝐹y ∧ ∃*y x𝐹y)) |
34 | 33 | ralbii 2324 |
. 2
⊢ (∀x ∈ A ∃!y x𝐹y ↔
∀x
∈ A
(∃y
x𝐹y ∧ ∃*y x𝐹y)) |
35 | 31, 32, 34 | 3bitr4i 201 |
1
⊢ ((𝐹 ↾ A) Fn A ↔
∀x
∈ A ∃!y x𝐹y) |