Metamath Proof Explorer

Theorem onexoegt

Description: For any ordinal, there is always a larger power of omega. (Contributed by RP, 1-Feb-2025)

Ref Expression
Assertion onexoegt ( 𝐴 ∈ On → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ↑o 𝑥 ) )

Proof

Step Hyp Ref Expression
1 0elon ⊢ ∅ ∈ On
2 0lt1o ⊢ ∅ ∈ 1o
3 omelon ⊢ ω ∈ On
4 oe0 ⊢ ( ω ∈ On → ( ω ↑o ∅ ) = 1o )
5 3 4 ax-mp ⊢ ( ω ↑o ∅ ) = 1o
6 2 5 eleqtrri ⊢ ∅ ∈ ( ω ↑o ∅ )
7 6 a1i ⊢ ( 𝐴 = ∅ → ∅ ∈ ( ω ↑o ∅ ) )
8 oveq2 ⊢ ( 𝑥 = ∅ → ( ω ↑o 𝑥 ) = ( ω ↑o ∅ ) )
9 8 eleq2d ⊢ ( 𝑥 = ∅ → ( ∅ ∈ ( ω ↑o 𝑥 ) ↔ ∅ ∈ ( ω ↑o ∅ ) ) )
10 9 rspcev ⊢ ( ( ∅ ∈ On ∧ ∅ ∈ ( ω ↑o ∅ ) ) → ∃ 𝑥 ∈ On ∅ ∈ ( ω ↑o 𝑥 ) )
11 1 7 10 sylancr ⊢ ( 𝐴 = ∅ → ∃ 𝑥 ∈ On ∅ ∈ ( ω ↑o 𝑥 ) )
12 eleq1 ⊢ ( 𝐴 = ∅ → ( 𝐴 ∈ ( ω ↑o 𝑥 ) ↔ ∅ ∈ ( ω ↑o 𝑥 ) ) )
13 12 rexbidv ⊢ ( 𝐴 = ∅ → ( ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ↑o 𝑥 ) ↔ ∃ 𝑥 ∈ On ∅ ∈ ( ω ↑o 𝑥 ) ) )
14 11 13 mpbird ⊢ ( 𝐴 = ∅ → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ↑o 𝑥 ) )
15 14 a1i ⊢ ( 𝐴 ∈ On → ( 𝐴 = ∅ → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ↑o 𝑥 ) ) )
16 1onn ⊢ 1o ∈ ω
17 ondif2 ⊢ ( ω ∈ ( On ∖ 2o ) ↔ ( ω ∈ On ∧ 1o ∈ ω ) )
18 3 16 17 mpbir2an ⊢ ω ∈ ( On ∖ 2o )
19 ondif1 ⊢ ( 𝐴 ∈ ( On ∖ 1o ) ↔ ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) )
20 19 biimpri ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → 𝐴 ∈ ( On ∖ 1o ) )
21 oeeu ⊢ ( ( ω ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ ( On ∖ 1o ) ) → ∃! 𝑑 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ( ω ∖ 1o ) ∃ 𝑐 ∈ ( ω ↑o 𝑎 ) ( 𝑑 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 ) )
22 18 20 21 sylancr ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ∃! 𝑑 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ( ω ∖ 1o ) ∃ 𝑐 ∈ ( ω ↑o 𝑎 ) ( 𝑑 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 ) )
23 euex ⊢ ( ∃! 𝑑 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ( ω ∖ 1o ) ∃ 𝑐 ∈ ( ω ↑o 𝑎 ) ( 𝑑 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 ) → ∃ 𝑑 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ( ω ∖ 1o ) ∃ 𝑐 ∈ ( ω ↑o 𝑎 ) ( 𝑑 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 ) )
24 simpr ⊢ ( ( 𝑑 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 ) → ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 )
25 simp1 ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → 𝑎 ∈ On )
26 onsuc ⊢ ( 𝑎 ∈ On → suc 𝑎 ∈ On )
27 25 26 syl ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → suc 𝑎 ∈ On )
28 27 adantl ⊢ ( ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ∧ ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) ) → suc 𝑎 ∈ On )
29 simpr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) ∧ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 ) → ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 )
30 oecl ⊢ ( ( ω ∈ On ∧ 𝑎 ∈ On ) → ( ω ↑o 𝑎 ) ∈ On )
31 3 25 30 sylancr ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → ( ω ↑o 𝑎 ) ∈ On )
32 3 a1i ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → ω ∈ On )
33 omcl ⊢ ( ( ( ω ↑o 𝑎 ) ∈ On ∧ ω ∈ On ) → ( ( ω ↑o 𝑎 ) ·o ω ) ∈ On )
34 31 32 33 syl2anc ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → ( ( ω ↑o 𝑎 ) ·o ω ) ∈ On )
35 simp3 ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → 𝑐 ∈ ( ω ↑o 𝑎 ) )
36 eldifi ⊢ ( 𝑏 ∈ ( ω ∖ 1o ) → 𝑏 ∈ ω )
37 nnon ⊢ ( 𝑏 ∈ ω → 𝑏 ∈ On )
38 36 37 syl ⊢ ( 𝑏 ∈ ( ω ∖ 1o ) → 𝑏 ∈ On )
39 38 3ad2ant2 ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → 𝑏 ∈ On )
40 omcl ⊢ ( ( ( ω ↑o 𝑎 ) ∈ On ∧ 𝑏 ∈ On ) → ( ( ω ↑o 𝑎 ) ·o 𝑏 ) ∈ On )
41 31 39 40 syl2anc ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → ( ( ω ↑o 𝑎 ) ·o 𝑏 ) ∈ On )
42 oaordi ⊢ ( ( ( ω ↑o 𝑎 ) ∈ On ∧ ( ( ω ↑o 𝑎 ) ·o 𝑏 ) ∈ On ) → ( 𝑐 ∈ ( ω ↑o 𝑎 ) → ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) ∈ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o ( ω ↑o 𝑎 ) ) ) )
43 31 41 42 syl2anc ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → ( 𝑐 ∈ ( ω ↑o 𝑎 ) → ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) ∈ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o ( ω ↑o 𝑎 ) ) ) )
44 35 43 mpd ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) ∈ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o ( ω ↑o 𝑎 ) ) )
45 omsuc ⊢ ( ( ( ω ↑o 𝑎 ) ∈ On ∧ 𝑏 ∈ On ) → ( ( ω ↑o 𝑎 ) ·o suc 𝑏 ) = ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o ( ω ↑o 𝑎 ) ) )
46 31 39 45 syl2anc ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → ( ( ω ↑o 𝑎 ) ·o suc 𝑏 ) = ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o ( ω ↑o 𝑎 ) ) )
47 44 46 eleqtrrd ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) ∈ ( ( ω ↑o 𝑎 ) ·o suc 𝑏 ) )
48 36 3ad2ant2 ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → 𝑏 ∈ ω )
49 peano2 ⊢ ( 𝑏 ∈ ω → suc 𝑏 ∈ ω )
50 48 49 syl ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → suc 𝑏 ∈ ω )
51 peano1 ⊢ ∅ ∈ ω
52 51 a1i ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → ∅ ∈ ω )
53 oen0 ⊢ ( ( ( ω ∈ On ∧ 𝑎 ∈ On ) ∧ ∅ ∈ ω ) → ∅ ∈ ( ω ↑o 𝑎 ) )
54 32 25 52 53 syl21anc ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → ∅ ∈ ( ω ↑o 𝑎 ) )
55 omordi ⊢ ( ( ( ω ∈ On ∧ ( ω ↑o 𝑎 ) ∈ On ) ∧ ∅ ∈ ( ω ↑o 𝑎 ) ) → ( suc 𝑏 ∈ ω → ( ( ω ↑o 𝑎 ) ·o suc 𝑏 ) ∈ ( ( ω ↑o 𝑎 ) ·o ω ) ) )
56 32 31 54 55 syl21anc ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → ( suc 𝑏 ∈ ω → ( ( ω ↑o 𝑎 ) ·o suc 𝑏 ) ∈ ( ( ω ↑o 𝑎 ) ·o ω ) ) )
57 50 56 mpd ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → ( ( ω ↑o 𝑎 ) ·o suc 𝑏 ) ∈ ( ( ω ↑o 𝑎 ) ·o ω ) )
58 ontr1 ⊢ ( ( ( ω ↑o 𝑎 ) ·o ω ) ∈ On → ( ( ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) ∈ ( ( ω ↑o 𝑎 ) ·o suc 𝑏 ) ∧ ( ( ω ↑o 𝑎 ) ·o suc 𝑏 ) ∈ ( ( ω ↑o 𝑎 ) ·o ω ) ) → ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) ∈ ( ( ω ↑o 𝑎 ) ·o ω ) ) )
59 58 imp ⊢ ( ( ( ( ω ↑o 𝑎 ) ·o ω ) ∈ On ∧ ( ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) ∈ ( ( ω ↑o 𝑎 ) ·o suc 𝑏 ) ∧ ( ( ω ↑o 𝑎 ) ·o suc 𝑏 ) ∈ ( ( ω ↑o 𝑎 ) ·o ω ) ) ) → ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) ∈ ( ( ω ↑o 𝑎 ) ·o ω ) )
60 34 47 57 59 syl12anc ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) ∈ ( ( ω ↑o 𝑎 ) ·o ω ) )
61 oesuc ⊢ ( ( ω ∈ On ∧ 𝑎 ∈ On ) → ( ω ↑o suc 𝑎 ) = ( ( ω ↑o 𝑎 ) ·o ω ) )
62 3 25 61 sylancr ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → ( ω ↑o suc 𝑎 ) = ( ( ω ↑o 𝑎 ) ·o ω ) )
63 60 62 eleqtrrd ⊢ ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) ∈ ( ω ↑o suc 𝑎 ) )
64 63 adantr ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) ∧ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 ) → ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) ∈ ( ω ↑o suc 𝑎 ) )
65 29 64 eqeltrrd ⊢ ( ( ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) ∧ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 ) → 𝐴 ∈ ( ω ↑o suc 𝑎 ) )
66 65 adantll ⊢ ( ( ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ∧ ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) ) ∧ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 ) → 𝐴 ∈ ( ω ↑o suc 𝑎 ) )
67 oveq2 ⊢ ( 𝑥 = suc 𝑎 → ( ω ↑o 𝑥 ) = ( ω ↑o suc 𝑎 ) )
68 67 eleq2d ⊢ ( 𝑥 = suc 𝑎 → ( 𝐴 ∈ ( ω ↑o 𝑥 ) ↔ 𝐴 ∈ ( ω ↑o suc 𝑎 ) ) )
69 68 rspcev ⊢ ( ( suc 𝑎 ∈ On ∧ 𝐴 ∈ ( ω ↑o suc 𝑎 ) ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ↑o 𝑥 ) )
70 28 66 69 syl2an2r ⊢ ( ( ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ∧ ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) ) ∧ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ↑o 𝑥 ) )
71 70 ex ⊢ ( ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ∧ ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) ) → ( ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ↑o 𝑥 ) ) )
72 24 71 syl5 ⊢ ( ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ∧ ( 𝑎 ∈ On ∧ 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) ) → ( ( 𝑑 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ↑o 𝑥 ) ) )
73 72 3exp2 ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( 𝑎 ∈ On → ( 𝑏 ∈ ( ω ∖ 1o ) → ( 𝑐 ∈ ( ω ↑o 𝑎 ) → ( ( 𝑑 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) ) ) )
74 73 imp4b ⊢ ( ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ∧ 𝑎 ∈ On ) → ( ( 𝑏 ∈ ( ω ∖ 1o ) ∧ 𝑐 ∈ ( ω ↑o 𝑎 ) ) → ( ( 𝑑 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ↑o 𝑥 ) ) ) )
75 74 rexlimdvv ⊢ ( ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) ∧ 𝑎 ∈ On ) → ( ∃ 𝑏 ∈ ( ω ∖ 1o ) ∃ 𝑐 ∈ ( ω ↑o 𝑎 ) ( 𝑑 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ↑o 𝑥 ) ) )
76 75 rexlimdva ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ( ω ∖ 1o ) ∃ 𝑐 ∈ ( ω ↑o 𝑎 ) ( 𝑑 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ↑o 𝑥 ) ) )
77 76 exlimdv ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( ∃ 𝑑 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ( ω ∖ 1o ) ∃ 𝑐 ∈ ( ω ↑o 𝑎 ) ( 𝑑 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ↑o 𝑥 ) ) )
78 23 77 syl5 ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ( ∃! 𝑑 ∃ 𝑎 ∈ On ∃ 𝑏 ∈ ( ω ∖ 1o ) ∃ 𝑐 ∈ ( ω ↑o 𝑎 ) ( 𝑑 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ( ( ( ω ↑o 𝑎 ) ·o 𝑏 ) +o 𝑐 ) = 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ↑o 𝑥 ) ) )
79 22 78 mpd ⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ↑o 𝑥 ) )
80 79 ex ⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ↑o 𝑥 ) ) )
81 on0eqel ⊢ ( 𝐴 ∈ On → ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) )
82 15 80 81 mpjaod ⊢ ( 𝐴 ∈ On → ∃ 𝑥 ∈ On 𝐴 ∈ ( ω ↑o 𝑥 ) )