Step | Hyp | Ref
| Expression |
1 | | pw2f1o2.f |
. 2
⊢ 𝐹 = (𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) |
2 | | vex 3499 |
. . . 4
⊢ 𝑥 ∈ V |
3 | 2 | cnvex 7632 |
. . 3
⊢ ◡𝑥 ∈ V |
4 | | imaexg 7622 |
. . 3
⊢ (◡𝑥 ∈ V → (◡𝑥 “ {1o}) ∈
V) |
5 | 3, 4 | mp1i 13 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (2o ↑m
𝐴)) → (◡𝑥 “ {1o}) ∈
V) |
6 | | mptexg 6986 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) ∈
V) |
7 | 6 | adantr 483 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝐴) → (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) ∈
V) |
8 | | 2on 8113 |
. . . . . 6
⊢
2o ∈ On |
9 | | elmapg 8421 |
. . . . . 6
⊢
((2o ∈ On ∧ 𝐴 ∈ 𝑉) → (𝑥 ∈ (2o ↑m
𝐴) ↔ 𝑥:𝐴⟶2o)) |
10 | 8, 9 | mpan 688 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (2o ↑m
𝐴) ↔ 𝑥:𝐴⟶2o)) |
11 | 10 | anbi1d 631 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (2o ↑m
𝐴) ∧ 𝑦 = (◡𝑥 “ {1o})) ↔ (𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})))) |
12 | | 1oex 8112 |
. . . . . . . . . . . 12
⊢
1o ∈ V |
13 | 12 | sucid 6272 |
. . . . . . . . . . 11
⊢
1o ∈ suc 1o |
14 | | df-2o 8105 |
. . . . . . . . . . 11
⊢
2o = suc 1o |
15 | 13, 14 | eleqtrri 2914 |
. . . . . . . . . 10
⊢
1o ∈ 2o |
16 | | 0ex 5213 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
17 | 16 | prid1 4700 |
. . . . . . . . . . 11
⊢ ∅
∈ {∅, {∅}} |
18 | | df2o2 8120 |
. . . . . . . . . . 11
⊢
2o = {∅, {∅}} |
19 | 17, 18 | eleqtrri 2914 |
. . . . . . . . . 10
⊢ ∅
∈ 2o |
20 | 15, 19 | ifcli 4515 |
. . . . . . . . 9
⊢ if(𝑧 ∈ 𝑦, 1o, ∅) ∈
2o |
21 | 20 | rgenw 3152 |
. . . . . . . 8
⊢
∀𝑧 ∈
𝐴 if(𝑧 ∈ 𝑦, 1o, ∅) ∈
2o |
22 | | eqid 2823 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) |
23 | 22 | fmpt 6876 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝐴 if(𝑧 ∈ 𝑦, 1o, ∅) ∈
2o ↔ (𝑧
∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)):𝐴⟶2o) |
24 | 21, 23 | mpbi 232 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)):𝐴⟶2o |
25 | | simpr 487 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) |
26 | 25 | feq1d 6501 |
. . . . . . 7
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → (𝑥:𝐴⟶2o ↔ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)):𝐴⟶2o)) |
27 | 24, 26 | mpbiri 260 |
. . . . . 6
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → 𝑥:𝐴⟶2o) |
28 | 25 | fveq1d 6674 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → (𝑥‘𝑤) = ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))‘𝑤)) |
29 | | elequ1 2121 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → (𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦)) |
30 | 29 | ifbid 4491 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑤 → if(𝑧 ∈ 𝑦, 1o, ∅) = if(𝑤 ∈ 𝑦, 1o, ∅)) |
31 | 12, 16 | ifcli 4515 |
. . . . . . . . . . . . . 14
⊢ if(𝑤 ∈ 𝑦, 1o, ∅) ∈
V |
32 | 30, 22, 31 | fvmpt 6770 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ 𝐴 → ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))‘𝑤) = if(𝑤 ∈ 𝑦, 1o, ∅)) |
33 | 28, 32 | sylan9eq 2878 |
. . . . . . . . . . . 12
⊢ (((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) ∧ 𝑤 ∈ 𝐴) → (𝑥‘𝑤) = if(𝑤 ∈ 𝑦, 1o, ∅)) |
34 | 33 | eqeq1d 2825 |
. . . . . . . . . . 11
⊢ (((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) ∧ 𝑤 ∈ 𝐴) → ((𝑥‘𝑤) = 1o ↔ if(𝑤 ∈ 𝑦, 1o, ∅) =
1o)) |
35 | | iftrue 4475 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑦 → if(𝑤 ∈ 𝑦, 1o, ∅) =
1o) |
36 | | noel 4298 |
. . . . . . . . . . . . . 14
⊢ ¬
∅ ∈ ∅ |
37 | | iffalse 4478 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑤 ∈ 𝑦 → if(𝑤 ∈ 𝑦, 1o, ∅) =
∅) |
38 | 37 | eqeq1d 2825 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑤 ∈ 𝑦 → (if(𝑤 ∈ 𝑦, 1o, ∅) = 1o
↔ ∅ = 1o)) |
39 | | 0lt1o 8131 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ 1o |
40 | | eleq2 2903 |
. . . . . . . . . . . . . . . 16
⊢ (∅
= 1o → (∅ ∈ ∅ ↔ ∅ ∈
1o)) |
41 | 39, 40 | mpbiri 260 |
. . . . . . . . . . . . . . 15
⊢ (∅
= 1o → ∅ ∈ ∅) |
42 | 38, 41 | syl6bi 255 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑤 ∈ 𝑦 → (if(𝑤 ∈ 𝑦, 1o, ∅) = 1o
→ ∅ ∈ ∅)) |
43 | 36, 42 | mtoi 201 |
. . . . . . . . . . . . 13
⊢ (¬
𝑤 ∈ 𝑦 → ¬ if(𝑤 ∈ 𝑦, 1o, ∅) =
1o) |
44 | 43 | con4i 114 |
. . . . . . . . . . . 12
⊢ (if(𝑤 ∈ 𝑦, 1o, ∅) = 1o
→ 𝑤 ∈ 𝑦) |
45 | 35, 44 | impbii 211 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝑦 ↔ if(𝑤 ∈ 𝑦, 1o, ∅) =
1o) |
46 | 34, 45 | syl6rbbr 292 |
. . . . . . . . . 10
⊢ (((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) ∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ 𝑦 ↔ (𝑥‘𝑤) = 1o)) |
47 | | fvex 6685 |
. . . . . . . . . . 11
⊢ (𝑥‘𝑤) ∈ V |
48 | 47 | elsn 4584 |
. . . . . . . . . 10
⊢ ((𝑥‘𝑤) ∈ {1o} ↔ (𝑥‘𝑤) = 1o) |
49 | 46, 48 | syl6bbr 291 |
. . . . . . . . 9
⊢ (((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) ∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ 𝑦 ↔ (𝑥‘𝑤) ∈ {1o})) |
50 | 49 | pm5.32da 581 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → ((𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝑦) ↔ (𝑤 ∈ 𝐴 ∧ (𝑥‘𝑤) ∈ {1o}))) |
51 | | ssel 3963 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ 𝐴 → (𝑤 ∈ 𝑦 → 𝑤 ∈ 𝐴)) |
52 | 51 | adantr 483 |
. . . . . . . . 9
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → (𝑤 ∈ 𝑦 → 𝑤 ∈ 𝐴)) |
53 | 52 | pm4.71rd 565 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → (𝑤 ∈ 𝑦 ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝑦))) |
54 | | ffn 6516 |
. . . . . . . . 9
⊢ (𝑥:𝐴⟶2o → 𝑥 Fn 𝐴) |
55 | | elpreima 6830 |
. . . . . . . . 9
⊢ (𝑥 Fn 𝐴 → (𝑤 ∈ (◡𝑥 “ {1o}) ↔ (𝑤 ∈ 𝐴 ∧ (𝑥‘𝑤) ∈ {1o}))) |
56 | 27, 54, 55 | 3syl 18 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → (𝑤 ∈ (◡𝑥 “ {1o}) ↔ (𝑤 ∈ 𝐴 ∧ (𝑥‘𝑤) ∈ {1o}))) |
57 | 50, 53, 56 | 3bitr4d 313 |
. . . . . . 7
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → (𝑤 ∈ 𝑦 ↔ 𝑤 ∈ (◡𝑥 “ {1o}))) |
58 | 57 | eqrdv 2821 |
. . . . . 6
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → 𝑦 = (◡𝑥 “ {1o})) |
59 | 27, 58 | jca 514 |
. . . . 5
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → (𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o}))) |
60 | | simpr 487 |
. . . . . . 7
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) → 𝑦 = (◡𝑥 “ {1o})) |
61 | | cnvimass 5951 |
. . . . . . . 8
⊢ (◡𝑥 “ {1o}) ⊆ dom 𝑥 |
62 | | fdm 6524 |
. . . . . . . . 9
⊢ (𝑥:𝐴⟶2o → dom 𝑥 = 𝐴) |
63 | 62 | adantr 483 |
. . . . . . . 8
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) → dom 𝑥 = 𝐴) |
64 | 61, 63 | sseqtrid 4021 |
. . . . . . 7
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) → (◡𝑥 “ {1o}) ⊆ 𝐴) |
65 | 60, 64 | eqsstrd 4007 |
. . . . . 6
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) → 𝑦 ⊆ 𝐴) |
66 | | simplr 767 |
. . . . . . . . . . . . . 14
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → 𝑦 = (◡𝑥 “ {1o})) |
67 | 66 | eleq2d 2900 |
. . . . . . . . . . . . 13
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ 𝑦 ↔ 𝑤 ∈ (◡𝑥 “ {1o}))) |
68 | 54 | adantr 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) → 𝑥 Fn 𝐴) |
69 | | fnbrfvb 6720 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 Fn 𝐴 ∧ 𝑤 ∈ 𝐴) → ((𝑥‘𝑤) = 1o ↔ 𝑤𝑥1o)) |
70 | 68, 69 | sylan 582 |
. . . . . . . . . . . . . 14
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → ((𝑥‘𝑤) = 1o ↔ 𝑤𝑥1o)) |
71 | | 1on 8111 |
. . . . . . . . . . . . . . 15
⊢
1o ∈ On |
72 | | vex 3499 |
. . . . . . . . . . . . . . . 16
⊢ 𝑤 ∈ V |
73 | 72 | eliniseg 5960 |
. . . . . . . . . . . . . . 15
⊢
(1o ∈ On → (𝑤 ∈ (◡𝑥 “ {1o}) ↔ 𝑤𝑥1o)) |
74 | 71, 73 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (◡𝑥 “ {1o}) ↔ 𝑤𝑥1o) |
75 | 70, 74 | syl6bbr 291 |
. . . . . . . . . . . . 13
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → ((𝑥‘𝑤) = 1o ↔ 𝑤 ∈ (◡𝑥 “ {1o}))) |
76 | 67, 75 | bitr4d 284 |
. . . . . . . . . . . 12
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ 𝑦 ↔ (𝑥‘𝑤) = 1o)) |
77 | 76 | biimpa 479 |
. . . . . . . . . . 11
⊢ ((((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝑥‘𝑤) = 1o) |
78 | 35 | adantl 484 |
. . . . . . . . . . 11
⊢ ((((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) ∧ 𝑤 ∈ 𝑦) → if(𝑤 ∈ 𝑦, 1o, ∅) =
1o) |
79 | 77, 78 | eqtr4d 2861 |
. . . . . . . . . 10
⊢ ((((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝑥‘𝑤) = if(𝑤 ∈ 𝑦, 1o, ∅)) |
80 | | ffvelrn 6851 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥:𝐴⟶2o ∧ 𝑤 ∈ 𝐴) → (𝑥‘𝑤) ∈ 2o) |
81 | 80 | adantlr 713 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (𝑥‘𝑤) ∈ 2o) |
82 | | df2o3 8119 |
. . . . . . . . . . . . . . . . 17
⊢
2o = {∅, 1o} |
83 | 81, 82 | eleqtrdi 2925 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (𝑥‘𝑤) ∈ {∅,
1o}) |
84 | 47 | elpr 4592 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥‘𝑤) ∈ {∅, 1o} ↔
((𝑥‘𝑤) = ∅ ∨ (𝑥‘𝑤) = 1o)) |
85 | 83, 84 | sylib 220 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → ((𝑥‘𝑤) = ∅ ∨ (𝑥‘𝑤) = 1o)) |
86 | 85 | ord 860 |
. . . . . . . . . . . . . 14
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (¬ (𝑥‘𝑤) = ∅ → (𝑥‘𝑤) = 1o)) |
87 | 86, 76 | sylibrd 261 |
. . . . . . . . . . . . 13
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (¬ (𝑥‘𝑤) = ∅ → 𝑤 ∈ 𝑦)) |
88 | 87 | con1d 147 |
. . . . . . . . . . . 12
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (¬ 𝑤 ∈ 𝑦 → (𝑥‘𝑤) = ∅)) |
89 | 88 | imp 409 |
. . . . . . . . . . 11
⊢ ((((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 ∈ 𝑦) → (𝑥‘𝑤) = ∅) |
90 | 37 | adantl 484 |
. . . . . . . . . . 11
⊢ ((((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 ∈ 𝑦) → if(𝑤 ∈ 𝑦, 1o, ∅) =
∅) |
91 | 89, 90 | eqtr4d 2861 |
. . . . . . . . . 10
⊢ ((((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 ∈ 𝑦) → (𝑥‘𝑤) = if(𝑤 ∈ 𝑦, 1o, ∅)) |
92 | 79, 91 | pm2.61dan 811 |
. . . . . . . . 9
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (𝑥‘𝑤) = if(𝑤 ∈ 𝑦, 1o, ∅)) |
93 | 32 | adantl 484 |
. . . . . . . . 9
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))‘𝑤) = if(𝑤 ∈ 𝑦, 1o, ∅)) |
94 | 92, 93 | eqtr4d 2861 |
. . . . . . . 8
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (𝑥‘𝑤) = ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))‘𝑤)) |
95 | 94 | ralrimiva 3184 |
. . . . . . 7
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) →
∀𝑤 ∈ 𝐴 (𝑥‘𝑤) = ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))‘𝑤)) |
96 | | ffn 6516 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)):𝐴⟶2o → (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) Fn 𝐴) |
97 | 24, 96 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) Fn 𝐴 |
98 | | eqfnfv 6804 |
. . . . . . . 8
⊢ ((𝑥 Fn 𝐴 ∧ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) Fn 𝐴) → (𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) ↔
∀𝑤 ∈ 𝐴 (𝑥‘𝑤) = ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))‘𝑤))) |
99 | 68, 97, 98 | sylancl 588 |
. . . . . . 7
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) → (𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) ↔
∀𝑤 ∈ 𝐴 (𝑥‘𝑤) = ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))‘𝑤))) |
100 | 95, 99 | mpbird 259 |
. . . . . 6
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) → 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) |
101 | 65, 100 | jca 514 |
. . . . 5
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) → (𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)))) |
102 | 59, 101 | impbii 211 |
. . . 4
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) ↔ (𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o}))) |
103 | 11, 102 | syl6bbr 291 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (2o ↑m
𝐴) ∧ 𝑦 = (◡𝑥 “ {1o})) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o,
∅))))) |
104 | | velpw 4546 |
. . . 4
⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴) |
105 | 104 | anbi1i 625 |
. . 3
⊢ ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)))) |
106 | 103, 105 | syl6bbr 291 |
. 2
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (2o ↑m
𝐴) ∧ 𝑦 = (◡𝑥 “ {1o})) ↔ (𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o,
∅))))) |
107 | 1, 5, 7, 106 | f1ocnvd 7398 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐹:(2o ↑m 𝐴)–1-1-onto→𝒫 𝐴 ∧ ◡𝐹 = (𝑦 ∈ 𝒫 𝐴 ↦ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o,
∅))))) |