Proof of Theorem fnres
| Step | Hyp | Ref
| Expression |
| 1 | | ancom 266 |
. . 3
⊢
((∀𝑥 ∈
𝐴 ∃*𝑦 𝑥𝐹𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑥𝐹𝑦)) |
| 2 | | vex 2766 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
| 3 | 2 | brres 4952 |
. . . . . . . . 9
⊢ (𝑥(𝐹 ↾ 𝐴)𝑦 ↔ (𝑥𝐹𝑦 ∧ 𝑥 ∈ 𝐴)) |
| 4 | | ancom 266 |
. . . . . . . . 9
⊢ ((𝑥𝐹𝑦 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)) |
| 5 | 3, 4 | bitri 184 |
. . . . . . . 8
⊢ (𝑥(𝐹 ↾ 𝐴)𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)) |
| 6 | 5 | mobii 2082 |
. . . . . . 7
⊢
(∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦 ↔ ∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)) |
| 7 | | moanimv 2120 |
. . . . . . 7
⊢
(∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ↔ (𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
| 8 | 6, 7 | bitri 184 |
. . . . . 6
⊢
(∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦 ↔ (𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
| 9 | 8 | albii 1484 |
. . . . 5
⊢
(∀𝑥∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
| 10 | | relres 4974 |
. . . . . 6
⊢ Rel
(𝐹 ↾ 𝐴) |
| 11 | | dffun6 5272 |
. . . . . 6
⊢ (Fun
(𝐹 ↾ 𝐴) ↔ (Rel (𝐹 ↾ 𝐴) ∧ ∀𝑥∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦)) |
| 12 | 10, 11 | mpbiran 942 |
. . . . 5
⊢ (Fun
(𝐹 ↾ 𝐴) ↔ ∀𝑥∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦) |
| 13 | | df-ral 2480 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃*𝑦 𝑥𝐹𝑦 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
| 14 | 9, 12, 13 | 3bitr4i 212 |
. . . 4
⊢ (Fun
(𝐹 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑥𝐹𝑦) |
| 15 | | dmres 4967 |
. . . . . . 7
⊢ dom
(𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹) |
| 16 | | inss1 3383 |
. . . . . . 7
⊢ (𝐴 ∩ dom 𝐹) ⊆ 𝐴 |
| 17 | 15, 16 | eqsstri 3215 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝐴) ⊆ 𝐴 |
| 18 | | eqss 3198 |
. . . . . 6
⊢ (dom
(𝐹 ↾ 𝐴) = 𝐴 ↔ (dom (𝐹 ↾ 𝐴) ⊆ 𝐴 ∧ 𝐴 ⊆ dom (𝐹 ↾ 𝐴))) |
| 19 | 17, 18 | mpbiran 942 |
. . . . 5
⊢ (dom
(𝐹 ↾ 𝐴) = 𝐴 ↔ 𝐴 ⊆ dom (𝐹 ↾ 𝐴)) |
| 20 | | dfss3 3173 |
. . . . . 6
⊢ (𝐴 ⊆ dom (𝐹 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ dom (𝐹 ↾ 𝐴)) |
| 21 | 15 | elin2 3351 |
. . . . . . . . 9
⊢ (𝑥 ∈ dom (𝐹 ↾ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ dom 𝐹)) |
| 22 | 21 | baib 920 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ dom (𝐹 ↾ 𝐴) ↔ 𝑥 ∈ dom 𝐹)) |
| 23 | | vex 2766 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
| 24 | 23 | eldm 4863 |
. . . . . . . 8
⊢ (𝑥 ∈ dom 𝐹 ↔ ∃𝑦 𝑥𝐹𝑦) |
| 25 | 22, 24 | bitrdi 196 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ dom (𝐹 ↾ 𝐴) ↔ ∃𝑦 𝑥𝐹𝑦)) |
| 26 | 25 | ralbiia 2511 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝑥 ∈ dom (𝐹 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦) |
| 27 | 20, 26 | bitri 184 |
. . . . 5
⊢ (𝐴 ⊆ dom (𝐹 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦) |
| 28 | 19, 27 | bitri 184 |
. . . 4
⊢ (dom
(𝐹 ↾ 𝐴) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦) |
| 29 | 14, 28 | anbi12i 460 |
. . 3
⊢ ((Fun
(𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴) ↔ (∀𝑥 ∈ 𝐴 ∃*𝑦 𝑥𝐹𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦)) |
| 30 | | r19.26 2623 |
. . 3
⊢
(∀𝑥 ∈
𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑥𝐹𝑦)) |
| 31 | 1, 29, 30 | 3bitr4i 212 |
. 2
⊢ ((Fun
(𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴) ↔ ∀𝑥 ∈ 𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦)) |
| 32 | | df-fn 5261 |
. 2
⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ (Fun (𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴)) |
| 33 | | eu5 2092 |
. . 3
⊢
(∃!𝑦 𝑥𝐹𝑦 ↔ (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦)) |
| 34 | 33 | ralbii 2503 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦 𝑥𝐹𝑦 ↔ ∀𝑥 ∈ 𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦)) |
| 35 | 31, 32, 34 | 3bitr4i 212 |
1
⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) |