Metamath Proof Explorer

Theorem dflim5

Description: A limit ordinal is either the proper class of ordinals or some nonzero product with omega. (Contributed by RP, 8-Jan-2025)

Ref Expression
Assertion dflim5 ( Lim 𝐴 ↔ ( 𝐴 = On ∨ ∃ 𝑥 ∈ ( On ∖ 1o ) 𝐴 = ( ω ·o 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 limord ⊢ ( Lim 𝐴 → Ord 𝐴 )
2 ordeleqon ⊢ ( Ord 𝐴 ↔ ( 𝐴 ∈ On ∨ 𝐴 = On ) )
3 2 biimpi ⊢ ( Ord 𝐴 → ( 𝐴 ∈ On ∨ 𝐴 = On ) )
4 3 orcomd ⊢ ( Ord 𝐴 → ( 𝐴 = On ∨ 𝐴 ∈ On ) )
5 1 4 syl ⊢ ( Lim 𝐴 → ( 𝐴 = On ∨ 𝐴 ∈ On ) )
6 5 pm4.71ri ⊢ ( Lim 𝐴 ↔ ( ( 𝐴 = On ∨ 𝐴 ∈ On ) ∧ Lim 𝐴 ) )
7 andir ⊢ ( ( ( 𝐴 = On ∨ 𝐴 ∈ On ) ∧ Lim 𝐴 ) ↔ ( ( 𝐴 = On ∧ Lim 𝐴 ) ∨ ( 𝐴 ∈ On ∧ Lim 𝐴 ) ) )
8 6 7 bitri ⊢ ( Lim 𝐴 ↔ ( ( 𝐴 = On ∧ Lim 𝐴 ) ∨ ( 𝐴 ∈ On ∧ Lim 𝐴 ) ) )
9 limon ⊢ Lim On
10 limeq ⊢ ( 𝐴 = On → ( Lim 𝐴 ↔ Lim On ) )
11 9 10 mpbiri ⊢ ( 𝐴 = On → Lim 𝐴 )
12 11 pm4.71i ⊢ ( 𝐴 = On ↔ ( 𝐴 = On ∧ Lim 𝐴 ) )
13 12 orbi1i ⊢ ( ( 𝐴 = On ∨ ( 𝐴 ∈ On ∧ Lim 𝐴 ) ) ↔ ( ( 𝐴 = On ∧ Lim 𝐴 ) ∨ ( 𝐴 ∈ On ∧ Lim 𝐴 ) ) )
14 simpl ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → 𝐴 ∈ On )
15 omelon ⊢ ω ∈ On
16 15 a1i ⊢ ( 𝐴 ∈ On → ω ∈ On )
17 id ⊢ ( 𝐴 ∈ On → 𝐴 ∈ On )
18 peano1 ⊢ ∅ ∈ ω
19 18 ne0ii ⊢ ω ≠ ∅
20 19 a1i ⊢ ( 𝐴 ∈ On → ω ≠ ∅ )
21 16 17 20 3jca ⊢ ( 𝐴 ∈ On → ( ω ∈ On ∧ 𝐴 ∈ On ∧ ω ≠ ∅ ) )
22 omeulem1 ⊢ ( ( ω ∈ On ∧ 𝐴 ∈ On ∧ ω ≠ ∅ ) → ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ω ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 )
23 14 21 22 3syl ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ω ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 )
24 limeq ⊢ ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ( Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ↔ Lim 𝐴 ) )
25 24 biimprd ⊢ ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ( Lim 𝐴 → Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ) )
26 simplr ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ ∅ ∈ 𝑥 ) → 𝑦 ∈ ω )
27 nnlim ⊢ ( 𝑦 ∈ ω → ¬ Lim 𝑦 )
28 26 27 syl ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ ∅ ∈ 𝑥 ) → ¬ Lim 𝑦 )
29 on0eln0 ⊢ ( 𝑥 ∈ On → ( ∅ ∈ 𝑥 ↔ 𝑥 ≠ ∅ ) )
30 29 biimprd ⊢ ( 𝑥 ∈ On → ( 𝑥 ≠ ∅ → ∅ ∈ 𝑥 ) )
31 30 necon1bd ⊢ ( 𝑥 ∈ On → ( ¬ ∅ ∈ 𝑥 → 𝑥 = ∅ ) )
32 31 adantr ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ¬ ∅ ∈ 𝑥 → 𝑥 = ∅ ) )
33 32 imp ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ ∅ ∈ 𝑥 ) → 𝑥 = ∅ )
34 33 26 jca ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ ∅ ∈ 𝑥 ) → ( 𝑥 = ∅ ∧ 𝑦 ∈ ω ) )
35 simpl ⊢ ( ( 𝑥 = ∅ ∧ 𝑦 ∈ ω ) → 𝑥 = ∅ )
36 35 oveq2d ⊢ ( ( 𝑥 = ∅ ∧ 𝑦 ∈ ω ) → ( ω ·o 𝑥 ) = ( ω ·o ∅ ) )
37 om0 ⊢ ( ω ∈ On → ( ω ·o ∅ ) = ∅ )
38 15 37 mp1i ⊢ ( ( 𝑥 = ∅ ∧ 𝑦 ∈ ω ) → ( ω ·o ∅ ) = ∅ )
39 36 38 eqtrd ⊢ ( ( 𝑥 = ∅ ∧ 𝑦 ∈ ω ) → ( ω ·o 𝑥 ) = ∅ )
40 39 oveq1d ⊢ ( ( 𝑥 = ∅ ∧ 𝑦 ∈ ω ) → ( ( ω ·o 𝑥 ) +o 𝑦 ) = ( ∅ +o 𝑦 ) )
41 nna0r ⊢ ( 𝑦 ∈ ω → ( ∅ +o 𝑦 ) = 𝑦 )
42 41 adantl ⊢ ( ( 𝑥 = ∅ ∧ 𝑦 ∈ ω ) → ( ∅ +o 𝑦 ) = 𝑦 )
43 40 42 eqtrd ⊢ ( ( 𝑥 = ∅ ∧ 𝑦 ∈ ω ) → ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝑦 )
44 limeq ⊢ ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝑦 → ( Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ↔ Lim 𝑦 ) )
45 34 43 44 3syl ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ ∅ ∈ 𝑥 ) → ( Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ↔ Lim 𝑦 ) )
46 28 45 mtbird ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ ∅ ∈ 𝑥 ) → ¬ Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) )
47 46 ex ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ¬ ∅ ∈ 𝑥 → ¬ Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ) )
48 ovex ⊢ ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) ∈ V
49 nlimsucg ⊢ ( ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) ∈ V → ¬ Lim suc ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) )
50 48 49 mp1i ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → ¬ Lim suc ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) )
51 nnord ⊢ ( 𝑦 ∈ ω → Ord 𝑦 )
52 orduniorsuc ⊢ ( Ord 𝑦 → ( 𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦 ) )
53 51 52 syl ⊢ ( 𝑦 ∈ ω → ( 𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦 ) )
54 3ianor ⊢ ( ¬ ( Ord 𝑦 ∧ 𝑦 ≠ ∅ ∧ 𝑦 = ∪ 𝑦 ) ↔ ( ¬ Ord 𝑦 ∨ ¬ 𝑦 ≠ ∅ ∨ ¬ 𝑦 = ∪ 𝑦 ) )
55 df-lim ⊢ ( Lim 𝑦 ↔ ( Ord 𝑦 ∧ 𝑦 ≠ ∅ ∧ 𝑦 = ∪ 𝑦 ) )
56 54 55 xchnxbir ⊢ ( ¬ Lim 𝑦 ↔ ( ¬ Ord 𝑦 ∨ ¬ 𝑦 ≠ ∅ ∨ ¬ 𝑦 = ∪ 𝑦 ) )
57 27 56 sylib ⊢ ( 𝑦 ∈ ω → ( ¬ Ord 𝑦 ∨ ¬ 𝑦 ≠ ∅ ∨ ¬ 𝑦 = ∪ 𝑦 ) )
58 51 pm2.24d ⊢ ( 𝑦 ∈ ω → ( ¬ Ord 𝑦 → ( 𝑦 = ∪ 𝑦 → 𝑦 = ∅ ) ) )
59 nne ⊢ ( ¬ 𝑦 ≠ ∅ ↔ 𝑦 = ∅ )
60 59 biimpi ⊢ ( ¬ 𝑦 ≠ ∅ → 𝑦 = ∅ )
61 60 a1i13 ⊢ ( 𝑦 ∈ ω → ( ¬ 𝑦 ≠ ∅ → ( 𝑦 = ∪ 𝑦 → 𝑦 = ∅ ) ) )
62 pm2.21 ⊢ ( ¬ 𝑦 = ∪ 𝑦 → ( 𝑦 = ∪ 𝑦 → 𝑦 = ∅ ) )
63 62 a1i ⊢ ( 𝑦 ∈ ω → ( ¬ 𝑦 = ∪ 𝑦 → ( 𝑦 = ∪ 𝑦 → 𝑦 = ∅ ) ) )
64 58 61 63 3jaod ⊢ ( 𝑦 ∈ ω → ( ( ¬ Ord 𝑦 ∨ ¬ 𝑦 ≠ ∅ ∨ ¬ 𝑦 = ∪ 𝑦 ) → ( 𝑦 = ∪ 𝑦 → 𝑦 = ∅ ) ) )
65 57 64 mpd ⊢ ( 𝑦 ∈ ω → ( 𝑦 = ∪ 𝑦 → 𝑦 = ∅ ) )
66 65 orim1d ⊢ ( 𝑦 ∈ ω → ( ( 𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦 ) → ( 𝑦 = ∅ ∨ 𝑦 = suc ∪ 𝑦 ) ) )
67 53 66 mpd ⊢ ( 𝑦 ∈ ω → ( 𝑦 = ∅ ∨ 𝑦 = suc ∪ 𝑦 ) )
68 67 ord ⊢ ( 𝑦 ∈ ω → ( ¬ 𝑦 = ∅ → 𝑦 = suc ∪ 𝑦 ) )
69 68 adantl ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ¬ 𝑦 = ∅ → 𝑦 = suc ∪ 𝑦 ) )
70 69 imp ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → 𝑦 = suc ∪ 𝑦 )
71 70 oveq2d ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → ( ( ω ·o 𝑥 ) +o 𝑦 ) = ( ( ω ·o 𝑥 ) +o suc ∪ 𝑦 ) )
72 simpl ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → 𝑥 ∈ On )
73 72 adantr ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → 𝑥 ∈ On )
74 omcl ⊢ ( ( ω ∈ On ∧ 𝑥 ∈ On ) → ( ω ·o 𝑥 ) ∈ On )
75 15 73 74 sylancr ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → ( ω ·o 𝑥 ) ∈ On )
76 nnon ⊢ ( 𝑦 ∈ ω → 𝑦 ∈ On )
77 onuni ⊢ ( 𝑦 ∈ On → ∪ 𝑦 ∈ On )
78 76 77 syl ⊢ ( 𝑦 ∈ ω → ∪ 𝑦 ∈ On )
79 78 adantl ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ∪ 𝑦 ∈ On )
80 79 adantr ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → ∪ 𝑦 ∈ On )
81 oasuc ⊢ ( ( ( ω ·o 𝑥 ) ∈ On ∧ ∪ 𝑦 ∈ On ) → ( ( ω ·o 𝑥 ) +o suc ∪ 𝑦 ) = suc ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) )
82 75 80 81 syl2anc ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → ( ( ω ·o 𝑥 ) +o suc ∪ 𝑦 ) = suc ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) )
83 71 82 eqtrd ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → ( ( ω ·o 𝑥 ) +o 𝑦 ) = suc ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) )
84 limeq ⊢ ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = suc ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) → ( Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ↔ Lim suc ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) ) )
85 83 84 syl ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → ( Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ↔ Lim suc ( ( ω ·o 𝑥 ) +o ∪ 𝑦 ) ) )
86 50 85 mtbird ⊢ ( ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ¬ 𝑦 = ∅ ) → ¬ Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) )
87 86 ex ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ¬ 𝑦 = ∅ → ¬ Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ) )
88 47 87 jaod ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ( ¬ ∅ ∈ 𝑥 ∨ ¬ 𝑦 = ∅ ) → ¬ Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) ) )
89 88 con2d ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) → ¬ ( ¬ ∅ ∈ 𝑥 ∨ ¬ 𝑦 = ∅ ) ) )
90 anor ⊢ ( ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ↔ ¬ ( ¬ ∅ ∈ 𝑥 ∨ ¬ 𝑦 = ∅ ) )
91 89 90 imbitrrdi ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( Lim ( ( ω ·o 𝑥 ) +o 𝑦 ) → ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) )
92 25 91 syl9 ⊢ ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( Lim 𝐴 → ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) ) )
93 92 com13 ⊢ ( Lim 𝐴 → ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) ) )
94 93 adantl ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) ) )
95 94 3imp ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) → ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) )
96 simp2 ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) → ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) )
97 96 72 syl ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) → 𝑥 ∈ On )
98 simpl ⊢ ( ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) → ∅ ∈ 𝑥 )
99 97 98 anim12i ⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) ∧ ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) → ( 𝑥 ∈ On ∧ ∅ ∈ 𝑥 ) )
100 ondif1 ⊢ ( 𝑥 ∈ ( On ∖ 1o ) ↔ ( 𝑥 ∈ On ∧ ∅ ∈ 𝑥 ) )
101 99 100 sylibr ⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) ∧ ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) → 𝑥 ∈ ( On ∖ 1o ) )
102 simpr ⊢ ( ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) → 𝑦 = ∅ )
103 102 oveq2d ⊢ ( ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) → ( ( ω ·o 𝑥 ) +o 𝑦 ) = ( ( ω ·o 𝑥 ) +o ∅ ) )
104 103 adantl ⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) ∧ ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) → ( ( ω ·o 𝑥 ) +o 𝑦 ) = ( ( ω ·o 𝑥 ) +o ∅ ) )
105 simpl3 ⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) ∧ ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) → ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 )
106 15 72 74 sylancr ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ω ·o 𝑥 ) ∈ On )
107 oa0 ⊢ ( ( ω ·o 𝑥 ) ∈ On → ( ( ω ·o 𝑥 ) +o ∅ ) = ( ω ·o 𝑥 ) )
108 96 106 107 3syl ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) → ( ( ω ·o 𝑥 ) +o ∅ ) = ( ω ·o 𝑥 ) )
109 108 adantr ⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) ∧ ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) → ( ( ω ·o 𝑥 ) +o ∅ ) = ( ω ·o 𝑥 ) )
110 104 105 109 3eqtr3d ⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) ∧ ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) → 𝐴 = ( ω ·o 𝑥 ) )
111 101 110 jca ⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) ∧ ( ∅ ∈ 𝑥 ∧ 𝑦 = ∅ ) ) → ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) )
112 95 111 mpdan ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) ∧ ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) → ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) )
113 112 3exp ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ( ( 𝑥 ∈ On ∧ 𝑦 ∈ ω ) → ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) ) ) )
114 113 expdimp ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ 𝑥 ∈ On ) → ( 𝑦 ∈ ω → ( ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) ) ) )
115 114 rexlimdv ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ∧ 𝑥 ∈ On ) → ( ∃ 𝑦 ∈ ω ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) ) )
116 115 expimpd ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ( ( 𝑥 ∈ On ∧ ∃ 𝑦 ∈ ω ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 ) → ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) ) )
117 116 reximdv2 ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ω ( ( ω ·o 𝑥 ) +o 𝑦 ) = 𝐴 → ∃ 𝑥 ∈ ( On ∖ 1o ) 𝐴 = ( ω ·o 𝑥 ) ) )
118 23 117 mpd ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) → ∃ 𝑥 ∈ ( On ∖ 1o ) 𝐴 = ( ω ·o 𝑥 ) )
119 simpr ⊢ ( ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) → 𝐴 = ( ω ·o 𝑥 ) )
120 eldifi ⊢ ( 𝑥 ∈ ( On ∖ 1o ) → 𝑥 ∈ On )
121 15 120 74 sylancr ⊢ ( 𝑥 ∈ ( On ∖ 1o ) → ( ω ·o 𝑥 ) ∈ On )
122 121 adantr ⊢ ( ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) → ( ω ·o 𝑥 ) ∈ On )
123 119 122 eqeltrd ⊢ ( ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) → 𝐴 ∈ On )
124 limom ⊢ Lim ω
125 15 124 pm3.2i ⊢ ( ω ∈ On ∧ Lim ω )
126 omlimcl2 ⊢ ( ( ( 𝑥 ∈ On ∧ ( ω ∈ On ∧ Lim ω ) ) ∧ ∅ ∈ 𝑥 ) → Lim ( ω ·o 𝑥 ) )
127 125 126 mpanl2 ⊢ ( ( 𝑥 ∈ On ∧ ∅ ∈ 𝑥 ) → Lim ( ω ·o 𝑥 ) )
128 100 127 sylbi ⊢ ( 𝑥 ∈ ( On ∖ 1o ) → Lim ( ω ·o 𝑥 ) )
129 128 adantr ⊢ ( ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) → Lim ( ω ·o 𝑥 ) )
130 limeq ⊢ ( 𝐴 = ( ω ·o 𝑥 ) → ( Lim 𝐴 ↔ Lim ( ω ·o 𝑥 ) ) )
131 130 adantl ⊢ ( ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) → ( Lim 𝐴 ↔ Lim ( ω ·o 𝑥 ) ) )
132 129 131 mpbird ⊢ ( ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) → Lim 𝐴 )
133 123 132 jca ⊢ ( ( 𝑥 ∈ ( On ∖ 1o ) ∧ 𝐴 = ( ω ·o 𝑥 ) ) → ( 𝐴 ∈ On ∧ Lim 𝐴 ) )
134 133 rexlimiva ⊢ ( ∃ 𝑥 ∈ ( On ∖ 1o ) 𝐴 = ( ω ·o 𝑥 ) → ( 𝐴 ∈ On ∧ Lim 𝐴 ) )
135 118 134 impbii ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝐴 ) ↔ ∃ 𝑥 ∈ ( On ∖ 1o ) 𝐴 = ( ω ·o 𝑥 ) )
136 135 orbi2i ⊢ ( ( 𝐴 = On ∨ ( 𝐴 ∈ On ∧ Lim 𝐴 ) ) ↔ ( 𝐴 = On ∨ ∃ 𝑥 ∈ ( On ∖ 1o ) 𝐴 = ( ω ·o 𝑥 ) ) )
137 8 13 136 3bitr2i ⊢ ( Lim 𝐴 ↔ ( 𝐴 = On ∨ ∃ 𝑥 ∈ ( On ∖ 1o ) 𝐴 = ( ω ·o 𝑥 ) ) )