Proof of Theorem fnres
Step | Hyp | Ref
| Expression |
1 | | ancom 452 |
. . 3
⊢
((∀𝑥 ∈
𝐴 ∃*𝑦 𝑥𝐹𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑥𝐹𝑦)) |
2 | | vex 3352 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
3 | 2 | brres 5543 |
. . . . . . . . 9
⊢ (𝑥(𝐹 ↾ 𝐴)𝑦 ↔ (𝑥𝐹𝑦 ∧ 𝑥 ∈ 𝐴)) |
4 | | ancom 452 |
. . . . . . . . 9
⊢ ((𝑥𝐹𝑦 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)) |
5 | 3, 4 | bitri 264 |
. . . . . . . 8
⊢ (𝑥(𝐹 ↾ 𝐴)𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)) |
6 | 5 | mobii 2640 |
. . . . . . 7
⊢
(∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦 ↔ ∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)) |
7 | | moanimv 2679 |
. . . . . . 7
⊢
(∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ↔ (𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
8 | 6, 7 | bitri 264 |
. . . . . 6
⊢
(∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦 ↔ (𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
9 | 8 | albii 1894 |
. . . . 5
⊢
(∀𝑥∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
10 | | relres 5567 |
. . . . . 6
⊢ Rel
(𝐹 ↾ 𝐴) |
11 | | dffun6 6046 |
. . . . . 6
⊢ (Fun
(𝐹 ↾ 𝐴) ↔ (Rel (𝐹 ↾ 𝐴) ∧ ∀𝑥∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦)) |
12 | 10, 11 | mpbiran 680 |
. . . . 5
⊢ (Fun
(𝐹 ↾ 𝐴) ↔ ∀𝑥∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦) |
13 | | df-ral 3065 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃*𝑦 𝑥𝐹𝑦 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
14 | 9, 12, 13 | 3bitr4i 292 |
. . . 4
⊢ (Fun
(𝐹 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑥𝐹𝑦) |
15 | | dmres 5560 |
. . . . . . 7
⊢ dom
(𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹) |
16 | | inss1 3979 |
. . . . . . 7
⊢ (𝐴 ∩ dom 𝐹) ⊆ 𝐴 |
17 | 15, 16 | eqsstri 3782 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝐴) ⊆ 𝐴 |
18 | | eqss 3765 |
. . . . . 6
⊢ (dom
(𝐹 ↾ 𝐴) = 𝐴 ↔ (dom (𝐹 ↾ 𝐴) ⊆ 𝐴 ∧ 𝐴 ⊆ dom (𝐹 ↾ 𝐴))) |
19 | 17, 18 | mpbiran 680 |
. . . . 5
⊢ (dom
(𝐹 ↾ 𝐴) = 𝐴 ↔ 𝐴 ⊆ dom (𝐹 ↾ 𝐴)) |
20 | | dfss3 3739 |
. . . . . 6
⊢ (𝐴 ⊆ dom (𝐹 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ dom (𝐹 ↾ 𝐴)) |
21 | 15 | elin2 3950 |
. . . . . . . . 9
⊢ (𝑥 ∈ dom (𝐹 ↾ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ dom 𝐹)) |
22 | 21 | baib 517 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ dom (𝐹 ↾ 𝐴) ↔ 𝑥 ∈ dom 𝐹)) |
23 | | vex 3352 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
24 | 23 | eldm 5459 |
. . . . . . . 8
⊢ (𝑥 ∈ dom 𝐹 ↔ ∃𝑦 𝑥𝐹𝑦) |
25 | 22, 24 | syl6bb 276 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ dom (𝐹 ↾ 𝐴) ↔ ∃𝑦 𝑥𝐹𝑦)) |
26 | 25 | ralbiia 3127 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝑥 ∈ dom (𝐹 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦) |
27 | 20, 26 | bitri 264 |
. . . . 5
⊢ (𝐴 ⊆ dom (𝐹 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦) |
28 | 19, 27 | bitri 264 |
. . . 4
⊢ (dom
(𝐹 ↾ 𝐴) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦) |
29 | 14, 28 | anbi12i 604 |
. . 3
⊢ ((Fun
(𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴) ↔ (∀𝑥 ∈ 𝐴 ∃*𝑦 𝑥𝐹𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦)) |
30 | | r19.26 3211 |
. . 3
⊢
(∀𝑥 ∈
𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑥𝐹𝑦)) |
31 | 1, 29, 30 | 3bitr4i 292 |
. 2
⊢ ((Fun
(𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴) ↔ ∀𝑥 ∈ 𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦)) |
32 | | df-fn 6034 |
. 2
⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ (Fun (𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴)) |
33 | | eu5 2643 |
. . 3
⊢
(∃!𝑦 𝑥𝐹𝑦 ↔ (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦)) |
34 | 33 | ralbii 3128 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦 𝑥𝐹𝑦 ↔ ∀𝑥 ∈ 𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦)) |
35 | 31, 32, 34 | 3bitr4i 292 |
1
⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) |