Step | Hyp | Ref
| Expression |
1 | | cnfcom3c 8486 |
. 2
⊢ (𝐴 ∈ On → ∃𝑛∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦))) |
2 | | df-2o 7448 |
. . . . . . . 8
⊢
2𝑜 = suc 1𝑜 |
3 | 2 | oveq2i 6560 |
. . . . . . 7
⊢ (ω
↑𝑜 2𝑜) = (ω
↑𝑜 suc 1𝑜) |
4 | | omelon 8426 |
. . . . . . . 8
⊢ ω
∈ On |
5 | | 1on 7454 |
. . . . . . . 8
⊢
1𝑜 ∈ On |
6 | | oesuc 7494 |
. . . . . . . 8
⊢ ((ω
∈ On ∧ 1𝑜 ∈ On) → (ω
↑𝑜 suc 1𝑜) = ((ω
↑𝑜 1𝑜) ·𝑜
ω)) |
7 | 4, 5, 6 | mp2an 704 |
. . . . . . 7
⊢ (ω
↑𝑜 suc 1𝑜) = ((ω
↑𝑜 1𝑜) ·𝑜
ω) |
8 | | oe1 7511 |
. . . . . . . . 9
⊢ (ω
∈ On → (ω ↑𝑜 1𝑜) =
ω) |
9 | 4, 8 | ax-mp 5 |
. . . . . . . 8
⊢ (ω
↑𝑜 1𝑜) = ω |
10 | 9 | oveq1i 6559 |
. . . . . . 7
⊢ ((ω
↑𝑜 1𝑜) ·𝑜
ω) = (ω ·𝑜 ω) |
11 | 3, 7, 10 | 3eqtri 2636 |
. . . . . 6
⊢ (ω
↑𝑜 2𝑜) = (ω
·𝑜 ω) |
12 | | omxpen 7947 |
. . . . . . 7
⊢ ((ω
∈ On ∧ ω ∈ On) → (ω ·𝑜
ω) ≈ (ω × ω)) |
13 | 4, 4, 12 | mp2an 704 |
. . . . . 6
⊢ (ω
·𝑜 ω) ≈ (ω ×
ω) |
14 | 11, 13 | eqbrtri 4604 |
. . . . 5
⊢ (ω
↑𝑜 2𝑜) ≈ (ω ×
ω) |
15 | | xpomen 8721 |
. . . . 5
⊢ (ω
× ω) ≈ ω |
16 | 14, 15 | entri 7896 |
. . . 4
⊢ (ω
↑𝑜 2𝑜) ≈
ω |
17 | 16 | a1i 11 |
. . 3
⊢ (𝐴 ∈ On → (ω
↑𝑜 2𝑜) ≈
ω) |
18 | | bren 7850 |
. . 3
⊢ ((ω
↑𝑜 2𝑜) ≈ ω ↔
∃𝑓 𝑓:(ω ↑𝑜
2𝑜)–1-1-onto→ω) |
19 | 17, 18 | sylib 207 |
. 2
⊢ (𝐴 ∈ On → ∃𝑓 𝑓:(ω ↑𝑜
2𝑜)–1-1-onto→ω) |
20 | | eeanv 2170 |
. . 3
⊢
(∃𝑛∃𝑓(∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦)) ∧ 𝑓:(ω ↑𝑜
2𝑜)–1-1-onto→ω) ↔ (∃𝑛∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦)) ∧ ∃𝑓 𝑓:(ω ↑𝑜
2𝑜)–1-1-onto→ω)) |
21 | | simpl 472 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦)) ∧ 𝑓:(ω ↑𝑜
2𝑜)–1-1-onto→ω)) → 𝐴 ∈ On) |
22 | | simprl 790 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦)) ∧ 𝑓:(ω ↑𝑜
2𝑜)–1-1-onto→ω)) → ∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦))) |
23 | | sseq2 3590 |
. . . . . . . . 9
⊢ (𝑥 = 𝑏 → (ω ⊆ 𝑥 ↔ ω ⊆ 𝑏)) |
24 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (ω ↑𝑜
𝑦) = (ω
↑𝑜 𝑤)) |
25 | | f1oeq3 6042 |
. . . . . . . . . . . 12
⊢ ((ω
↑𝑜 𝑦) = (ω ↑𝑜 𝑤) → ((𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦) ↔ (𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑤))) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → ((𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦) ↔ (𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑤))) |
27 | 26 | cbvrexv 3148 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈ (On
∖ 1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦) ↔ ∃𝑤 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑤)) |
28 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑏 → (𝑛‘𝑥) = (𝑛‘𝑏)) |
29 | | f1oeq1 6040 |
. . . . . . . . . . . . 13
⊢ ((𝑛‘𝑥) = (𝑛‘𝑏) → ((𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑤) ↔ (𝑛‘𝑏):𝑥–1-1-onto→(ω ↑𝑜 𝑤))) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑏 → ((𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑤) ↔ (𝑛‘𝑏):𝑥–1-1-onto→(ω ↑𝑜 𝑤))) |
31 | | f1oeq2 6041 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑏 → ((𝑛‘𝑏):𝑥–1-1-onto→(ω ↑𝑜 𝑤) ↔ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
32 | 30, 31 | bitrd 267 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑏 → ((𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑤) ↔ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
33 | 32 | rexbidv 3034 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑏 → (∃𝑤 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑤) ↔ ∃𝑤 ∈ (On ∖
1𝑜)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
34 | 27, 33 | syl5bb 271 |
. . . . . . . . 9
⊢ (𝑥 = 𝑏 → (∃𝑦 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦) ↔ ∃𝑤 ∈ (On ∖
1𝑜)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
35 | 23, 34 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑥 = 𝑏 → ((ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦)) ↔ (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1𝑜)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤)))) |
36 | 35 | cbvralv 3147 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦)) ↔ ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1𝑜)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
37 | 22, 36 | sylib 207 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦)) ∧ 𝑓:(ω ↑𝑜
2𝑜)–1-1-onto→ω)) → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1𝑜)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
38 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑏 = 𝑧 → (ω ↑𝑜
𝑏) = (ω
↑𝑜 𝑧)) |
39 | 38 | cbvmptv 4678 |
. . . . . . . 8
⊢ (𝑏 ∈ (On ∖
1𝑜) ↦ (ω ↑𝑜 𝑏)) = (𝑧 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑧)) |
40 | 39 | cnveqi 5219 |
. . . . . . 7
⊢ ◡(𝑏 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑏)) = ◡(𝑧 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑧)) |
41 | 40 | fveq1i 6104 |
. . . . . 6
⊢ (◡(𝑏 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑏))‘ran (𝑛‘𝑏)) = (◡(𝑧 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑧))‘ran (𝑛‘𝑏)) |
42 | | 2on 7455 |
. . . . . . . . . 10
⊢
2𝑜 ∈ On |
43 | | peano1 6977 |
. . . . . . . . . . 11
⊢ ∅
∈ ω |
44 | | oen0 7553 |
. . . . . . . . . . 11
⊢
(((ω ∈ On ∧ 2𝑜 ∈ On) ∧
∅ ∈ ω) → ∅ ∈ (ω
↑𝑜 2𝑜)) |
45 | 43, 44 | mpan2 703 |
. . . . . . . . . 10
⊢ ((ω
∈ On ∧ 2𝑜 ∈ On) → ∅ ∈ (ω
↑𝑜 2𝑜)) |
46 | 4, 42, 45 | mp2an 704 |
. . . . . . . . 9
⊢ ∅
∈ (ω ↑𝑜
2𝑜) |
47 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑓 ∘ (( I ↾ ((ω
↑𝑜 2𝑜) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅), ∅〉})) = (𝑓 ∘ (( I ↾ ((ω
↑𝑜 2𝑜) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅),
∅〉})) |
48 | 47 | fveqf1o 6457 |
. . . . . . . . 9
⊢ ((𝑓:(ω
↑𝑜 2𝑜)–1-1-onto→ω ∧ ∅ ∈ (ω
↑𝑜 2𝑜) ∧ ∅ ∈ ω)
→ ((𝑓 ∘ (( I
↾ ((ω ↑𝑜 2𝑜) ∖
{∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅), ∅〉})):(ω
↑𝑜 2𝑜)–1-1-onto→ω ∧ ((𝑓 ∘ (( I ↾ ((ω
↑𝑜 2𝑜) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅),
∅〉}))‘∅) = ∅)) |
49 | 46, 43, 48 | mp3an23 1408 |
. . . . . . . 8
⊢ (𝑓:(ω
↑𝑜 2𝑜)–1-1-onto→ω → ((𝑓 ∘ (( I ↾ ((ω
↑𝑜 2𝑜) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅), ∅〉})):(ω
↑𝑜 2𝑜)–1-1-onto→ω ∧ ((𝑓 ∘ (( I ↾ ((ω
↑𝑜 2𝑜) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅),
∅〉}))‘∅) = ∅)) |
50 | 49 | ad2antll 761 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦)) ∧ 𝑓:(ω ↑𝑜
2𝑜)–1-1-onto→ω)) → ((𝑓 ∘ (( I ↾ ((ω
↑𝑜 2𝑜) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅), ∅〉})):(ω
↑𝑜 2𝑜)–1-1-onto→ω ∧ ((𝑓 ∘ (( I ↾ ((ω
↑𝑜 2𝑜) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅),
∅〉}))‘∅) = ∅)) |
51 | 50 | simpld 474 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦)) ∧ 𝑓:(ω ↑𝑜
2𝑜)–1-1-onto→ω)) → (𝑓 ∘ (( I ↾ ((ω
↑𝑜 2𝑜) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅), ∅〉})):(ω
↑𝑜 2𝑜)–1-1-onto→ω) |
52 | 50 | simprd 478 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦)) ∧ 𝑓:(ω ↑𝑜
2𝑜)–1-1-onto→ω)) → ((𝑓 ∘ (( I ↾ ((ω
↑𝑜 2𝑜) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅),
∅〉}))‘∅) = ∅) |
53 | 21, 37, 41, 51, 52 | infxpenc2lem3 8727 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦)) ∧ 𝑓:(ω ↑𝑜
2𝑜)–1-1-onto→ω)) → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
54 | 53 | ex 449 |
. . . 4
⊢ (𝐴 ∈ On →
((∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦)) ∧ 𝑓:(ω ↑𝑜
2𝑜)–1-1-onto→ω) → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))) |
55 | 54 | exlimdvv 1849 |
. . 3
⊢ (𝐴 ∈ On → (∃𝑛∃𝑓(∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦)) ∧ 𝑓:(ω ↑𝑜
2𝑜)–1-1-onto→ω) → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))) |
56 | 20, 55 | syl5bir 232 |
. 2
⊢ (𝐴 ∈ On → ((∃𝑛∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1𝑜)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑𝑜 𝑦)) ∧ ∃𝑓 𝑓:(ω ↑𝑜
2𝑜)–1-1-onto→ω) → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))) |
57 | 1, 19, 56 | mp2and 711 |
1
⊢ (𝐴 ∈ On → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |