Step |
Hyp |
Ref |
Expression |
1 |
|
cnfcom3c |
⊢ ( 𝐴 ∈ On → ∃ 𝑛 ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ) |
2 |
|
df-2o |
⊢ 2o = suc 1o |
3 |
2
|
oveq2i |
⊢ ( ω ↑o 2o ) = ( ω ↑o suc 1o ) |
4 |
|
omelon |
⊢ ω ∈ On |
5 |
|
1on |
⊢ 1o ∈ On |
6 |
|
oesuc |
⊢ ( ( ω ∈ On ∧ 1o ∈ On ) → ( ω ↑o suc 1o ) = ( ( ω ↑o 1o ) ·o ω ) ) |
7 |
4 5 6
|
mp2an |
⊢ ( ω ↑o suc 1o ) = ( ( ω ↑o 1o ) ·o ω ) |
8 |
|
oe1 |
⊢ ( ω ∈ On → ( ω ↑o 1o ) = ω ) |
9 |
4 8
|
ax-mp |
⊢ ( ω ↑o 1o ) = ω |
10 |
9
|
oveq1i |
⊢ ( ( ω ↑o 1o ) ·o ω ) = ( ω ·o ω ) |
11 |
3 7 10
|
3eqtri |
⊢ ( ω ↑o 2o ) = ( ω ·o ω ) |
12 |
|
omxpen |
⊢ ( ( ω ∈ On ∧ ω ∈ On ) → ( ω ·o ω ) ≈ ( ω × ω ) ) |
13 |
4 4 12
|
mp2an |
⊢ ( ω ·o ω ) ≈ ( ω × ω ) |
14 |
11 13
|
eqbrtri |
⊢ ( ω ↑o 2o ) ≈ ( ω × ω ) |
15 |
|
xpomen |
⊢ ( ω × ω ) ≈ ω |
16 |
14 15
|
entri |
⊢ ( ω ↑o 2o ) ≈ ω |
17 |
16
|
a1i |
⊢ ( 𝐴 ∈ On → ( ω ↑o 2o ) ≈ ω ) |
18 |
|
bren |
⊢ ( ( ω ↑o 2o ) ≈ ω ↔ ∃ 𝑓 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) |
19 |
17 18
|
sylib |
⊢ ( 𝐴 ∈ On → ∃ 𝑓 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) |
20 |
|
exdistrv |
⊢ ( ∃ 𝑛 ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ↔ ( ∃ 𝑛 ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ ∃ 𝑓 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) |
21 |
|
simpl |
⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → 𝐴 ∈ On ) |
22 |
|
simprl |
⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ) |
23 |
|
sseq2 |
⊢ ( 𝑥 = 𝑏 → ( ω ⊆ 𝑥 ↔ ω ⊆ 𝑏 ) ) |
24 |
|
oveq2 |
⊢ ( 𝑦 = 𝑤 → ( ω ↑o 𝑦 ) = ( ω ↑o 𝑤 ) ) |
25 |
24
|
f1oeq3d |
⊢ ( 𝑦 = 𝑤 → ( ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ↔ ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) |
26 |
25
|
cbvrexvw |
⊢ ( ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ↔ ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ) |
27 |
|
fveq2 |
⊢ ( 𝑥 = 𝑏 → ( 𝑛 ‘ 𝑥 ) = ( 𝑛 ‘ 𝑏 ) ) |
28 |
27
|
f1oeq1d |
⊢ ( 𝑥 = 𝑏 → ( ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ↔ ( 𝑛 ‘ 𝑏 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) |
29 |
|
f1oeq2 |
⊢ ( 𝑥 = 𝑏 → ( ( 𝑛 ‘ 𝑏 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ↔ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) |
30 |
28 29
|
bitrd |
⊢ ( 𝑥 = 𝑏 → ( ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ↔ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) |
31 |
30
|
rexbidv |
⊢ ( 𝑥 = 𝑏 → ( ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ↔ ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) |
32 |
26 31
|
syl5bb |
⊢ ( 𝑥 = 𝑏 → ( ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ↔ ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) |
33 |
23 32
|
imbi12d |
⊢ ( 𝑥 = 𝑏 → ( ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ↔ ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) ) |
34 |
33
|
cbvralvw |
⊢ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ↔ ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) |
35 |
22 34
|
sylib |
⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) |
36 |
|
oveq2 |
⊢ ( 𝑏 = 𝑧 → ( ω ↑o 𝑏 ) = ( ω ↑o 𝑧 ) ) |
37 |
36
|
cbvmptv |
⊢ ( 𝑏 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑏 ) ) = ( 𝑧 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑧 ) ) |
38 |
37
|
cnveqi |
⊢ ◡ ( 𝑏 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑏 ) ) = ◡ ( 𝑧 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑧 ) ) |
39 |
38
|
fveq1i |
⊢ ( ◡ ( 𝑏 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑏 ) ) ‘ ran ( 𝑛 ‘ 𝑏 ) ) = ( ◡ ( 𝑧 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑧 ) ) ‘ ran ( 𝑛 ‘ 𝑏 ) ) |
40 |
|
2on |
⊢ 2o ∈ On |
41 |
|
peano1 |
⊢ ∅ ∈ ω |
42 |
|
oen0 |
⊢ ( ( ( ω ∈ On ∧ 2o ∈ On ) ∧ ∅ ∈ ω ) → ∅ ∈ ( ω ↑o 2o ) ) |
43 |
41 42
|
mpan2 |
⊢ ( ( ω ∈ On ∧ 2o ∈ On ) → ∅ ∈ ( ω ↑o 2o ) ) |
44 |
4 40 43
|
mp2an |
⊢ ∅ ∈ ( ω ↑o 2o ) |
45 |
|
eqid |
⊢ ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { 〈 ∅ , ( ◡ 𝑓 ‘ ∅ ) 〉 , 〈 ( ◡ 𝑓 ‘ ∅ ) , ∅ 〉 } ) ) = ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { 〈 ∅ , ( ◡ 𝑓 ‘ ∅ ) 〉 , 〈 ( ◡ 𝑓 ‘ ∅ ) , ∅ 〉 } ) ) |
46 |
45
|
fveqf1o |
⊢ ( ( 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ∧ ∅ ∈ ( ω ↑o 2o ) ∧ ∅ ∈ ω ) → ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { 〈 ∅ , ( ◡ 𝑓 ‘ ∅ ) 〉 , 〈 ( ◡ 𝑓 ‘ ∅ ) , ∅ 〉 } ) ) : ( ω ↑o 2o ) –1-1-onto→ ω ∧ ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { 〈 ∅ , ( ◡ 𝑓 ‘ ∅ ) 〉 , 〈 ( ◡ 𝑓 ‘ ∅ ) , ∅ 〉 } ) ) ‘ ∅ ) = ∅ ) ) |
47 |
44 41 46
|
mp3an23 |
⊢ ( 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω → ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { 〈 ∅ , ( ◡ 𝑓 ‘ ∅ ) 〉 , 〈 ( ◡ 𝑓 ‘ ∅ ) , ∅ 〉 } ) ) : ( ω ↑o 2o ) –1-1-onto→ ω ∧ ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { 〈 ∅ , ( ◡ 𝑓 ‘ ∅ ) 〉 , 〈 ( ◡ 𝑓 ‘ ∅ ) , ∅ 〉 } ) ) ‘ ∅ ) = ∅ ) ) |
48 |
47
|
ad2antll |
⊢ ( ( 𝐴 ∈ 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 |
⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { 〈 ∅ , ( ◡ 𝑓 ‘ ∅ ) 〉 , 〈 ( ◡ 𝑓 ‘ ∅ ) , ∅ 〉 } ) ) : ( ω ↑o 2o ) –1-1-onto→ ω ) |
50 |
48
|
simprd |
⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { 〈 ∅ , ( ◡ 𝑓 ‘ ∅ ) 〉 , 〈 ( ◡ 𝑓 ‘ ∅ ) , ∅ 〉 } ) ) ‘ ∅ ) = ∅ ) |
51 |
21 35 39 49 50
|
infxpenc2lem3 |
⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) |
52 |
51
|
ex |
⊢ ( 𝐴 ∈ On → ( ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) ) |
53 |
52
|
exlimdvv |
⊢ ( 𝐴 ∈ On → ( ∃ 𝑛 ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) ) |
54 |
20 53
|
syl5bir |
⊢ ( 𝐴 ∈ On → ( ( ∃ 𝑛 ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ ∃ 𝑓 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) ) |
55 |
1 19 54
|
mp2and |
⊢ ( 𝐴 ∈ On → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) |