Proof of Theorem pwfi2f1o
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . . 5
⊢ (𝑥 ∈ (2o
↑m 𝐴)
↦ (◡𝑥 “ {1o})) = (𝑥 ∈ (2o
↑m 𝐴)
↦ (◡𝑥 “ {1o})) | 
| 2 | 1 | pw2f1o2 43050 | . . . 4
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})):(2o
↑m 𝐴)–1-1-onto→𝒫 𝐴) | 
| 3 |  | f1of1 6847 | . . . 4
⊢ ((𝑥 ∈ (2o
↑m 𝐴)
↦ (◡𝑥 “ {1o})):(2o
↑m 𝐴)–1-1-onto→𝒫 𝐴 → (𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})):(2o
↑m 𝐴)–1-1→𝒫 𝐴) | 
| 4 | 2, 3 | syl 17 | . . 3
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})):(2o
↑m 𝐴)–1-1→𝒫 𝐴) | 
| 5 |  | pwfi2f1o.s | . . . 4
⊢ 𝑆 = {𝑦 ∈ (2o ↑m
𝐴) ∣ 𝑦 finSupp
∅} | 
| 6 |  | ssrab2 4080 | . . . 4
⊢ {𝑦 ∈ (2o
↑m 𝐴)
∣ 𝑦 finSupp ∅}
⊆ (2o ↑m 𝐴) | 
| 7 | 5, 6 | eqsstri 4030 | . . 3
⊢ 𝑆 ⊆ (2o
↑m 𝐴) | 
| 8 |  | f1ores 6862 | . . 3
⊢ (((𝑥 ∈ (2o
↑m 𝐴)
↦ (◡𝑥 “ {1o})):(2o
↑m 𝐴)–1-1→𝒫 𝐴 ∧ 𝑆 ⊆ (2o ↑m
𝐴)) → ((𝑥 ∈ (2o
↑m 𝐴)
↦ (◡𝑥 “ {1o})) ↾ 𝑆):𝑆–1-1-onto→((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) “ 𝑆)) | 
| 9 | 4, 7, 8 | sylancl 586 | . 2
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) ↾ 𝑆):𝑆–1-1-onto→((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) “ 𝑆)) | 
| 10 |  | elmapfun 8906 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ (2o
↑m 𝐴)
→ Fun 𝑦) | 
| 11 |  | id 22 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ (2o
↑m 𝐴)
→ 𝑦 ∈
(2o ↑m 𝐴)) | 
| 12 |  | 0ex 5307 | . . . . . . . . . . . . . 14
⊢ ∅
∈ V | 
| 13 | 12 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ (2o
↑m 𝐴)
→ ∅ ∈ V) | 
| 14 | 10, 11, 13 | 3jca 1129 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ (2o
↑m 𝐴)
→ (Fun 𝑦 ∧ 𝑦 ∈ (2o
↑m 𝐴) ∧
∅ ∈ V)) | 
| 15 | 14 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ (2o ↑m
𝐴)) → (Fun 𝑦 ∧ 𝑦 ∈ (2o ↑m
𝐴) ∧ ∅ ∈
V)) | 
| 16 |  | funisfsupp 9407 | . . . . . . . . . . 11
⊢ ((Fun
𝑦 ∧ 𝑦 ∈ (2o ↑m
𝐴) ∧ ∅ ∈ V)
→ (𝑦 finSupp ∅
↔ (𝑦 supp ∅)
∈ Fin)) | 
| 17 | 15, 16 | syl 17 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ (2o ↑m
𝐴)) → (𝑦 finSupp ∅ ↔ (𝑦 supp ∅) ∈
Fin)) | 
| 18 | 13 | anim2i 617 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ (2o ↑m
𝐴)) → (𝐴 ∈ 𝑉 ∧ ∅ ∈ V)) | 
| 19 |  | elmapi 8889 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (2o
↑m 𝐴)
→ 𝑦:𝐴⟶2o) | 
| 20 | 19 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ (2o ↑m
𝐴)) → 𝑦:𝐴⟶2o) | 
| 21 |  | fsuppeq 8200 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ ∅ ∈ V) → (𝑦:𝐴⟶2o → (𝑦 supp ∅) = (◡𝑦 “ (2o ∖
{∅})))) | 
| 22 | 18, 20, 21 | sylc 65 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ (2o ↑m
𝐴)) → (𝑦 supp ∅) = (◡𝑦 “ (2o ∖
{∅}))) | 
| 23 |  | df-2o 8507 | . . . . . . . . . . . . . . . 16
⊢
2o = suc 1o | 
| 24 |  | df-suc 6390 | . . . . . . . . . . . . . . . . 17
⊢ suc
1o = (1o ∪ {1o}) | 
| 25 | 24 | equncomi 4160 | . . . . . . . . . . . . . . . 16
⊢ suc
1o = ({1o} ∪ 1o) | 
| 26 | 23, 25 | eqtri 2765 | . . . . . . . . . . . . . . 15
⊢
2o = ({1o} ∪ 1o) | 
| 27 |  | df1o2 8513 | . . . . . . . . . . . . . . . 16
⊢
1o = {∅} | 
| 28 | 27 | eqcomi 2746 | . . . . . . . . . . . . . . 15
⊢ {∅}
= 1o | 
| 29 | 26, 28 | difeq12i 4124 | . . . . . . . . . . . . . 14
⊢
(2o ∖ {∅}) = (({1o} ∪
1o) ∖ 1o) | 
| 30 |  | difun2 4481 | . . . . . . . . . . . . . . 15
⊢
(({1o} ∪ 1o) ∖ 1o) =
({1o} ∖ 1o) | 
| 31 |  | incom 4209 | . . . . . . . . . . . . . . . . 17
⊢
({1o} ∩ 1o) = (1o ∩
{1o}) | 
| 32 |  | 1on 8518 | . . . . . . . . . . . . . . . . . . 19
⊢
1o ∈ On | 
| 33 | 32 | onordi 6495 | . . . . . . . . . . . . . . . . . 18
⊢ Ord
1o | 
| 34 |  | orddisj 6422 | . . . . . . . . . . . . . . . . . 18
⊢ (Ord
1o → (1o ∩ {1o}) =
∅) | 
| 35 | 33, 34 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢
(1o ∩ {1o}) = ∅ | 
| 36 | 31, 35 | eqtri 2765 | . . . . . . . . . . . . . . . 16
⊢
({1o} ∩ 1o) = ∅ | 
| 37 |  | disj3 4454 | . . . . . . . . . . . . . . . 16
⊢
(({1o} ∩ 1o) = ∅ ↔ {1o}
= ({1o} ∖ 1o)) | 
| 38 | 36, 37 | mpbi 230 | . . . . . . . . . . . . . . 15
⊢
{1o} = ({1o} ∖
1o) | 
| 39 | 30, 38 | eqtr4i 2768 | . . . . . . . . . . . . . 14
⊢
(({1o} ∪ 1o) ∖ 1o) =
{1o} | 
| 40 | 29, 39 | eqtri 2765 | . . . . . . . . . . . . 13
⊢
(2o ∖ {∅}) = {1o} | 
| 41 | 40 | imaeq2i 6076 | . . . . . . . . . . . 12
⊢ (◡𝑦 “ (2o ∖ {∅})) =
(◡𝑦 “ {1o}) | 
| 42 | 22, 41 | eqtrdi 2793 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ (2o ↑m
𝐴)) → (𝑦 supp ∅) = (◡𝑦 “ {1o})) | 
| 43 | 42 | eleq1d 2826 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ (2o ↑m
𝐴)) → ((𝑦 supp ∅) ∈ Fin ↔
(◡𝑦 “ {1o}) ∈
Fin)) | 
| 44 |  | cnvimass 6100 | . . . . . . . . . . . 12
⊢ (◡𝑦 “ {1o}) ⊆ dom 𝑦 | 
| 45 | 44, 20 | fssdm 6755 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ (2o ↑m
𝐴)) → (◡𝑦 “ {1o}) ⊆ 𝐴) | 
| 46 | 45 | biantrurd 532 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ (2o ↑m
𝐴)) → ((◡𝑦 “ {1o}) ∈ Fin ↔
((◡𝑦 “ {1o}) ⊆ 𝐴 ∧ (◡𝑦 “ {1o}) ∈
Fin))) | 
| 47 | 17, 43, 46 | 3bitrd 305 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ (2o ↑m
𝐴)) → (𝑦 finSupp ∅ ↔ ((◡𝑦 “ {1o}) ⊆ 𝐴 ∧ (◡𝑦 “ {1o}) ∈
Fin))) | 
| 48 |  | elfpw 9394 | . . . . . . . . 9
⊢ ((◡𝑦 “ {1o}) ∈ (𝒫
𝐴 ∩ Fin) ↔ ((◡𝑦 “ {1o}) ⊆ 𝐴 ∧ (◡𝑦 “ {1o}) ∈
Fin)) | 
| 49 | 47, 48 | bitr4di 289 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ (2o ↑m
𝐴)) → (𝑦 finSupp ∅ ↔ (◡𝑦 “ {1o}) ∈ (𝒫
𝐴 ∩
Fin))) | 
| 50 | 49 | rabbidva 3443 | . . . . . . 7
⊢ (𝐴 ∈ 𝑉 → {𝑦 ∈ (2o ↑m
𝐴) ∣ 𝑦 finSupp ∅} = {𝑦 ∈ (2o
↑m 𝐴)
∣ (◡𝑦 “ {1o}) ∈ (𝒫
𝐴 ∩
Fin)}) | 
| 51 |  | cnveq 5884 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ◡𝑥 = ◡𝑦) | 
| 52 | 51 | imaeq1d 6077 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → (◡𝑥 “ {1o}) = (◡𝑦 “ {1o})) | 
| 53 | 52 | cbvmptv 5255 | . . . . . . . 8
⊢ (𝑥 ∈ (2o
↑m 𝐴)
↦ (◡𝑥 “ {1o})) = (𝑦 ∈ (2o
↑m 𝐴)
↦ (◡𝑦 “ {1o})) | 
| 54 | 53 | mptpreima 6258 | . . . . . . 7
⊢ (◡(𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) “ (𝒫
𝐴 ∩ Fin)) = {𝑦 ∈ (2o
↑m 𝐴)
∣ (◡𝑦 “ {1o}) ∈ (𝒫
𝐴 ∩
Fin)} | 
| 55 | 50, 5, 54 | 3eqtr4g 2802 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝑆 = (◡(𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) “ (𝒫
𝐴 ∩
Fin))) | 
| 56 | 55 | imaeq2d 6078 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) “ 𝑆) = ((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) “ (◡(𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) “ (𝒫
𝐴 ∩
Fin)))) | 
| 57 |  | f1ofo 6855 | . . . . . . 7
⊢ ((𝑥 ∈ (2o
↑m 𝐴)
↦ (◡𝑥 “ {1o})):(2o
↑m 𝐴)–1-1-onto→𝒫 𝐴 → (𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})):(2o
↑m 𝐴)–onto→𝒫 𝐴) | 
| 58 | 2, 57 | syl 17 | . . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})):(2o
↑m 𝐴)–onto→𝒫 𝐴) | 
| 59 |  | inss1 4237 | . . . . . 6
⊢
(𝒫 𝐴 ∩
Fin) ⊆ 𝒫 𝐴 | 
| 60 |  | foimacnv 6865 | . . . . . 6
⊢ (((𝑥 ∈ (2o
↑m 𝐴)
↦ (◡𝑥 “ {1o})):(2o
↑m 𝐴)–onto→𝒫 𝐴 ∧ (𝒫 𝐴 ∩ Fin) ⊆ 𝒫 𝐴) → ((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) “ (◡(𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) “ (𝒫
𝐴 ∩ Fin))) = (𝒫
𝐴 ∩
Fin)) | 
| 61 | 58, 59, 60 | sylancl 586 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) “ (◡(𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) “ (𝒫
𝐴 ∩ Fin))) = (𝒫
𝐴 ∩
Fin)) | 
| 62 | 56, 61 | eqtrd 2777 | . . . 4
⊢ (𝐴 ∈ 𝑉 → ((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) “ 𝑆) = (𝒫 𝐴 ∩ Fin)) | 
| 63 |  | f1oeq3 6838 | . . . 4
⊢ (((𝑥 ∈ (2o
↑m 𝐴)
↦ (◡𝑥 “ {1o})) “ 𝑆) = (𝒫 𝐴 ∩ Fin) → (((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) ↾ 𝑆):𝑆–1-1-onto→((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) “ 𝑆) ↔ ((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) ↾ 𝑆):𝑆–1-1-onto→(𝒫 𝐴 ∩ Fin))) | 
| 64 | 62, 63 | syl 17 | . . 3
⊢ (𝐴 ∈ 𝑉 → (((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) ↾ 𝑆):𝑆–1-1-onto→((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) “ 𝑆) ↔ ((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) ↾ 𝑆):𝑆–1-1-onto→(𝒫 𝐴 ∩ Fin))) | 
| 65 |  | resmpt 6055 | . . . . . 6
⊢ (𝑆 ⊆ (2o
↑m 𝐴)
→ ((𝑥 ∈
(2o ↑m 𝐴) ↦ (◡𝑥 “ {1o})) ↾ 𝑆) = (𝑥 ∈ 𝑆 ↦ (◡𝑥 “ {1o}))) | 
| 66 | 7, 65 | ax-mp 5 | . . . . 5
⊢ ((𝑥 ∈ (2o
↑m 𝐴)
↦ (◡𝑥 “ {1o})) ↾ 𝑆) = (𝑥 ∈ 𝑆 ↦ (◡𝑥 “ {1o})) | 
| 67 |  | pwfi2f1o.f | . . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ (◡𝑥 “ {1o})) | 
| 68 | 66, 67 | eqtr4i 2768 | . . . 4
⊢ ((𝑥 ∈ (2o
↑m 𝐴)
↦ (◡𝑥 “ {1o})) ↾ 𝑆) = 𝐹 | 
| 69 |  | f1oeq1 6836 | . . . 4
⊢ (((𝑥 ∈ (2o
↑m 𝐴)
↦ (◡𝑥 “ {1o})) ↾ 𝑆) = 𝐹 → (((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) ↾ 𝑆):𝑆–1-1-onto→(𝒫 𝐴 ∩ Fin) ↔ 𝐹:𝑆–1-1-onto→(𝒫 𝐴 ∩ Fin))) | 
| 70 | 68, 69 | mp1i 13 | . . 3
⊢ (𝐴 ∈ 𝑉 → (((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) ↾ 𝑆):𝑆–1-1-onto→(𝒫 𝐴 ∩ Fin) ↔ 𝐹:𝑆–1-1-onto→(𝒫 𝐴 ∩ Fin))) | 
| 71 | 64, 70 | bitrd 279 | . 2
⊢ (𝐴 ∈ 𝑉 → (((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) ↾ 𝑆):𝑆–1-1-onto→((𝑥 ∈ (2o ↑m
𝐴) ↦ (◡𝑥 “ {1o})) “ 𝑆) ↔ 𝐹:𝑆–1-1-onto→(𝒫 𝐴 ∩ Fin))) | 
| 72 | 9, 71 | mpbid 232 | 1
⊢ (𝐴 ∈ 𝑉 → 𝐹:𝑆–1-1-onto→(𝒫 𝐴 ∩ Fin)) |