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 A <-> ( A = On \/ E. x e. ( On \ 1o ) A = ( _om .o x ) ) )

Proof

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