Metamath Proof Explorer

Theorem nnoeomeqom

Description: Any natural number at least as large as two raised to the power of omega is omega. Lemma 3.25 of Schloeder p. 11. (Contributed by RP, 30-Jan-2025)

Ref Expression
Assertion nnoeomeqom ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → ( 𝐴 ↑o ω ) = ω )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → 𝐴 ∈ ω )
2 nnon ⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
3 1 2 syl ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → 𝐴 ∈ On )
4 omelon ⊢ ω ∈ On
5 limom ⊢ Lim ω
6 4 5 pm3.2i ⊢ ( ω ∈ On ∧ Lim ω )
7 6 a1i ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → ( ω ∈ On ∧ Lim ω ) )
8 0elon ⊢ ∅ ∈ On
9 8 a1i ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → ∅ ∈ On )
10 0ss ⊢ ∅ ⊆ 1o
11 10 a1i ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → ∅ ⊆ 1o )
12 simpr ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → 1o ∈ 𝐴 )
13 ontr2 ⊢ ( ( ∅ ∈ On ∧ 𝐴 ∈ On ) → ( ( ∅ ⊆ 1o ∧ 1o ∈ 𝐴 ) → ∅ ∈ 𝐴 ) )
14 13 imp ⊢ ( ( ( ∅ ∈ On ∧ 𝐴 ∈ On ) ∧ ( ∅ ⊆ 1o ∧ 1o ∈ 𝐴 ) ) → ∅ ∈ 𝐴 )
15 9 3 11 12 14 syl22anc ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → ∅ ∈ 𝐴 )
16 oelim ⊢ ( ( ( 𝐴 ∈ On ∧ ( ω ∈ On ∧ Lim ω ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o ω ) = ∪ 𝑥 ∈ ω ( 𝐴 ↑o 𝑥 ) )
17 3 7 15 16 syl21anc ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → ( 𝐴 ↑o ω ) = ∪ 𝑥 ∈ ω ( 𝐴 ↑o 𝑥 ) )
18 ovex ⊢ ( 𝐴 ↑o 𝑥 ) ∈ V
19 18 dfiun2 ⊢ ∪ 𝑥 ∈ ω ( 𝐴 ↑o 𝑥 ) = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ ω 𝑦 = ( 𝐴 ↑o 𝑥 ) }
20 eluniab ⊢ ( 𝑧 ∈ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ ω 𝑦 = ( 𝐴 ↑o 𝑥 ) } ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ ∃ 𝑥 ∈ ω 𝑦 = ( 𝐴 ↑o 𝑥 ) ) )
21 19.42v ⊢ ( ∃ 𝑥 ( 𝑧 ∈ 𝑦 ∧ ( 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ) ↔ ( 𝑧 ∈ 𝑦 ∧ ∃ 𝑥 ( 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ) )
22 3anass ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑦 ∧ ( 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ) )
23 22 exbii ⊢ ( ∃ 𝑥 ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ↔ ∃ 𝑥 ( 𝑧 ∈ 𝑦 ∧ ( 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ) )
24 df-rex ⊢ ( ∃ 𝑥 ∈ ω 𝑦 = ( 𝐴 ↑o 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) )
25 24 anbi2i ⊢ ( ( 𝑧 ∈ 𝑦 ∧ ∃ 𝑥 ∈ ω 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑦 ∧ ∃ 𝑥 ( 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ) )
26 21 23 25 3bitr4ri ⊢ ( ( 𝑧 ∈ 𝑦 ∧ ∃ 𝑥 ∈ ω 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ↔ ∃ 𝑥 ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) )
27 26 exbii ⊢ ( ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ ∃ 𝑥 ∈ ω 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ↔ ∃ 𝑦 ∃ 𝑥 ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) )
28 excom ⊢ ( ∃ 𝑦 ∃ 𝑥 ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) )
29 20 27 28 3bitri ⊢ ( 𝑧 ∈ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ ω 𝑦 = ( 𝐴 ↑o 𝑥 ) } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) )
30 simpr3 ⊢ ( ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ) → 𝑦 = ( 𝐴 ↑o 𝑥 ) )
31 simp2 ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) → 𝑥 ∈ ω )
32 nnecl ⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ ω ) → ( 𝐴 ↑o 𝑥 ) ∈ ω )
33 1 31 32 syl2an ⊢ ( ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ) → ( 𝐴 ↑o 𝑥 ) ∈ ω )
34 onelss ⊢ ( ω ∈ On → ( ( 𝐴 ↑o 𝑥 ) ∈ ω → ( 𝐴 ↑o 𝑥 ) ⊆ ω ) )
35 4 33 34 mpsyl ⊢ ( ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ) → ( 𝐴 ↑o 𝑥 ) ⊆ ω )
36 30 35 eqsstrd ⊢ ( ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ) → 𝑦 ⊆ ω )
37 simpr1 ⊢ ( ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ) → 𝑧 ∈ 𝑦 )
38 36 37 sseldd ⊢ ( ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ) → 𝑧 ∈ ω )
39 38 ex ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → ( ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) → 𝑧 ∈ ω ) )
40 39 exlimdvv ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) → 𝑧 ∈ ω ) )
41 peano2 ⊢ ( 𝑧 ∈ ω → suc 𝑧 ∈ ω )
42 41 adantl ⊢ ( ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) ∧ 𝑧 ∈ ω ) → suc 𝑧 ∈ ω )
43 ovex ⊢ ( 𝐴 ↑o suc 𝑧 ) ∈ V
44 43 a1i ⊢ ( ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) ∧ 𝑧 ∈ ω ) → ( 𝐴 ↑o suc 𝑧 ) ∈ V )
45 2 anim1i ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) )
46 ondif2 ⊢ ( 𝐴 ∈ ( On ∖ 2o ) ↔ ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) )
47 45 46 sylibr ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → 𝐴 ∈ ( On ∖ 2o ) )
48 nnon ⊢ ( suc 𝑧 ∈ ω → suc 𝑧 ∈ On )
49 41 48 syl ⊢ ( 𝑧 ∈ ω → suc 𝑧 ∈ On )
50 oeworde ⊢ ( ( 𝐴 ∈ ( On ∖ 2o ) ∧ suc 𝑧 ∈ On ) → suc 𝑧 ⊆ ( 𝐴 ↑o suc 𝑧 ) )
51 47 49 50 syl2an ⊢ ( ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) ∧ 𝑧 ∈ ω ) → suc 𝑧 ⊆ ( 𝐴 ↑o suc 𝑧 ) )
52 vex ⊢ 𝑧 ∈ V
53 52 sucid ⊢ 𝑧 ∈ suc 𝑧
54 53 a1i ⊢ ( ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) ∧ 𝑧 ∈ ω ) → 𝑧 ∈ suc 𝑧 )
55 51 54 sseldd ⊢ ( ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) ∧ 𝑧 ∈ ω ) → 𝑧 ∈ ( 𝐴 ↑o suc 𝑧 ) )
56 eqidd ⊢ ( ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) ∧ 𝑧 ∈ ω ) → ( 𝐴 ↑o suc 𝑧 ) = ( 𝐴 ↑o suc 𝑧 ) )
57 55 42 56 3jca ⊢ ( ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) ∧ 𝑧 ∈ ω ) → ( 𝑧 ∈ ( 𝐴 ↑o suc 𝑧 ) ∧ suc 𝑧 ∈ ω ∧ ( 𝐴 ↑o suc 𝑧 ) = ( 𝐴 ↑o suc 𝑧 ) ) )
58 eleq2 ⊢ ( 𝑦 = ( 𝐴 ↑o suc 𝑧 ) → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ ( 𝐴 ↑o suc 𝑧 ) ) )
59 eqeq1 ⊢ ( 𝑦 = ( 𝐴 ↑o suc 𝑧 ) → ( 𝑦 = ( 𝐴 ↑o suc 𝑧 ) ↔ ( 𝐴 ↑o suc 𝑧 ) = ( 𝐴 ↑o suc 𝑧 ) ) )
60 58 59 3anbi13d ⊢ ( 𝑦 = ( 𝐴 ↑o suc 𝑧 ) → ( ( 𝑧 ∈ 𝑦 ∧ suc 𝑧 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o suc 𝑧 ) ) ↔ ( 𝑧 ∈ ( 𝐴 ↑o suc 𝑧 ) ∧ suc 𝑧 ∈ ω ∧ ( 𝐴 ↑o suc 𝑧 ) = ( 𝐴 ↑o suc 𝑧 ) ) ) )
61 44 57 60 spcedv ⊢ ( ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) ∧ 𝑧 ∈ ω ) → ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ suc 𝑧 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o suc 𝑧 ) ) )
62 eleq1 ⊢ ( 𝑥 = suc 𝑧 → ( 𝑥 ∈ ω ↔ suc 𝑧 ∈ ω ) )
63 oveq2 ⊢ ( 𝑥 = suc 𝑧 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o suc 𝑧 ) )
64 63 eqeq2d ⊢ ( 𝑥 = suc 𝑧 → ( 𝑦 = ( 𝐴 ↑o 𝑥 ) ↔ 𝑦 = ( 𝐴 ↑o suc 𝑧 ) ) )
65 62 64 3anbi23d ⊢ ( 𝑥 = suc 𝑧 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑦 ∧ suc 𝑧 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o suc 𝑧 ) ) ) )
66 65 exbidv ⊢ ( 𝑥 = suc 𝑧 → ( ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ suc 𝑧 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o suc 𝑧 ) ) ) )
67 42 61 66 spcedv ⊢ ( ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) ∧ 𝑧 ∈ ω ) → ∃ 𝑥 ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) )
68 67 ex ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → ( 𝑧 ∈ ω → ∃ 𝑥 ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ) )
69 40 68 impbid ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑥 ∈ ω ∧ 𝑦 = ( 𝐴 ↑o 𝑥 ) ) ↔ 𝑧 ∈ ω ) )
70 29 69 bitrid ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → ( 𝑧 ∈ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ ω 𝑦 = ( 𝐴 ↑o 𝑥 ) } ↔ 𝑧 ∈ ω ) )
71 70 eqrdv ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → ∪ { 𝑦 ∣ ∃ 𝑥 ∈ ω 𝑦 = ( 𝐴 ↑o 𝑥 ) } = ω )
72 19 71 eqtrid ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → ∪ 𝑥 ∈ ω ( 𝐴 ↑o 𝑥 ) = ω )
73 17 72 eqtrd ⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ 𝐴 ) → ( 𝐴 ↑o ω ) = ω )