Proof of Theorem fnres
| Step | Hyp | Ref
| Expression |
| 1 | | ancom 460 |
. . 3
⊢
((∀𝑥 ∈
𝐴 ∃*𝑦 𝑥𝐹𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑥𝐹𝑦)) |
| 2 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
| 3 | 2 | brresi 6006 |
. . . . . . . 8
⊢ (𝑥(𝐹 ↾ 𝐴)𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)) |
| 4 | 3 | mobii 2548 |
. . . . . . 7
⊢
(∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦 ↔ ∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)) |
| 5 | | moanimv 2619 |
. . . . . . 7
⊢
(∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ↔ (𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
| 6 | 4, 5 | bitri 275 |
. . . . . 6
⊢
(∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦 ↔ (𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
| 7 | 6 | albii 1819 |
. . . . 5
⊢
(∀𝑥∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
| 8 | | relres 6023 |
. . . . . 6
⊢ Rel
(𝐹 ↾ 𝐴) |
| 9 | | dffun6 6574 |
. . . . . 6
⊢ (Fun
(𝐹 ↾ 𝐴) ↔ (Rel (𝐹 ↾ 𝐴) ∧ ∀𝑥∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦)) |
| 10 | 8, 9 | mpbiran 709 |
. . . . 5
⊢ (Fun
(𝐹 ↾ 𝐴) ↔ ∀𝑥∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦) |
| 11 | | df-ral 3062 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃*𝑦 𝑥𝐹𝑦 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
| 12 | 7, 10, 11 | 3bitr4i 303 |
. . . 4
⊢ (Fun
(𝐹 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑥𝐹𝑦) |
| 13 | | dmres 6030 |
. . . . . . 7
⊢ dom
(𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹) |
| 14 | | inss1 4237 |
. . . . . . 7
⊢ (𝐴 ∩ dom 𝐹) ⊆ 𝐴 |
| 15 | 13, 14 | eqsstri 4030 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝐴) ⊆ 𝐴 |
| 16 | | eqss 3999 |
. . . . . 6
⊢ (dom
(𝐹 ↾ 𝐴) = 𝐴 ↔ (dom (𝐹 ↾ 𝐴) ⊆ 𝐴 ∧ 𝐴 ⊆ dom (𝐹 ↾ 𝐴))) |
| 17 | 15, 16 | mpbiran 709 |
. . . . 5
⊢ (dom
(𝐹 ↾ 𝐴) = 𝐴 ↔ 𝐴 ⊆ dom (𝐹 ↾ 𝐴)) |
| 18 | | dfss3 3972 |
. . . . . 6
⊢ (𝐴 ⊆ dom (𝐹 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ dom (𝐹 ↾ 𝐴)) |
| 19 | 13 | elin2 4203 |
. . . . . . . . 9
⊢ (𝑥 ∈ dom (𝐹 ↾ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ dom 𝐹)) |
| 20 | 19 | baib 535 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ dom (𝐹 ↾ 𝐴) ↔ 𝑥 ∈ dom 𝐹)) |
| 21 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
| 22 | 21 | eldm 5911 |
. . . . . . . 8
⊢ (𝑥 ∈ dom 𝐹 ↔ ∃𝑦 𝑥𝐹𝑦) |
| 23 | 20, 22 | bitrdi 287 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ dom (𝐹 ↾ 𝐴) ↔ ∃𝑦 𝑥𝐹𝑦)) |
| 24 | 23 | ralbiia 3091 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝑥 ∈ dom (𝐹 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦) |
| 25 | 18, 24 | bitri 275 |
. . . . 5
⊢ (𝐴 ⊆ dom (𝐹 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦) |
| 26 | 17, 25 | bitri 275 |
. . . 4
⊢ (dom
(𝐹 ↾ 𝐴) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦) |
| 27 | 12, 26 | anbi12i 628 |
. . 3
⊢ ((Fun
(𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴) ↔ (∀𝑥 ∈ 𝐴 ∃*𝑦 𝑥𝐹𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦)) |
| 28 | | r19.26 3111 |
. . 3
⊢
(∀𝑥 ∈
𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑥𝐹𝑦)) |
| 29 | 1, 27, 28 | 3bitr4i 303 |
. 2
⊢ ((Fun
(𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴) ↔ ∀𝑥 ∈ 𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦)) |
| 30 | | df-fn 6564 |
. 2
⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ (Fun (𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴)) |
| 31 | | df-eu 2569 |
. . 3
⊢
(∃!𝑦 𝑥𝐹𝑦 ↔ (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦)) |
| 32 | 31 | ralbii 3093 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦 𝑥𝐹𝑦 ↔ ∀𝑥 ∈ 𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦)) |
| 33 | 29, 30, 32 | 3bitr4i 303 |
1
⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) |