| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cnfcom3c 9746 | . 2
⊢ (𝐴 ∈ On → ∃𝑛∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦))) | 
| 2 |  | df-2o 8507 | . . . . . . . 8
⊢
2o = suc 1o | 
| 3 | 2 | oveq2i 7442 | . . . . . . 7
⊢ (ω
↑o 2o) = (ω ↑o suc
1o) | 
| 4 |  | omelon 9686 | . . . . . . . 8
⊢ ω
∈ On | 
| 5 |  | 1on 8518 | . . . . . . . 8
⊢
1o ∈ On | 
| 6 |  | oesuc 8565 | . . . . . . . 8
⊢ ((ω
∈ On ∧ 1o ∈ On) → (ω ↑o suc
1o) = ((ω ↑o 1o)
·o ω)) | 
| 7 | 4, 5, 6 | mp2an 692 | . . . . . . 7
⊢ (ω
↑o suc 1o) = ((ω ↑o
1o) ·o ω) | 
| 8 |  | oe1 8582 | . . . . . . . . 9
⊢ (ω
∈ On → (ω ↑o 1o) =
ω) | 
| 9 | 4, 8 | ax-mp 5 | . . . . . . . 8
⊢ (ω
↑o 1o) = ω | 
| 10 | 9 | oveq1i 7441 | . . . . . . 7
⊢ ((ω
↑o 1o) ·o ω) = (ω
·o ω) | 
| 11 | 3, 7, 10 | 3eqtri 2769 | . . . . . 6
⊢ (ω
↑o 2o) = (ω ·o
ω) | 
| 12 |  | omxpen 9114 | . . . . . . 7
⊢ ((ω
∈ On ∧ ω ∈ On) → (ω ·o
ω) ≈ (ω × ω)) | 
| 13 | 4, 4, 12 | mp2an 692 | . . . . . 6
⊢ (ω
·o ω) ≈ (ω ×
ω) | 
| 14 | 11, 13 | eqbrtri 5164 | . . . . 5
⊢ (ω
↑o 2o) ≈ (ω ×
ω) | 
| 15 |  | xpomen 10055 | . . . . 5
⊢ (ω
× ω) ≈ ω | 
| 16 | 14, 15 | entri 9048 | . . . 4
⊢ (ω
↑o 2o) ≈ ω | 
| 17 | 16 | a1i 11 | . . 3
⊢ (𝐴 ∈ On → (ω
↑o 2o) ≈ ω) | 
| 18 |  | bren 8995 | . . 3
⊢ ((ω
↑o 2o) ≈ ω ↔ ∃𝑓 𝑓:(ω ↑o
2o)–1-1-onto→ω) | 
| 19 | 17, 18 | sylib 218 | . 2
⊢ (𝐴 ∈ On → ∃𝑓 𝑓:(ω ↑o
2o)–1-1-onto→ω) | 
| 20 |  | exdistrv 1955 | . . 3
⊢
(∃𝑛∃𝑓(∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω) ↔ (∃𝑛∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ ∃𝑓 𝑓:(ω ↑o
2o)–1-1-onto→ω)) | 
| 21 |  | simpl 482 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω)) → 𝐴 ∈ On) | 
| 22 |  | simprl 771 | . . . . . . 7
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω)) → ∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦))) | 
| 23 |  | sseq2 4010 | . . . . . . . . 9
⊢ (𝑥 = 𝑏 → (ω ⊆ 𝑥 ↔ ω ⊆ 𝑏)) | 
| 24 |  | oveq2 7439 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (ω ↑o 𝑦) = (ω ↑o
𝑤)) | 
| 25 | 24 | f1oeq3d 6845 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → ((𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦) ↔ (𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑤))) | 
| 26 | 25 | cbvrexvw 3238 | . . . . . . . . . 10
⊢
(∃𝑦 ∈ (On
∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦) ↔ ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑤)) | 
| 27 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑏 → (𝑛‘𝑥) = (𝑛‘𝑏)) | 
| 28 | 27 | f1oeq1d 6843 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑏 → ((𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑤) ↔ (𝑛‘𝑏):𝑥–1-1-onto→(ω ↑o 𝑤))) | 
| 29 |  | f1oeq2 6837 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑏 → ((𝑛‘𝑏):𝑥–1-1-onto→(ω ↑o 𝑤) ↔ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) | 
| 30 | 28, 29 | bitrd 279 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑏 → ((𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑤) ↔ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) | 
| 31 | 30 | rexbidv 3179 | . . . . . . . . . 10
⊢ (𝑥 = 𝑏 → (∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑤) ↔ ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) | 
| 32 | 26, 31 | bitrid 283 | . . . . . . . . 9
⊢ (𝑥 = 𝑏 → (∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦) ↔ ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) | 
| 33 | 23, 32 | imbi12d 344 | . . . . . . . 8
⊢ (𝑥 = 𝑏 → ((ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ↔ (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)))) | 
| 34 | 33 | cbvralvw 3237 | . . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ↔ ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) | 
| 35 | 22, 34 | sylib 218 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω)) → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) | 
| 36 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑏 = 𝑧 → (ω ↑o 𝑏) = (ω ↑o
𝑧)) | 
| 37 | 36 | cbvmptv 5255 | . . . . . . . 8
⊢ (𝑏 ∈ (On ∖
1o) ↦ (ω ↑o 𝑏)) = (𝑧 ∈ (On ∖ 1o) ↦
(ω ↑o 𝑧)) | 
| 38 | 37 | cnveqi 5885 | . . . . . . 7
⊢ ◡(𝑏 ∈ (On ∖ 1o) ↦
(ω ↑o 𝑏)) = ◡(𝑧 ∈ (On ∖ 1o) ↦
(ω ↑o 𝑧)) | 
| 39 | 38 | fveq1i 6907 | . . . . . 6
⊢ (◡(𝑏 ∈ (On ∖ 1o) ↦
(ω ↑o 𝑏))‘ran (𝑛‘𝑏)) = (◡(𝑧 ∈ (On ∖ 1o) ↦
(ω ↑o 𝑧))‘ran (𝑛‘𝑏)) | 
| 40 |  | 2on 8520 | . . . . . . . . . 10
⊢
2o ∈ On | 
| 41 |  | peano1 7910 | . . . . . . . . . . 11
⊢ ∅
∈ ω | 
| 42 |  | oen0 8624 | . . . . . . . . . . 11
⊢
(((ω ∈ On ∧ 2o ∈ On) ∧ ∅ ∈
ω) → ∅ ∈ (ω ↑o
2o)) | 
| 43 | 41, 42 | mpan2 691 | . . . . . . . . . 10
⊢ ((ω
∈ On ∧ 2o ∈ On) → ∅ ∈ (ω
↑o 2o)) | 
| 44 | 4, 40, 43 | mp2an 692 | . . . . . . . . 9
⊢ ∅
∈ (ω ↑o 2o) | 
| 45 |  | eqid 2737 | . . . . . . . . . 10
⊢ (𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅), ∅〉})) = (𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅),
∅〉})) | 
| 46 | 45 | fveqf1o 7322 | . . . . . . . . 9
⊢ ((𝑓:(ω ↑o
2o)–1-1-onto→ω ∧ ∅ ∈ (ω
↑o 2o) ∧ ∅ ∈ ω) → ((𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅), ∅〉})):(ω
↑o 2o)–1-1-onto→ω ∧ ((𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅),
∅〉}))‘∅) = ∅)) | 
| 47 | 44, 41, 46 | mp3an23 1455 | . . . . . . . 8
⊢ (𝑓:(ω ↑o
2o)–1-1-onto→ω → ((𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅), ∅〉})):(ω
↑o 2o)–1-1-onto→ω ∧ ((𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅),
∅〉}))‘∅) = ∅)) | 
| 48 | 47 | ad2antll 729 | . . . . . . 7
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω)) → ((𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅), ∅〉})):(ω
↑o 2o)–1-1-onto→ω ∧ ((𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅),
∅〉}))‘∅) = ∅)) | 
| 49 | 48 | simpld 494 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω)) → (𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅), ∅〉})):(ω
↑o 2o)–1-1-onto→ω) | 
| 50 | 48 | simprd 495 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω)) → ((𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅),
∅〉}))‘∅) = ∅) | 
| 51 | 21, 35, 39, 49, 50 | infxpenc2lem3 10061 | . . . . 5
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω)) → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) | 
| 52 | 51 | ex 412 | . . . 4
⊢ (𝐴 ∈ On →
((∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω) → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))) | 
| 53 | 52 | exlimdvv 1934 | . . 3
⊢ (𝐴 ∈ On → (∃𝑛∃𝑓(∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω) → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))) | 
| 54 | 20, 53 | biimtrrid 243 | . 2
⊢ (𝐴 ∈ On → ((∃𝑛∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ ∃𝑓 𝑓:(ω ↑o
2o)–1-1-onto→ω) → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))) | 
| 55 | 1, 19, 54 | mp2and 699 | 1
⊢ (𝐴 ∈ On → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |