| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pw2f1o2.f | . 2
⊢ 𝐹 = (𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) | 
| 2 |  | vex 3483 | . . . 4
⊢ 𝑥 ∈ V | 
| 3 | 2 | cnvex 7948 | . . 3
⊢ ◡𝑥 ∈ V | 
| 4 |  | imaexg 7936 | . . 3
⊢ (◡𝑥 ∈ V → (◡𝑥 “ {1o}) ∈
V) | 
| 5 | 3, 4 | mp1i 13 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (2o ↑m
𝐴)) → (◡𝑥 “ {1o}) ∈
V) | 
| 6 |  | mptexg 7242 | . . 3
⊢ (𝐴 ∈ 𝑉 → (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) ∈
V) | 
| 7 | 6 | adantr 480 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ 𝒫 𝐴) → (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) ∈
V) | 
| 8 |  | 2on 8521 | . . . . . 6
⊢
2o ∈ On | 
| 9 |  | elmapg 8880 | . . . . . 6
⊢
((2o ∈ On ∧ 𝐴 ∈ 𝑉) → (𝑥 ∈ (2o ↑m
𝐴) ↔ 𝑥:𝐴⟶2o)) | 
| 10 | 8, 9 | mpan 690 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (2o ↑m
𝐴) ↔ 𝑥:𝐴⟶2o)) | 
| 11 | 10 | anbi1d 631 | . . . 4
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (2o ↑m
𝐴) ∧ 𝑦 = (◡𝑥 “ {1o})) ↔ (𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})))) | 
| 12 |  | 1oex 8517 | . . . . . . . . . . . 12
⊢
1o ∈ V | 
| 13 | 12 | sucid 6465 | . . . . . . . . . . 11
⊢
1o ∈ suc 1o | 
| 14 |  | df-2o 8508 | . . . . . . . . . . 11
⊢
2o = suc 1o | 
| 15 | 13, 14 | eleqtrri 2839 | . . . . . . . . . 10
⊢
1o ∈ 2o | 
| 16 |  | 0ex 5306 | . . . . . . . . . . . 12
⊢ ∅
∈ V | 
| 17 | 16 | prid1 4761 | . . . . . . . . . . 11
⊢ ∅
∈ {∅, {∅}} | 
| 18 |  | df2o2 8516 | . . . . . . . . . . 11
⊢
2o = {∅, {∅}} | 
| 19 | 17, 18 | eleqtrri 2839 | . . . . . . . . . 10
⊢ ∅
∈ 2o | 
| 20 | 15, 19 | ifcli 4572 | . . . . . . . . 9
⊢ if(𝑧 ∈ 𝑦, 1o, ∅) ∈
2o | 
| 21 | 20 | rgenw 3064 | . . . . . . . 8
⊢
∀𝑧 ∈
𝐴 if(𝑧 ∈ 𝑦, 1o, ∅) ∈
2o | 
| 22 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) | 
| 23 | 22 | fmpt 7129 | . . . . . . . 8
⊢
(∀𝑧 ∈
𝐴 if(𝑧 ∈ 𝑦, 1o, ∅) ∈
2o ↔ (𝑧
∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)):𝐴⟶2o) | 
| 24 | 21, 23 | mpbi 230 | . . . . . . 7
⊢ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)):𝐴⟶2o | 
| 25 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) | 
| 26 | 25 | feq1d 6719 | . . . . . . 7
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → (𝑥:𝐴⟶2o ↔ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)):𝐴⟶2o)) | 
| 27 | 24, 26 | mpbiri 258 | . . . . . 6
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → 𝑥:𝐴⟶2o) | 
| 28 |  | iftrue 4530 | . . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑦 → if(𝑤 ∈ 𝑦, 1o, ∅) =
1o) | 
| 29 |  | noel 4337 | . . . . . . . . . . . . . 14
⊢  ¬
∅ ∈ ∅ | 
| 30 |  | iffalse 4533 | . . . . . . . . . . . . . . . 16
⊢ (¬
𝑤 ∈ 𝑦 → if(𝑤 ∈ 𝑦, 1o, ∅) =
∅) | 
| 31 | 30 | eqeq1d 2738 | . . . . . . . . . . . . . . 15
⊢ (¬
𝑤 ∈ 𝑦 → (if(𝑤 ∈ 𝑦, 1o, ∅) = 1o
↔ ∅ = 1o)) | 
| 32 |  | 0lt1o 8543 | . . . . . . . . . . . . . . . 16
⊢ ∅
∈ 1o | 
| 33 |  | eleq2 2829 | . . . . . . . . . . . . . . . 16
⊢ (∅
= 1o → (∅ ∈ ∅ ↔ ∅ ∈
1o)) | 
| 34 | 32, 33 | mpbiri 258 | . . . . . . . . . . . . . . 15
⊢ (∅
= 1o → ∅ ∈ ∅) | 
| 35 | 31, 34 | biimtrdi 253 | . . . . . . . . . . . . . 14
⊢ (¬
𝑤 ∈ 𝑦 → (if(𝑤 ∈ 𝑦, 1o, ∅) = 1o
→ ∅ ∈ ∅)) | 
| 36 | 29, 35 | mtoi 199 | . . . . . . . . . . . . 13
⊢ (¬
𝑤 ∈ 𝑦 → ¬ if(𝑤 ∈ 𝑦, 1o, ∅) =
1o) | 
| 37 | 36 | con4i 114 | . . . . . . . . . . . 12
⊢ (if(𝑤 ∈ 𝑦, 1o, ∅) = 1o
→ 𝑤 ∈ 𝑦) | 
| 38 | 28, 37 | impbii 209 | . . . . . . . . . . 11
⊢ (𝑤 ∈ 𝑦 ↔ if(𝑤 ∈ 𝑦, 1o, ∅) =
1o) | 
| 39 | 25 | fveq1d 6907 | . . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → (𝑥‘𝑤) = ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))‘𝑤)) | 
| 40 |  | elequ1 2114 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑤 → (𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦)) | 
| 41 | 40 | ifbid 4548 | . . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑤 → if(𝑧 ∈ 𝑦, 1o, ∅) = if(𝑤 ∈ 𝑦, 1o, ∅)) | 
| 42 | 12, 16 | ifcli 4572 | . . . . . . . . . . . . . 14
⊢ if(𝑤 ∈ 𝑦, 1o, ∅) ∈
V | 
| 43 | 41, 22, 42 | fvmpt 7015 | . . . . . . . . . . . . 13
⊢ (𝑤 ∈ 𝐴 → ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))‘𝑤) = if(𝑤 ∈ 𝑦, 1o, ∅)) | 
| 44 | 39, 43 | sylan9eq 2796 | . . . . . . . . . . . 12
⊢ (((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) ∧ 𝑤 ∈ 𝐴) → (𝑥‘𝑤) = if(𝑤 ∈ 𝑦, 1o, ∅)) | 
| 45 | 44 | eqeq1d 2738 | . . . . . . . . . . 11
⊢ (((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) ∧ 𝑤 ∈ 𝐴) → ((𝑥‘𝑤) = 1o ↔ if(𝑤 ∈ 𝑦, 1o, ∅) =
1o)) | 
| 46 | 38, 45 | bitr4id 290 | . . . . . . . . . 10
⊢ (((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) ∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ 𝑦 ↔ (𝑥‘𝑤) = 1o)) | 
| 47 |  | fvex 6918 | . . . . . . . . . . 11
⊢ (𝑥‘𝑤) ∈ V | 
| 48 | 47 | elsn 4640 | . . . . . . . . . 10
⊢ ((𝑥‘𝑤) ∈ {1o} ↔ (𝑥‘𝑤) = 1o) | 
| 49 | 46, 48 | bitr4di 289 | . . . . . . . . 9
⊢ (((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) ∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ 𝑦 ↔ (𝑥‘𝑤) ∈ {1o})) | 
| 50 | 49 | pm5.32da 579 | . . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → ((𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝑦) ↔ (𝑤 ∈ 𝐴 ∧ (𝑥‘𝑤) ∈ {1o}))) | 
| 51 |  | ssel 3976 | . . . . . . . . . 10
⊢ (𝑦 ⊆ 𝐴 → (𝑤 ∈ 𝑦 → 𝑤 ∈ 𝐴)) | 
| 52 | 51 | adantr 480 | . . . . . . . . 9
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → (𝑤 ∈ 𝑦 → 𝑤 ∈ 𝐴)) | 
| 53 | 52 | pm4.71rd 562 | . . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → (𝑤 ∈ 𝑦 ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝑦))) | 
| 54 |  | ffn 6735 | . . . . . . . . 9
⊢ (𝑥:𝐴⟶2o → 𝑥 Fn 𝐴) | 
| 55 |  | elpreima 7077 | . . . . . . . . 9
⊢ (𝑥 Fn 𝐴 → (𝑤 ∈ (◡𝑥 “ {1o}) ↔ (𝑤 ∈ 𝐴 ∧ (𝑥‘𝑤) ∈ {1o}))) | 
| 56 | 27, 54, 55 | 3syl 18 | . . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → (𝑤 ∈ (◡𝑥 “ {1o}) ↔ (𝑤 ∈ 𝐴 ∧ (𝑥‘𝑤) ∈ {1o}))) | 
| 57 | 50, 53, 56 | 3bitr4d 311 | . . . . . . 7
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → (𝑤 ∈ 𝑦 ↔ 𝑤 ∈ (◡𝑥 “ {1o}))) | 
| 58 | 57 | eqrdv 2734 | . . . . . 6
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → 𝑦 = (◡𝑥 “ {1o})) | 
| 59 | 27, 58 | jca 511 | . . . . 5
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) → (𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o}))) | 
| 60 |  | simpr 484 | . . . . . . 7
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) → 𝑦 = (◡𝑥 “ {1o})) | 
| 61 |  | cnvimass 6099 | . . . . . . . 8
⊢ (◡𝑥 “ {1o}) ⊆ dom 𝑥 | 
| 62 |  | fdm 6744 | . . . . . . . . 9
⊢ (𝑥:𝐴⟶2o → dom 𝑥 = 𝐴) | 
| 63 | 62 | adantr 480 | . . . . . . . 8
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) → dom 𝑥 = 𝐴) | 
| 64 | 61, 63 | sseqtrid 4025 | . . . . . . 7
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) → (◡𝑥 “ {1o}) ⊆ 𝐴) | 
| 65 | 60, 64 | eqsstrd 4017 | . . . . . 6
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) → 𝑦 ⊆ 𝐴) | 
| 66 |  | simplr 768 | . . . . . . . . . . . . . 14
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → 𝑦 = (◡𝑥 “ {1o})) | 
| 67 | 66 | eleq2d 2826 | . . . . . . . . . . . . 13
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ 𝑦 ↔ 𝑤 ∈ (◡𝑥 “ {1o}))) | 
| 68 | 54 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) → 𝑥 Fn 𝐴) | 
| 69 |  | fnbrfvb 6958 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 Fn 𝐴 ∧ 𝑤 ∈ 𝐴) → ((𝑥‘𝑤) = 1o ↔ 𝑤𝑥1o)) | 
| 70 | 68, 69 | sylan 580 | . . . . . . . . . . . . . 14
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → ((𝑥‘𝑤) = 1o ↔ 𝑤𝑥1o)) | 
| 71 |  | 1on 8519 | . . . . . . . . . . . . . . 15
⊢
1o ∈ On | 
| 72 |  | vex 3483 | . . . . . . . . . . . . . . . 16
⊢ 𝑤 ∈ V | 
| 73 | 72 | eliniseg 6111 | . . . . . . . . . . . . . . 15
⊢
(1o ∈ On → (𝑤 ∈ (◡𝑥 “ {1o}) ↔ 𝑤𝑥1o)) | 
| 74 | 71, 73 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (◡𝑥 “ {1o}) ↔ 𝑤𝑥1o) | 
| 75 | 70, 74 | bitr4di 289 | . . . . . . . . . . . . 13
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → ((𝑥‘𝑤) = 1o ↔ 𝑤 ∈ (◡𝑥 “ {1o}))) | 
| 76 | 67, 75 | bitr4d 282 | . . . . . . . . . . . 12
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ 𝑦 ↔ (𝑥‘𝑤) = 1o)) | 
| 77 | 76 | biimpa 476 | . . . . . . . . . . 11
⊢ ((((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝑥‘𝑤) = 1o) | 
| 78 | 28 | adantl 481 | . . . . . . . . . . 11
⊢ ((((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) ∧ 𝑤 ∈ 𝑦) → if(𝑤 ∈ 𝑦, 1o, ∅) =
1o) | 
| 79 | 77, 78 | eqtr4d 2779 | . . . . . . . . . 10
⊢ ((((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) ∧ 𝑤 ∈ 𝑦) → (𝑥‘𝑤) = if(𝑤 ∈ 𝑦, 1o, ∅)) | 
| 80 |  | ffvelcdm 7100 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥:𝐴⟶2o ∧ 𝑤 ∈ 𝐴) → (𝑥‘𝑤) ∈ 2o) | 
| 81 | 80 | adantlr 715 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (𝑥‘𝑤) ∈ 2o) | 
| 82 |  | df2o3 8515 | . . . . . . . . . . . . . . . . 17
⊢
2o = {∅, 1o} | 
| 83 | 81, 82 | eleqtrdi 2850 | . . . . . . . . . . . . . . . 16
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (𝑥‘𝑤) ∈ {∅,
1o}) | 
| 84 | 47 | elpr 4649 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥‘𝑤) ∈ {∅, 1o} ↔
((𝑥‘𝑤) = ∅ ∨ (𝑥‘𝑤) = 1o)) | 
| 85 | 83, 84 | sylib 218 | . . . . . . . . . . . . . . 15
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → ((𝑥‘𝑤) = ∅ ∨ (𝑥‘𝑤) = 1o)) | 
| 86 | 85 | ord 864 | . . . . . . . . . . . . . 14
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (¬ (𝑥‘𝑤) = ∅ → (𝑥‘𝑤) = 1o)) | 
| 87 | 86, 76 | sylibrd 259 | . . . . . . . . . . . . 13
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (¬ (𝑥‘𝑤) = ∅ → 𝑤 ∈ 𝑦)) | 
| 88 | 87 | con1d 145 | . . . . . . . . . . . 12
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (¬ 𝑤 ∈ 𝑦 → (𝑥‘𝑤) = ∅)) | 
| 89 | 88 | imp 406 | . . . . . . . . . . 11
⊢ ((((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 ∈ 𝑦) → (𝑥‘𝑤) = ∅) | 
| 90 | 30 | adantl 481 | . . . . . . . . . . 11
⊢ ((((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 ∈ 𝑦) → if(𝑤 ∈ 𝑦, 1o, ∅) =
∅) | 
| 91 | 89, 90 | eqtr4d 2779 | . . . . . . . . . 10
⊢ ((((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) ∧ ¬ 𝑤 ∈ 𝑦) → (𝑥‘𝑤) = if(𝑤 ∈ 𝑦, 1o, ∅)) | 
| 92 | 79, 91 | pm2.61dan 812 | . . . . . . . . 9
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (𝑥‘𝑤) = if(𝑤 ∈ 𝑦, 1o, ∅)) | 
| 93 | 43 | adantl 481 | . . . . . . . . 9
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))‘𝑤) = if(𝑤 ∈ 𝑦, 1o, ∅)) | 
| 94 | 92, 93 | eqtr4d 2779 | . . . . . . . 8
⊢ (((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) ∧ 𝑤 ∈ 𝐴) → (𝑥‘𝑤) = ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))‘𝑤)) | 
| 95 | 94 | ralrimiva 3145 | . . . . . . 7
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) →
∀𝑤 ∈ 𝐴 (𝑥‘𝑤) = ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))‘𝑤)) | 
| 96 |  | ffn 6735 | . . . . . . . . 9
⊢ ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)):𝐴⟶2o → (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) Fn 𝐴) | 
| 97 | 24, 96 | ax-mp 5 | . . . . . . . 8
⊢ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) Fn 𝐴 | 
| 98 |  | eqfnfv 7050 | . . . . . . . 8
⊢ ((𝑥 Fn 𝐴 ∧ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) Fn 𝐴) → (𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) ↔
∀𝑤 ∈ 𝐴 (𝑥‘𝑤) = ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))‘𝑤))) | 
| 99 | 68, 97, 98 | sylancl 586 | . . . . . . 7
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) → (𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)) ↔
∀𝑤 ∈ 𝐴 (𝑥‘𝑤) = ((𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))‘𝑤))) | 
| 100 | 95, 99 | mpbird 257 | . . . . . 6
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) → 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) | 
| 101 | 65, 100 | jca 511 | . . . . 5
⊢ ((𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o})) → (𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)))) | 
| 102 | 59, 101 | impbii 209 | . . . 4
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) ↔ (𝑥:𝐴⟶2o ∧ 𝑦 = (◡𝑥 “ {1o}))) | 
| 103 | 11, 102 | bitr4di 289 | . . 3
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (2o ↑m
𝐴) ∧ 𝑦 = (◡𝑥 “ {1o})) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o,
∅))))) | 
| 104 |  | velpw 4604 | . . . 4
⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴) | 
| 105 | 104 | anbi1i 624 | . . 3
⊢ ((𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅))) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o, ∅)))) | 
| 106 | 103, 105 | bitr4di 289 | . 2
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (2o ↑m
𝐴) ∧ 𝑦 = (◡𝑥 “ {1o})) ↔ (𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o,
∅))))) | 
| 107 | 1, 5, 7, 106 | f1ocnvd 7685 | 1
⊢ (𝐴 ∈ 𝑉 → (𝐹:(2o ↑m 𝐴)–1-1-onto→𝒫 𝐴 ∧ ◡𝐹 = (𝑦 ∈ 𝒫 𝐴 ↦ (𝑧 ∈ 𝐴 ↦ if(𝑧 ∈ 𝑦, 1o,
∅))))) |