Step | Hyp | Ref
| Expression |
1 | | cnfcom3c 9171 |
. 2
⊢ (𝐴 ∈ On → ∃𝑛∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦))) |
2 | | df-2o 8105 |
. . . . . . . 8
⊢
2o = suc 1o |
3 | 2 | oveq2i 7169 |
. . . . . . 7
⊢ (ω
↑o 2o) = (ω ↑o suc
1o) |
4 | | omelon 9111 |
. . . . . . . 8
⊢ ω
∈ On |
5 | | 1on 8111 |
. . . . . . . 8
⊢
1o ∈ On |
6 | | oesuc 8154 |
. . . . . . . 8
⊢ ((ω
∈ On ∧ 1o ∈ On) → (ω ↑o suc
1o) = ((ω ↑o 1o)
·o ω)) |
7 | 4, 5, 6 | mp2an 690 |
. . . . . . 7
⊢ (ω
↑o suc 1o) = ((ω ↑o
1o) ·o ω) |
8 | | oe1 8172 |
. . . . . . . . 9
⊢ (ω
∈ On → (ω ↑o 1o) =
ω) |
9 | 4, 8 | ax-mp 5 |
. . . . . . . 8
⊢ (ω
↑o 1o) = ω |
10 | 9 | oveq1i 7168 |
. . . . . . 7
⊢ ((ω
↑o 1o) ·o ω) = (ω
·o ω) |
11 | 3, 7, 10 | 3eqtri 2850 |
. . . . . 6
⊢ (ω
↑o 2o) = (ω ·o
ω) |
12 | | omxpen 8621 |
. . . . . . 7
⊢ ((ω
∈ On ∧ ω ∈ On) → (ω ·o
ω) ≈ (ω × ω)) |
13 | 4, 4, 12 | mp2an 690 |
. . . . . 6
⊢ (ω
·o ω) ≈ (ω ×
ω) |
14 | 11, 13 | eqbrtri 5089 |
. . . . 5
⊢ (ω
↑o 2o) ≈ (ω ×
ω) |
15 | | xpomen 9443 |
. . . . 5
⊢ (ω
× ω) ≈ ω |
16 | 14, 15 | entri 8565 |
. . . 4
⊢ (ω
↑o 2o) ≈ ω |
17 | 16 | a1i 11 |
. . 3
⊢ (𝐴 ∈ On → (ω
↑o 2o) ≈ ω) |
18 | | bren 8520 |
. . 3
⊢ ((ω
↑o 2o) ≈ ω ↔ ∃𝑓 𝑓:(ω ↑o
2o)–1-1-onto→ω) |
19 | 17, 18 | sylib 220 |
. 2
⊢ (𝐴 ∈ On → ∃𝑓 𝑓:(ω ↑o
2o)–1-1-onto→ω) |
20 | | exdistrv 1956 |
. . 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 485 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω)) → 𝐴 ∈ On) |
22 | | simprl 769 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω)) → ∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦))) |
23 | | sseq2 3995 |
. . . . . . . . 9
⊢ (𝑥 = 𝑏 → (ω ⊆ 𝑥 ↔ ω ⊆ 𝑏)) |
24 | | oveq2 7166 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (ω ↑o 𝑦) = (ω ↑o
𝑤)) |
25 | 24 | f1oeq3d 6614 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → ((𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦) ↔ (𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑤))) |
26 | 25 | cbvrexvw 3452 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈ (On
∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦) ↔ ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑤)) |
27 | | fveq2 6672 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑏 → (𝑛‘𝑥) = (𝑛‘𝑏)) |
28 | | f1oeq1 6606 |
. . . . . . . . . . . . 13
⊢ ((𝑛‘𝑥) = (𝑛‘𝑏) → ((𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑤) ↔ (𝑛‘𝑏):𝑥–1-1-onto→(ω ↑o 𝑤))) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑏 → ((𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑤) ↔ (𝑛‘𝑏):𝑥–1-1-onto→(ω ↑o 𝑤))) |
30 | | f1oeq2 6607 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑏 → ((𝑛‘𝑏):𝑥–1-1-onto→(ω ↑o 𝑤) ↔ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
31 | 29, 30 | bitrd 281 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑏 → ((𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑤) ↔ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
32 | 31 | rexbidv 3299 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑏 → (∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑤) ↔ ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
33 | 26, 32 | syl5bb 285 |
. . . . . . . . 9
⊢ (𝑥 = 𝑏 → (∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦) ↔ ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
34 | 23, 33 | imbi12d 347 |
. . . . . . . 8
⊢ (𝑥 = 𝑏 → ((ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ↔ (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)))) |
35 | 34 | cbvralvw 3451 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ↔ ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
36 | 22, 35 | sylib 220 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω)) → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
37 | | oveq2 7166 |
. . . . . . . . 9
⊢ (𝑏 = 𝑧 → (ω ↑o 𝑏) = (ω ↑o
𝑧)) |
38 | 37 | cbvmptv 5171 |
. . . . . . . 8
⊢ (𝑏 ∈ (On ∖
1o) ↦ (ω ↑o 𝑏)) = (𝑧 ∈ (On ∖ 1o) ↦
(ω ↑o 𝑧)) |
39 | 38 | cnveqi 5747 |
. . . . . . 7
⊢ ◡(𝑏 ∈ (On ∖ 1o) ↦
(ω ↑o 𝑏)) = ◡(𝑧 ∈ (On ∖ 1o) ↦
(ω ↑o 𝑧)) |
40 | 39 | fveq1i 6673 |
. . . . . 6
⊢ (◡(𝑏 ∈ (On ∖ 1o) ↦
(ω ↑o 𝑏))‘ran (𝑛‘𝑏)) = (◡(𝑧 ∈ (On ∖ 1o) ↦
(ω ↑o 𝑧))‘ran (𝑛‘𝑏)) |
41 | | 2on 8113 |
. . . . . . . . . 10
⊢
2o ∈ On |
42 | | peano1 7603 |
. . . . . . . . . . 11
⊢ ∅
∈ ω |
43 | | oen0 8214 |
. . . . . . . . . . 11
⊢
(((ω ∈ On ∧ 2o ∈ On) ∧ ∅ ∈
ω) → ∅ ∈ (ω ↑o
2o)) |
44 | 42, 43 | mpan2 689 |
. . . . . . . . . 10
⊢ ((ω
∈ On ∧ 2o ∈ On) → ∅ ∈ (ω
↑o 2o)) |
45 | 4, 41, 44 | mp2an 690 |
. . . . . . . . 9
⊢ ∅
∈ (ω ↑o 2o) |
46 | | eqid 2823 |
. . . . . . . . . 10
⊢ (𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅), ∅〉})) = (𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅),
∅〉})) |
47 | 46 | fveqf1o 7060 |
. . . . . . . . 9
⊢ ((𝑓:(ω ↑o
2o)–1-1-onto→ω ∧ ∅ ∈ (ω
↑o 2o) ∧ ∅ ∈ ω) → ((𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅), ∅〉})):(ω
↑o 2o)–1-1-onto→ω ∧ ((𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅),
∅〉}))‘∅) = ∅)) |
48 | 45, 42, 47 | mp3an23 1449 |
. . . . . . . 8
⊢ (𝑓:(ω ↑o
2o)–1-1-onto→ω → ((𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅), ∅〉})):(ω
↑o 2o)–1-1-onto→ω ∧ ((𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅),
∅〉}))‘∅) = ∅)) |
49 | 48 | ad2antll 727 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω)) → ((𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅), ∅〉})):(ω
↑o 2o)–1-1-onto→ω ∧ ((𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅),
∅〉}))‘∅) = ∅)) |
50 | 49 | simpld 497 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω)) → (𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅), ∅〉})):(ω
↑o 2o)–1-1-onto→ω) |
51 | 49 | simprd 498 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω)) → ((𝑓 ∘ (( I ↾ ((ω
↑o 2o) ∖ {∅, (◡𝑓‘∅)})) ∪ {〈∅,
(◡𝑓‘∅)〉, 〈(◡𝑓‘∅),
∅〉}))‘∅) = ∅) |
52 | 21, 36, 40, 50, 51 | infxpenc2lem3 9449 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ (∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω)) → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
53 | 52 | ex 415 |
. . . 4
⊢ (𝐴 ∈ On →
((∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖
1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω) → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))) |
54 | 53 | exlimdvv 1935 |
. . 3
⊢ (𝐴 ∈ On → (∃𝑛∃𝑓(∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ 𝑓:(ω ↑o
2o)–1-1-onto→ω) → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))) |
55 | 20, 54 | syl5bir 245 |
. 2
⊢ (𝐴 ∈ On → ((∃𝑛∀𝑥 ∈ 𝐴 (ω ⊆ 𝑥 → ∃𝑦 ∈ (On ∖ 1o)(𝑛‘𝑥):𝑥–1-1-onto→(ω ↑o 𝑦)) ∧ ∃𝑓 𝑓:(ω ↑o
2o)–1-1-onto→ω) → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))) |
56 | 1, 19, 55 | mp2and 697 |
1
⊢ (𝐴 ∈ On → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |