Step | Hyp | Ref
| Expression |
1 | | pw2f1o2.f |
. 2
⊢ 𝐹 = (𝑥 ∈ (2𝑜
↑𝑚 𝐴) ↦ (◡𝑥 “
{1𝑜})) |
2 | | vex 3176 |
. . . 4
⊢ 𝑥 ∈ V |
3 | 2 | cnvex 7006 |
. . 3
⊢ ◡𝑥 ∈ V |
4 | | imaexg 6995 |
. . 3
⊢ (◡𝑥 ∈ V → (◡𝑥 “ {1𝑜}) ∈
V) |
5 | 3, 4 | mp1i 13 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (2𝑜
↑𝑚 𝐴)) → (◡𝑥 “ {1𝑜}) ∈
V) |
6 | | mptexg 6389 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅)) ∈
V) |
7 | 6 | adantr 480 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝐴) → (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅)) ∈
V) |
8 | | 2on 7455 |
. . . . . 6
⊢
2𝑜 ∈ On |
9 | | elmapg 7757 |
. . . . . 6
⊢
((2𝑜 ∈ On ∧ 𝐴 ∈ 𝑉) → (𝑥 ∈ (2𝑜
↑𝑚 𝐴) ↔ 𝑥:𝐴⟶2𝑜)) |
10 | 8, 9 | mpan 702 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (2𝑜
↑𝑚 𝐴) ↔ 𝑥:𝐴⟶2𝑜)) |
11 | 10 | anbi1d 737 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ↔
(𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “
{1𝑜})))) |
12 | | 1on 7454 |
. . . . . . . . . . . . 13
⊢
1𝑜 ∈ On |
13 | 12 | elexi 3186 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ V |
14 | 13 | sucid 5721 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ suc 1𝑜 |
15 | | df-2o 7448 |
. . . . . . . . . . 11
⊢
2𝑜 = suc 1𝑜 |
16 | 14, 15 | eleqtrri 2687 |
. . . . . . . . . 10
⊢
1𝑜 ∈ 2𝑜 |
17 | | 0ex 4718 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
18 | 17 | prid1 4241 |
. . . . . . . . . . 11
⊢ ∅
∈ {∅, {∅}} |
19 | | df2o2 7461 |
. . . . . . . . . . 11
⊢
2𝑜 = {∅, {∅}} |
20 | 18, 19 | eleqtrri 2687 |
. . . . . . . . . 10
⊢ ∅
∈ 2𝑜 |
21 | 16, 20 | keepel 4105 |
. . . . . . . . 9
⊢ if(𝑧 ∈ 𝑦, 1𝑜, ∅) ∈
2𝑜 |
22 | 21 | rgenw 2908 |
. . . . . . . 8
⊢
∀𝑧 ∈
𝐴 if(𝑧 ∈ 𝑦, 1𝑜, ∅) ∈
2𝑜 |
23 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅)) = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜,
∅)) |
24 | 23 | fmpt 6289 |
. . . . . . . 8
⊢
(∀𝑧 ∈
𝐴 if(𝑧 ∈ 𝑦, 1𝑜, ∅) ∈
2𝑜 ↔ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅)):𝐴⟶2𝑜) |
25 | 22, 24 | mpbi 219 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅)):𝐴⟶2𝑜 |
26 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))) →
𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜,
∅))) |
27 | 26 | feq1d 5943 |
. . . . . . 7
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))) →
(𝑥:𝐴⟶2𝑜 ↔ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅)):𝐴⟶2𝑜)) |
28 | 25, 27 | mpbiri 247 |
. . . . . 6
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))) →
𝑥:𝐴⟶2𝑜) |
29 | 26 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))) →
(𝑥‘𝑤) = ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜,
∅))‘𝑤)) |
30 | | elequ1 1984 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → (𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦)) |
31 | 30 | ifbid 4058 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑤 → if(𝑧 ∈ 𝑦, 1𝑜, ∅) = if(𝑤 ∈ 𝑦, 1𝑜,
∅)) |
32 | 13, 17 | keepel 4105 |
. . . . . . . . . . . . . 14
⊢ if(𝑤 ∈ 𝑦, 1𝑜, ∅) ∈
V |
33 | 31, 23, 32 | fvmpt 6191 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ 𝐴 → ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜,
∅))‘𝑤) =
if(𝑤 ∈ 𝑦, 1𝑜,
∅)) |
34 | 29, 33 | sylan9eq 2664 |
. . . . . . . . . . . 12
⊢ (((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))) ∧
𝑤 ∈ 𝐴) → (𝑥‘𝑤) = if(𝑤 ∈ 𝑦, 1𝑜,
∅)) |
35 | 34 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ (((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))) ∧
𝑤 ∈ 𝐴) → ((𝑥‘𝑤) = 1𝑜 ↔ if(𝑤 ∈ 𝑦, 1𝑜, ∅) =
1𝑜)) |
36 | | iftrue 4042 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑦 → if(𝑤 ∈ 𝑦, 1𝑜, ∅) =
1𝑜) |
37 | | noel 3878 |
. . . . . . . . . . . . . 14
⊢ ¬
∅ ∈ ∅ |
38 | | iffalse 4045 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑤 ∈ 𝑦 → if(𝑤 ∈ 𝑦, 1𝑜, ∅) =
∅) |
39 | 38 | eqeq1d 2612 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑤 ∈ 𝑦 → (if(𝑤 ∈ 𝑦, 1𝑜, ∅) =
1𝑜 ↔ ∅ = 1𝑜)) |
40 | | 0lt1o 7471 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ 1𝑜 |
41 | | eleq2 2677 |
. . . . . . . . . . . . . . . 16
⊢ (∅
= 1𝑜 → (∅ ∈ ∅ ↔ ∅ ∈
1𝑜)) |
42 | 40, 41 | mpbiri 247 |
. . . . . . . . . . . . . . 15
⊢ (∅
= 1𝑜 → ∅ ∈ ∅) |
43 | 39, 42 | syl6bi 242 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑤 ∈ 𝑦 → (if(𝑤 ∈ 𝑦, 1𝑜, ∅) =
1𝑜 → ∅ ∈ ∅)) |
44 | 37, 43 | mtoi 189 |
. . . . . . . . . . . . 13
⊢ (¬
𝑤 ∈ 𝑦 → ¬ if(𝑤 ∈ 𝑦, 1𝑜, ∅) =
1𝑜) |
45 | 44 | con4i 112 |
. . . . . . . . . . . 12
⊢ (if(𝑤 ∈ 𝑦, 1𝑜, ∅) =
1𝑜 → 𝑤 ∈ 𝑦) |
46 | 36, 45 | impbii 198 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ 𝑦 ↔ if(𝑤 ∈ 𝑦, 1𝑜, ∅) =
1𝑜) |
47 | 35, 46 | syl6rbbr 278 |
. . . . . . . . . 10
⊢ (((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))) ∧
𝑤 ∈ 𝐴) → (𝑤 ∈ 𝑦 ↔ (𝑥‘𝑤) = 1𝑜)) |
48 | | fvex 6113 |
. . . . . . . . . . 11
⊢ (𝑥‘𝑤) ∈ V |
49 | 48 | elsn 4140 |
. . . . . . . . . 10
⊢ ((𝑥‘𝑤) ∈ {1𝑜} ↔
(𝑥‘𝑤) = 1𝑜) |
50 | 47, 49 | syl6bbr 277 |
. . . . . . . . 9
⊢ (((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))) ∧
𝑤 ∈ 𝐴) → (𝑤 ∈ 𝑦 ↔ (𝑥‘𝑤) ∈
{1𝑜})) |
51 | 50 | pm5.32da 671 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))) →
((𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝑦) ↔ (𝑤 ∈ 𝐴 ∧ (𝑥‘𝑤) ∈
{1𝑜}))) |
52 | | ssel 3562 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ 𝐴 → (𝑤 ∈ 𝑦 → 𝑤 ∈ 𝐴)) |
53 | 52 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))) →
(𝑤 ∈ 𝑦 → 𝑤 ∈ 𝐴)) |
54 | 53 | pm4.71rd 665 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))) →
(𝑤 ∈ 𝑦 ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝑦))) |
55 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝑥:𝐴⟶2𝑜 → 𝑥 Fn 𝐴) |
56 | | elpreima 6245 |
. . . . . . . . 9
⊢ (𝑥 Fn 𝐴 → (𝑤 ∈ (◡𝑥 “ {1𝑜}) ↔
(𝑤 ∈ 𝐴 ∧ (𝑥‘𝑤) ∈
{1𝑜}))) |
57 | 28, 55, 56 | 3syl 18 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))) →
(𝑤 ∈ (◡𝑥 “ {1𝑜}) ↔
(𝑤 ∈ 𝐴 ∧ (𝑥‘𝑤) ∈
{1𝑜}))) |
58 | 51, 54, 57 | 3bitr4d 299 |
. . . . . . 7
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))) →
(𝑤 ∈ 𝑦 ↔ 𝑤 ∈ (◡𝑥 “
{1𝑜}))) |
59 | 58 | eqrdv 2608 |
. . . . . 6
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))) →
𝑦 = (◡𝑥 “
{1𝑜})) |
60 | 28, 59 | jca 553 |
. . . . 5
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))) →
(𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “
{1𝑜}))) |
61 | | simpr 476 |
. . . . . . 7
⊢ ((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) →
𝑦 = (◡𝑥 “
{1𝑜})) |
62 | | cnvimass 5404 |
. . . . . . . 8
⊢ (◡𝑥 “ {1𝑜}) ⊆ dom
𝑥 |
63 | | fdm 5964 |
. . . . . . . . 9
⊢ (𝑥:𝐴⟶2𝑜 → dom
𝑥 = 𝐴) |
64 | 63 | adantr 480 |
. . . . . . . 8
⊢ ((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) → dom
𝑥 = 𝐴) |
65 | 62, 64 | syl5sseq 3616 |
. . . . . . 7
⊢ ((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) →
(◡𝑥 “ {1𝑜}) ⊆
𝐴) |
66 | 61, 65 | eqsstrd 3602 |
. . . . . 6
⊢ ((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) →
𝑦 ⊆ 𝐴) |
67 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ (((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) → 𝑦 = (◡𝑥 “
{1𝑜})) |
68 | 67 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ (((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) → (𝑤 ∈ 𝑦 ↔ 𝑤 ∈ (◡𝑥 “
{1𝑜}))) |
69 | 55 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) →
𝑥 Fn 𝐴) |
70 | | fnbrfvb 6146 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 Fn 𝐴 ∧ 𝑤 ∈ 𝐴) → ((𝑥‘𝑤) = 1𝑜 ↔ 𝑤𝑥1𝑜)) |
71 | 69, 70 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ (((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) → ((𝑥‘𝑤) = 1𝑜 ↔ 𝑤𝑥1𝑜)) |
72 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑤 ∈ V |
73 | 72 | eliniseg 5413 |
. . . . . . . . . . . . . . 15
⊢
(1𝑜 ∈ On → (𝑤 ∈ (◡𝑥 “ {1𝑜}) ↔
𝑤𝑥1𝑜)) |
74 | 12, 73 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (◡𝑥 “ {1𝑜}) ↔
𝑤𝑥1𝑜) |
75 | 71, 74 | syl6bbr 277 |
. . . . . . . . . . . . 13
⊢ (((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) → ((𝑥‘𝑤) = 1𝑜 ↔ 𝑤 ∈ (◡𝑥 “
{1𝑜}))) |
76 | 68, 75 | bitr4d 270 |
. . . . . . . . . . . 12
⊢ (((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) → (𝑤 ∈ 𝑦 ↔ (𝑥‘𝑤) = 1𝑜)) |
77 | 76 | biimpa 500 |
. . . . . . . . . . 11
⊢ ((((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝑥‘𝑤) = 1𝑜) |
78 | 36 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) ∧ 𝑤 ∈ 𝑦) → if(𝑤 ∈ 𝑦, 1𝑜, ∅) =
1𝑜) |
79 | 77, 78 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝑥‘𝑤) = if(𝑤 ∈ 𝑦, 1𝑜,
∅)) |
80 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥:𝐴⟶2𝑜 ∧ 𝑤 ∈ 𝐴) → (𝑥‘𝑤) ∈
2𝑜) |
81 | 80 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) → (𝑥‘𝑤) ∈
2𝑜) |
82 | | df2o3 7460 |
. . . . . . . . . . . . . . . . 17
⊢
2𝑜 = {∅,
1𝑜} |
83 | 81, 82 | syl6eleq 2698 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) → (𝑥‘𝑤) ∈ {∅,
1𝑜}) |
84 | 48 | elpr 4146 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥‘𝑤) ∈ {∅, 1𝑜}
↔ ((𝑥‘𝑤) = ∅ ∨ (𝑥‘𝑤) = 1𝑜)) |
85 | 83, 84 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) → ((𝑥‘𝑤) = ∅ ∨ (𝑥‘𝑤) = 1𝑜)) |
86 | 85 | ord 391 |
. . . . . . . . . . . . . 14
⊢ (((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) → (¬ (𝑥‘𝑤) = ∅ → (𝑥‘𝑤) = 1𝑜)) |
87 | 86, 76 | sylibrd 248 |
. . . . . . . . . . . . 13
⊢ (((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) → (¬ (𝑥‘𝑤) = ∅ → 𝑤 ∈ 𝑦)) |
88 | 87 | con1d 138 |
. . . . . . . . . . . 12
⊢ (((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) → (¬ 𝑤 ∈ 𝑦 → (𝑥‘𝑤) = ∅)) |
89 | 88 | imp 444 |
. . . . . . . . . . 11
⊢ ((((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) ∧ ¬ 𝑤 ∈ 𝑦) → (𝑥‘𝑤) = ∅) |
90 | 38 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) ∧ ¬ 𝑤 ∈ 𝑦) → if(𝑤 ∈ 𝑦, 1𝑜, ∅) =
∅) |
91 | 89, 90 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) ∧ ¬ 𝑤 ∈ 𝑦) → (𝑥‘𝑤) = if(𝑤 ∈ 𝑦, 1𝑜,
∅)) |
92 | 79, 91 | pm2.61dan 828 |
. . . . . . . . 9
⊢ (((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) → (𝑥‘𝑤) = if(𝑤 ∈ 𝑦, 1𝑜,
∅)) |
93 | 33 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜,
∅))‘𝑤) =
if(𝑤 ∈ 𝑦, 1𝑜,
∅)) |
94 | 92, 93 | eqtr4d 2647 |
. . . . . . . 8
⊢ (((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ∧
𝑤 ∈ 𝐴) → (𝑥‘𝑤) = ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜,
∅))‘𝑤)) |
95 | 94 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) →
∀𝑤 ∈ 𝐴 (𝑥‘𝑤) = ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜,
∅))‘𝑤)) |
96 | | ffn 5958 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅)):𝐴⟶2𝑜
→ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅)) Fn 𝐴) |
97 | 25, 96 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅)) Fn 𝐴 |
98 | | eqfnfv 6219 |
. . . . . . . 8
⊢ ((𝑥 Fn 𝐴 ∧ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅)) Fn 𝐴) → (𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅)) ↔
∀𝑤 ∈ 𝐴 (𝑥‘𝑤) = ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜,
∅))‘𝑤))) |
99 | 69, 97, 98 | sylancl 693 |
. . . . . . 7
⊢ ((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) →
(𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅)) ↔
∀𝑤 ∈ 𝐴 (𝑥‘𝑤) = ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜,
∅))‘𝑤))) |
100 | 95, 99 | mpbird 246 |
. . . . . 6
⊢ ((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) →
𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜,
∅))) |
101 | 66, 100 | jca 553 |
. . . . 5
⊢ ((𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “ {1𝑜})) →
(𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜,
∅)))) |
102 | 60, 101 | impbii 198 |
. . . 4
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))) ↔
(𝑥:𝐴⟶2𝑜 ∧ 𝑦 = (◡𝑥 “
{1𝑜}))) |
103 | 11, 102 | syl6bbr 277 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ↔
(𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜,
∅))))) |
104 | | selpw 4115 |
. . . 4
⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴) |
105 | 104 | anbi1i 727 |
. . 3
⊢ ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜, ∅))) ↔
(𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜,
∅)))) |
106 | 103, 105 | syl6bbr 277 |
. 2
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑦 = (◡𝑥 “ {1𝑜})) ↔
(𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜,
∅))))) |
107 | 1, 5, 7, 106 | f1ocnvd 6782 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐹:(2𝑜
↑𝑚 𝐴)–1-1-onto→𝒫 𝐴 ∧ ◡𝐹 = (𝑦 ∈ 𝒫 𝐴 ↦ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1𝑜,
∅))))) |