Metamath Proof Explorer


Theorem rankxplim3

Description: The rank of a Cartesian product is a limit ordinal iff its union is. (Contributed by NM, 19-Sep-2006)

Ref Expression
Hypotheses rankxplim.1
|- A e. _V
rankxplim.2
|- B e. _V
Assertion rankxplim3
|- ( Lim ( rank ` ( A X. B ) ) <-> Lim U. ( rank ` ( A X. B ) ) )

Proof

Step Hyp Ref Expression
1 rankxplim.1
 |-  A e. _V
2 rankxplim.2
 |-  B e. _V
3 limuni2
 |-  ( Lim ( rank ` ( A X. B ) ) -> Lim U. ( rank ` ( A X. B ) ) )
4 0ellim
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> (/) e. U. ( rank ` ( A X. B ) ) )
5 n0i
 |-  ( (/) e. U. ( rank ` ( A X. B ) ) -> -. U. ( rank ` ( A X. B ) ) = (/) )
6 unieq
 |-  ( ( rank ` ( A X. B ) ) = (/) -> U. ( rank ` ( A X. B ) ) = U. (/) )
7 uni0
 |-  U. (/) = (/)
8 6 7 eqtrdi
 |-  ( ( rank ` ( A X. B ) ) = (/) -> U. ( rank ` ( A X. B ) ) = (/) )
9 8 con3i
 |-  ( -. U. ( rank ` ( A X. B ) ) = (/) -> -. ( rank ` ( A X. B ) ) = (/) )
10 4 5 9 3syl
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> -. ( rank ` ( A X. B ) ) = (/) )
11 rankon
 |-  ( rank ` ( A u. B ) ) e. On
12 11 onsuci
 |-  suc ( rank ` ( A u. B ) ) e. On
13 12 onsuci
 |-  suc suc ( rank ` ( A u. B ) ) e. On
14 13 elexi
 |-  suc suc ( rank ` ( A u. B ) ) e. _V
15 14 sucid
 |-  suc suc ( rank ` ( A u. B ) ) e. suc suc suc ( rank ` ( A u. B ) )
16 13 onsuci
 |-  suc suc suc ( rank ` ( A u. B ) ) e. On
17 ontri1
 |-  ( ( suc suc suc ( rank ` ( A u. B ) ) e. On /\ suc suc ( rank ` ( A u. B ) ) e. On ) -> ( suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) ) <-> -. suc suc ( rank ` ( A u. B ) ) e. suc suc suc ( rank ` ( A u. B ) ) ) )
18 16 13 17 mp2an
 |-  ( suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) ) <-> -. suc suc ( rank ` ( A u. B ) ) e. suc suc suc ( rank ` ( A u. B ) ) )
19 18 con2bii
 |-  ( suc suc ( rank ` ( A u. B ) ) e. suc suc suc ( rank ` ( A u. B ) ) <-> -. suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) ) )
20 15 19 mpbi
 |-  -. suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) )
21 1 2 rankxpu
 |-  ( rank ` ( A X. B ) ) C_ suc suc ( rank ` ( A u. B ) )
22 sstr
 |-  ( ( suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) /\ ( rank ` ( A X. B ) ) C_ suc suc ( rank ` ( A u. B ) ) ) -> suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) ) )
23 21 22 mpan2
 |-  ( suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) -> suc suc suc ( rank ` ( A u. B ) ) C_ suc suc ( rank ` ( A u. B ) ) )
24 20 23 mto
 |-  -. suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) )
25 reeanv
 |-  ( E. x e. On E. y e. On ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) <-> ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) )
26 simprl
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> ( rank ` ( A u. B ) ) = suc x )
27 simpr
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( rank ` ( A u. B ) ) = suc x ) -> ( rank ` ( A u. B ) ) = suc x )
28 df-ne
 |-  ( ( A X. B ) =/= (/) <-> -. ( A X. B ) = (/) )
29 1 2 xpex
 |-  ( A X. B ) e. _V
30 29 rankeq0
 |-  ( ( A X. B ) = (/) <-> ( rank ` ( A X. B ) ) = (/) )
31 30 notbii
 |-  ( -. ( A X. B ) = (/) <-> -. ( rank ` ( A X. B ) ) = (/) )
32 28 31 bitr2i
 |-  ( -. ( rank ` ( A X. B ) ) = (/) <-> ( A X. B ) =/= (/) )
33 10 32 sylib
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( A X. B ) =/= (/) )
34 unixp
 |-  ( ( A X. B ) =/= (/) -> U. U. ( A X. B ) = ( A u. B ) )
35 33 34 syl
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> U. U. ( A X. B ) = ( A u. B ) )
36 35 fveq2d
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( rank ` U. U. ( A X. B ) ) = ( rank ` ( A u. B ) ) )
37 rankuni
 |-  ( rank ` U. U. ( A X. B ) ) = U. ( rank ` U. ( A X. B ) )
38 rankuni
 |-  ( rank ` U. ( A X. B ) ) = U. ( rank ` ( A X. B ) )
39 38 unieqi
 |-  U. ( rank ` U. ( A X. B ) ) = U. U. ( rank ` ( A X. B ) )
40 37 39 eqtri
 |-  ( rank ` U. U. ( A X. B ) ) = U. U. ( rank ` ( A X. B ) )
41 36 40 eqtr3di
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( rank ` ( A u. B ) ) = U. U. ( rank ` ( A X. B ) ) )
42 eqimss
 |-  ( ( rank ` ( A u. B ) ) = U. U. ( rank ` ( A X. B ) ) -> ( rank ` ( A u. B ) ) C_ U. U. ( rank ` ( A X. B ) ) )
43 41 42 syl
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( rank ` ( A u. B ) ) C_ U. U. ( rank ` ( A X. B ) ) )
44 43 adantr
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( rank ` ( A u. B ) ) = suc x ) -> ( rank ` ( A u. B ) ) C_ U. U. ( rank ` ( A X. B ) ) )
45 27 44 eqsstrrd
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( rank ` ( A u. B ) ) = suc x ) -> suc x C_ U. U. ( rank ` ( A X. B ) ) )
46 45 adantrr
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc x C_ U. U. ( rank ` ( A X. B ) ) )
47 limuni
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> U. ( rank ` ( A X. B ) ) = U. U. ( rank ` ( A X. B ) ) )
48 47 adantr
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> U. ( rank ` ( A X. B ) ) = U. U. ( rank ` ( A X. B ) ) )
49 46 48 sseqtrrd
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc x C_ U. ( rank ` ( A X. B ) ) )
50 vex
 |-  x e. _V
51 rankon
 |-  ( rank ` ( A X. B ) ) e. On
52 51 onordi
 |-  Ord ( rank ` ( A X. B ) )
53 orduni
 |-  ( Ord ( rank ` ( A X. B ) ) -> Ord U. ( rank ` ( A X. B ) ) )
54 52 53 ax-mp
 |-  Ord U. ( rank ` ( A X. B ) )
55 ordelsuc
 |-  ( ( x e. _V /\ Ord U. ( rank ` ( A X. B ) ) ) -> ( x e. U. ( rank ` ( A X. B ) ) <-> suc x C_ U. ( rank ` ( A X. B ) ) ) )
56 50 54 55 mp2an
 |-  ( x e. U. ( rank ` ( A X. B ) ) <-> suc x C_ U. ( rank ` ( A X. B ) ) )
57 49 56 sylibr
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> x e. U. ( rank ` ( A X. B ) ) )
58 limsuc
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( x e. U. ( rank ` ( A X. B ) ) <-> suc x e. U. ( rank ` ( A X. B ) ) ) )
59 58 adantr
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> ( x e. U. ( rank ` ( A X. B ) ) <-> suc x e. U. ( rank ` ( A X. B ) ) ) )
60 57 59 mpbid
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc x e. U. ( rank ` ( A X. B ) ) )
61 26 60 eqeltrd
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) )
62 limsuc
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) <-> suc ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) ) )
63 62 adantr
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> ( ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) <-> suc ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) ) )
64 61 63 mpbid
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) )
65 ordsucelsuc
 |-  ( Ord U. ( rank ` ( A X. B ) ) -> ( suc ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) <-> suc suc ( rank ` ( A u. B ) ) e. suc U. ( rank ` ( A X. B ) ) ) )
66 54 65 ax-mp
 |-  ( suc ( rank ` ( A u. B ) ) e. U. ( rank ` ( A X. B ) ) <-> suc suc ( rank ` ( A u. B ) ) e. suc U. ( rank ` ( A X. B ) ) )
67 64 66 sylib
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc suc ( rank ` ( A u. B ) ) e. suc U. ( rank ` ( A X. B ) ) )
68 onsucuni2
 |-  ( ( ( rank ` ( A X. B ) ) e. On /\ ( rank ` ( A X. B ) ) = suc y ) -> suc U. ( rank ` ( A X. B ) ) = ( rank ` ( A X. B ) ) )
69 51 68 mpan
 |-  ( ( rank ` ( A X. B ) ) = suc y -> suc U. ( rank ` ( A X. B ) ) = ( rank ` ( A X. B ) ) )
70 69 ad2antll
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc U. ( rank ` ( A X. B ) ) = ( rank ` ( A X. B ) ) )
71 67 70 eleqtrd
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc suc ( rank ` ( A u. B ) ) e. ( rank ` ( A X. B ) ) )
72 13 51 onsucssi
 |-  ( suc suc ( rank ` ( A u. B ) ) e. ( rank ` ( A X. B ) ) <-> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) )
73 71 72 sylib
 |-  ( ( Lim U. ( rank ` ( A X. B ) ) /\ ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) ) -> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) )
74 73 ex
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) -> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) ) )
75 74 a1d
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( ( x e. On /\ y e. On ) -> ( ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) -> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) ) ) )
76 75 rexlimdvv
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( E. x e. On E. y e. On ( ( rank ` ( A u. B ) ) = suc x /\ ( rank ` ( A X. B ) ) = suc y ) -> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) ) )
77 25 76 syl5bir
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> ( ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) -> suc suc suc ( rank ` ( A u. B ) ) C_ ( rank ` ( A X. B ) ) ) )
78 24 77 mtoi
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) )
79 ianor
 |-  ( -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) <-> ( -. E. x e. On ( rank ` ( A u. B ) ) = suc x \/ -. E. y e. On ( rank ` ( A X. B ) ) = suc y ) )
80 un00
 |-  ( ( A = (/) /\ B = (/) ) <-> ( A u. B ) = (/) )
81 animorl
 |-  ( ( A = (/) /\ B = (/) ) -> ( A = (/) \/ B = (/) ) )
82 80 81 sylbir
 |-  ( ( A u. B ) = (/) -> ( A = (/) \/ B = (/) ) )
83 xpeq0
 |-  ( ( A X. B ) = (/) <-> ( A = (/) \/ B = (/) ) )
84 82 83 sylibr
 |-  ( ( A u. B ) = (/) -> ( A X. B ) = (/) )
85 84 con3i
 |-  ( -. ( A X. B ) = (/) -> -. ( A u. B ) = (/) )
86 31 85 sylbir
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> -. ( A u. B ) = (/) )
87 1 2 unex
 |-  ( A u. B ) e. _V
88 87 rankeq0
 |-  ( ( A u. B ) = (/) <-> ( rank ` ( A u. B ) ) = (/) )
89 88 notbii
 |-  ( -. ( A u. B ) = (/) <-> -. ( rank ` ( A u. B ) ) = (/) )
90 86 89 sylib
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> -. ( rank ` ( A u. B ) ) = (/) )
91 11 onordi
 |-  Ord ( rank ` ( A u. B ) )
92 ordzsl
 |-  ( Ord ( rank ` ( A u. B ) ) <-> ( ( rank ` ( A u. B ) ) = (/) \/ E. x e. On ( rank ` ( A u. B ) ) = suc x \/ Lim ( rank ` ( A u. B ) ) ) )
93 91 92 mpbi
 |-  ( ( rank ` ( A u. B ) ) = (/) \/ E. x e. On ( rank ` ( A u. B ) ) = suc x \/ Lim ( rank ` ( A u. B ) ) )
94 93 3ori
 |-  ( ( -. ( rank ` ( A u. B ) ) = (/) /\ -. E. x e. On ( rank ` ( A u. B ) ) = suc x ) -> Lim ( rank ` ( A u. B ) ) )
95 90 94 sylan
 |-  ( ( -. ( rank ` ( A X. B ) ) = (/) /\ -. E. x e. On ( rank ` ( A u. B ) ) = suc x ) -> Lim ( rank ` ( A u. B ) ) )
96 95 ex
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> ( -. E. x e. On ( rank ` ( A u. B ) ) = suc x -> Lim ( rank ` ( A u. B ) ) ) )
97 ordzsl
 |-  ( Ord ( rank ` ( A X. B ) ) <-> ( ( rank ` ( A X. B ) ) = (/) \/ E. y e. On ( rank ` ( A X. B ) ) = suc y \/ Lim ( rank ` ( A X. B ) ) ) )
98 52 97 mpbi
 |-  ( ( rank ` ( A X. B ) ) = (/) \/ E. y e. On ( rank ` ( A X. B ) ) = suc y \/ Lim ( rank ` ( A X. B ) ) )
99 98 3ori
 |-  ( ( -. ( rank ` ( A X. B ) ) = (/) /\ -. E. y e. On ( rank ` ( A X. B ) ) = suc y ) -> Lim ( rank ` ( A X. B ) ) )
100 99 ex
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> ( -. E. y e. On ( rank ` ( A X. B ) ) = suc y -> Lim ( rank ` ( A X. B ) ) ) )
101 96 100 orim12d
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> ( ( -. E. x e. On ( rank ` ( A u. B ) ) = suc x \/ -. E. y e. On ( rank ` ( A X. B ) ) = suc y ) -> ( Lim ( rank ` ( A u. B ) ) \/ Lim ( rank ` ( A X. B ) ) ) ) )
102 79 101 syl5bi
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> ( -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) -> ( Lim ( rank ` ( A u. B ) ) \/ Lim ( rank ` ( A X. B ) ) ) ) )
103 102 imp
 |-  ( ( -. ( rank ` ( A X. B ) ) = (/) /\ -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) ) -> ( Lim ( rank ` ( A u. B ) ) \/ Lim ( rank ` ( A X. B ) ) ) )
104 simpl
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ -. ( rank ` ( A X. B ) ) = (/) ) -> Lim ( rank ` ( A u. B ) ) )
105 30 necon3abii
 |-  ( ( A X. B ) =/= (/) <-> -. ( rank ` ( A X. B ) ) = (/) )
106 1 2 rankxplim
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ ( A X. B ) =/= (/) ) -> ( rank ` ( A X. B ) ) = ( rank ` ( A u. B ) ) )
107 105 106 sylan2br
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ -. ( rank ` ( A X. B ) ) = (/) ) -> ( rank ` ( A X. B ) ) = ( rank ` ( A u. B ) ) )
108 limeq
 |-  ( ( rank ` ( A X. B ) ) = ( rank ` ( A u. B ) ) -> ( Lim ( rank ` ( A X. B ) ) <-> Lim ( rank ` ( A u. B ) ) ) )
109 107 108 syl
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ -. ( rank ` ( A X. B ) ) = (/) ) -> ( Lim ( rank ` ( A X. B ) ) <-> Lim ( rank ` ( A u. B ) ) ) )
110 104 109 mpbird
 |-  ( ( Lim ( rank ` ( A u. B ) ) /\ -. ( rank ` ( A X. B ) ) = (/) ) -> Lim ( rank ` ( A X. B ) ) )
111 110 expcom
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> ( Lim ( rank ` ( A u. B ) ) -> Lim ( rank ` ( A X. B ) ) ) )
112 idd
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> ( Lim ( rank ` ( A X. B ) ) -> Lim ( rank ` ( A X. B ) ) ) )
113 111 112 jaod
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> ( ( Lim ( rank ` ( A u. B ) ) \/ Lim ( rank ` ( A X. B ) ) ) -> Lim ( rank ` ( A X. B ) ) ) )
114 113 adantr
 |-  ( ( -. ( rank ` ( A X. B ) ) = (/) /\ -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) ) -> ( ( Lim ( rank ` ( A u. B ) ) \/ Lim ( rank ` ( A X. B ) ) ) -> Lim ( rank ` ( A X. B ) ) ) )
115 103 114 mpd
 |-  ( ( -. ( rank ` ( A X. B ) ) = (/) /\ -. ( E. x e. On ( rank ` ( A u. B ) ) = suc x /\ E. y e. On ( rank ` ( A X. B ) ) = suc y ) ) -> Lim ( rank ` ( A X. B ) ) )
116 10 78 115 syl2anc
 |-  ( Lim U. ( rank ` ( A X. B ) ) -> Lim ( rank ` ( A X. B ) ) )
117 3 116 impbii
 |-  ( Lim ( rank ` ( A X. B ) ) <-> Lim U. ( rank ` ( A X. B ) ) )