Step | Hyp | Ref
| Expression |
1 | | ancom 462 |
. . 3
⊢
((∀𝑥 ∈
𝐴 ∃*𝑦 𝑥𝐹𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑥𝐹𝑦)) |
2 | | vex 3441 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
3 | 2 | brresi 5908 |
. . . . . . . 8
⊢ (𝑥(𝐹 ↾ 𝐴)𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)) |
4 | 3 | mobii 2546 |
. . . . . . 7
⊢
(∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦 ↔ ∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)) |
5 | | moanimv 2619 |
. . . . . . 7
⊢
(∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ↔ (𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
6 | 4, 5 | bitri 276 |
. . . . . 6
⊢
(∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦 ↔ (𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
7 | 6 | albii 1819 |
. . . . 5
⊢
(∀𝑥∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
8 | | relres 5928 |
. . . . . 6
⊢ Rel
(𝐹 ↾ 𝐴) |
9 | | dffun6 6467 |
. . . . . 6
⊢ (Fun
(𝐹 ↾ 𝐴) ↔ (Rel (𝐹 ↾ 𝐴) ∧ ∀𝑥∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦)) |
10 | 8, 9 | mpbiran 707 |
. . . . 5
⊢ (Fun
(𝐹 ↾ 𝐴) ↔ ∀𝑥∃*𝑦 𝑥(𝐹 ↾ 𝐴)𝑦) |
11 | | df-ral 3063 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∃*𝑦 𝑥𝐹𝑦 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
12 | 7, 10, 11 | 3bitr4i 304 |
. . . 4
⊢ (Fun
(𝐹 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑥𝐹𝑦) |
13 | | dmres 5921 |
. . . . . . 7
⊢ dom
(𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹) |
14 | | inss1 4168 |
. . . . . . 7
⊢ (𝐴 ∩ dom 𝐹) ⊆ 𝐴 |
15 | 13, 14 | eqsstri 3960 |
. . . . . 6
⊢ dom
(𝐹 ↾ 𝐴) ⊆ 𝐴 |
16 | | eqss 3941 |
. . . . . 6
⊢ (dom
(𝐹 ↾ 𝐴) = 𝐴 ↔ (dom (𝐹 ↾ 𝐴) ⊆ 𝐴 ∧ 𝐴 ⊆ dom (𝐹 ↾ 𝐴))) |
17 | 15, 16 | mpbiran 707 |
. . . . 5
⊢ (dom
(𝐹 ↾ 𝐴) = 𝐴 ↔ 𝐴 ⊆ dom (𝐹 ↾ 𝐴)) |
18 | | dfss3 3914 |
. . . . . 6
⊢ (𝐴 ⊆ dom (𝐹 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ dom (𝐹 ↾ 𝐴)) |
19 | 13 | elin2 4137 |
. . . . . . . . 9
⊢ (𝑥 ∈ dom (𝐹 ↾ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ dom 𝐹)) |
20 | 19 | baib 537 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ dom (𝐹 ↾ 𝐴) ↔ 𝑥 ∈ dom 𝐹)) |
21 | | vex 3441 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
22 | 21 | eldm 5818 |
. . . . . . . 8
⊢ (𝑥 ∈ dom 𝐹 ↔ ∃𝑦 𝑥𝐹𝑦) |
23 | 20, 22 | bitrdi 288 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ dom (𝐹 ↾ 𝐴) ↔ ∃𝑦 𝑥𝐹𝑦)) |
24 | 23 | ralbiia 3091 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝑥 ∈ dom (𝐹 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦) |
25 | 18, 24 | bitri 276 |
. . . . 5
⊢ (𝐴 ⊆ dom (𝐹 ↾ 𝐴) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦) |
26 | 17, 25 | bitri 276 |
. . . 4
⊢ (dom
(𝐹 ↾ 𝐴) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦) |
27 | 12, 26 | anbi12i 628 |
. . 3
⊢ ((Fun
(𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴) ↔ (∀𝑥 ∈ 𝐴 ∃*𝑦 𝑥𝐹𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦)) |
28 | | r19.26 3111 |
. . 3
⊢
(∀𝑥 ∈
𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 𝑥𝐹𝑦 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑥𝐹𝑦)) |
29 | 1, 27, 28 | 3bitr4i 304 |
. 2
⊢ ((Fun
(𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴) ↔ ∀𝑥 ∈ 𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦)) |
30 | | df-fn 6457 |
. 2
⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ (Fun (𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴)) |
31 | | df-eu 2567 |
. . 3
⊢
(∃!𝑦 𝑥𝐹𝑦 ↔ (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦)) |
32 | 31 | ralbii 3093 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦 𝑥𝐹𝑦 ↔ ∀𝑥 ∈ 𝐴 (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦)) |
33 | 29, 30, 32 | 3bitr4i 304 |
1
⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) |