Metamath Proof Explorer


Theorem rankxpsuc

Description: The rank of a Cartesian product when the rank of the union of its arguments is a successor ordinal. Part of Exercise 4 of Kunen p. 107. See rankxplim for the limit ordinal case. (Contributed by NM, 19-Sep-2006)

Ref Expression
Hypotheses rankxplim.1
|- A e. _V
rankxplim.2
|- B e. _V
Assertion rankxpsuc
|- ( ( ( rank ` ( A u. B ) ) = suc C /\ ( A X. B ) =/= (/) ) -> ( rank ` ( A X. B ) ) = suc suc ( rank ` ( A u. B ) ) )

Proof

Step Hyp Ref Expression
1 rankxplim.1
 |-  A e. _V
2 rankxplim.2
 |-  B e. _V
3 unixp
 |-  ( ( A X. B ) =/= (/) -> U. U. ( A X. B ) = ( A u. B ) )
4 3 fveq2d
 |-  ( ( A X. B ) =/= (/) -> ( rank ` U. U. ( A X. B ) ) = ( rank ` ( A u. B ) ) )
5 rankuni
 |-  ( rank ` U. U. ( A X. B ) ) = U. ( rank ` U. ( A X. B ) )
6 rankuni
 |-  ( rank ` U. ( A X. B ) ) = U. ( rank ` ( A X. B ) )
7 6 unieqi
 |-  U. ( rank ` U. ( A X. B ) ) = U. U. ( rank ` ( A X. B ) )
8 5 7 eqtri
 |-  ( rank ` U. U. ( A X. B ) ) = U. U. ( rank ` ( A X. B ) )
9 4 8 eqtr3di
 |-  ( ( A X. B ) =/= (/) -> ( rank ` ( A u. B ) ) = U. U. ( rank ` ( A X. B ) ) )
10 suc11reg
 |-  ( suc ( rank ` ( A u. B ) ) = suc U. U. ( rank ` ( A X. B ) ) <-> ( rank ` ( A u. B ) ) = U. U. ( rank ` ( A X. B ) ) )
11 9 10 sylibr
 |-  ( ( A X. B ) =/= (/) -> suc ( rank ` ( A u. B ) ) = suc U. U. ( rank ` ( A X. B ) ) )
12 11 adantl
 |-  ( ( ( rank ` ( A u. B ) ) = suc C /\ ( A X. B ) =/= (/) ) -> suc ( rank ` ( A u. B ) ) = suc U. U. ( rank ` ( A X. B ) ) )
13 fvex
 |-  ( rank ` ( A u. B ) ) e. _V
14 eleq1
 |-  ( ( rank ` ( A u. B ) ) = suc C -> ( ( rank ` ( A u. B ) ) e. _V <-> suc C e. _V ) )
15 13 14 mpbii
 |-  ( ( rank ` ( A u. B ) ) = suc C -> suc C e. _V )
16 sucexb
 |-  ( C e. _V <-> suc C e. _V )
17 15 16 sylibr
 |-  ( ( rank ` ( A u. B ) ) = suc C -> C e. _V )
18 nlimsucg
 |-  ( C e. _V -> -. Lim suc C )
19 17 18 syl
 |-  ( ( rank ` ( A u. B ) ) = suc C -> -. Lim suc C )
20 limeq
 |-  ( ( rank ` ( A u. B ) ) = suc C -> ( Lim ( rank ` ( A u. B ) ) <-> Lim suc C ) )
21 19 20 mtbird
 |-  ( ( rank ` ( A u. B ) ) = suc C -> -. Lim ( rank ` ( A u. B ) ) )
22 1 2 rankxplim2
 |-  ( Lim ( rank ` ( A X. B ) ) -> Lim ( rank ` ( A u. B ) ) )
23 21 22 nsyl
 |-  ( ( rank ` ( A u. B ) ) = suc C -> -. Lim ( rank ` ( A X. B ) ) )
24 1 2 xpex
 |-  ( A X. B ) e. _V
25 24 rankeq0
 |-  ( ( A X. B ) = (/) <-> ( rank ` ( A X. B ) ) = (/) )
26 25 necon3abii
 |-  ( ( A X. B ) =/= (/) <-> -. ( rank ` ( A X. B ) ) = (/) )
27 rankon
 |-  ( rank ` ( A X. B ) ) e. On
28 27 onordi
 |-  Ord ( rank ` ( A X. B ) )
29 ordzsl
 |-  ( Ord ( rank ` ( A X. B ) ) <-> ( ( rank ` ( A X. B ) ) = (/) \/ E. x e. On ( rank ` ( A X. B ) ) = suc x \/ Lim ( rank ` ( A X. B ) ) ) )
30 28 29 mpbi
 |-  ( ( rank ` ( A X. B ) ) = (/) \/ E. x e. On ( rank ` ( A X. B ) ) = suc x \/ Lim ( rank ` ( A X. B ) ) )
31 3orass
 |-  ( ( ( rank ` ( A X. B ) ) = (/) \/ E. x e. On ( rank ` ( A X. B ) ) = suc x \/ Lim ( rank ` ( A X. B ) ) ) <-> ( ( rank ` ( A X. B ) ) = (/) \/ ( E. x e. On ( rank ` ( A X. B ) ) = suc x \/ Lim ( rank ` ( A X. B ) ) ) ) )
32 30 31 mpbi
 |-  ( ( rank ` ( A X. B ) ) = (/) \/ ( E. x e. On ( rank ` ( A X. B ) ) = suc x \/ Lim ( rank ` ( A X. B ) ) ) )
33 32 ori
 |-  ( -. ( rank ` ( A X. B ) ) = (/) -> ( E. x e. On ( rank ` ( A X. B ) ) = suc x \/ Lim ( rank ` ( A X. B ) ) ) )
34 26 33 sylbi
 |-  ( ( A X. B ) =/= (/) -> ( E. x e. On ( rank ` ( A X. B ) ) = suc x \/ Lim ( rank ` ( A X. B ) ) ) )
35 34 ord
 |-  ( ( A X. B ) =/= (/) -> ( -. E. x e. On ( rank ` ( A X. B ) ) = suc x -> Lim ( rank ` ( A X. B ) ) ) )
36 35 con1d
 |-  ( ( A X. B ) =/= (/) -> ( -. Lim ( rank ` ( A X. B ) ) -> E. x e. On ( rank ` ( A X. B ) ) = suc x ) )
37 23 36 syl5com
 |-  ( ( rank ` ( A u. B ) ) = suc C -> ( ( A X. B ) =/= (/) -> E. x e. On ( rank ` ( A X. B ) ) = suc x ) )
38 nlimsucg
 |-  ( x e. _V -> -. Lim suc x )
39 38 elv
 |-  -. Lim suc x
40 limeq
 |-  ( ( rank ` ( A X. B ) ) = suc x -> ( Lim ( rank ` ( A X. B ) ) <-> Lim suc x ) )
41 39 40 mtbiri
 |-  ( ( rank ` ( A X. B ) ) = suc x -> -. Lim ( rank ` ( A X. B ) ) )
42 41 rexlimivw
 |-  ( E. x e. On ( rank ` ( A X. B ) ) = suc x -> -. Lim ( rank ` ( A X. B ) ) )
43 1 2 rankxplim3
 |-  ( Lim ( rank ` ( A X. B ) ) <-> Lim U. ( rank ` ( A X. B ) ) )
44 42 43 sylnib
 |-  ( E. x e. On ( rank ` ( A X. B ) ) = suc x -> -. Lim U. ( rank ` ( A X. B ) ) )
45 37 44 syl6com
 |-  ( ( A X. B ) =/= (/) -> ( ( rank ` ( A u. B ) ) = suc C -> -. Lim U. ( rank ` ( A X. B ) ) ) )
46 unixp0
 |-  ( ( A X. B ) = (/) <-> U. ( A X. B ) = (/) )
47 24 uniex
 |-  U. ( A X. B ) e. _V
48 47 rankeq0
 |-  ( U. ( A X. B ) = (/) <-> ( rank ` U. ( A X. B ) ) = (/) )
49 6 eqeq1i
 |-  ( ( rank ` U. ( A X. B ) ) = (/) <-> U. ( rank ` ( A X. B ) ) = (/) )
50 46 48 49 3bitri
 |-  ( ( A X. B ) = (/) <-> U. ( rank ` ( A X. B ) ) = (/) )
51 50 necon3abii
 |-  ( ( A X. B ) =/= (/) <-> -. U. ( rank ` ( A X. B ) ) = (/) )
52 onuni
 |-  ( ( rank ` ( A X. B ) ) e. On -> U. ( rank ` ( A X. B ) ) e. On )
53 27 52 ax-mp
 |-  U. ( rank ` ( A X. B ) ) e. On
54 53 onordi
 |-  Ord U. ( rank ` ( A X. B ) )
55 ordzsl
 |-  ( Ord U. ( rank ` ( A X. B ) ) <-> ( U. ( rank ` ( A X. B ) ) = (/) \/ E. x e. On U. ( rank ` ( A X. B ) ) = suc x \/ Lim U. ( rank ` ( A X. B ) ) ) )
56 54 55 mpbi
 |-  ( U. ( rank ` ( A X. B ) ) = (/) \/ E. x e. On U. ( rank ` ( A X. B ) ) = suc x \/ Lim U. ( rank ` ( A X. B ) ) )
57 3orass
 |-  ( ( U. ( rank ` ( A X. B ) ) = (/) \/ E. x e. On U. ( rank ` ( A X. B ) ) = suc x \/ Lim U. ( rank ` ( A X. B ) ) ) <-> ( U. ( rank ` ( A X. B ) ) = (/) \/ ( E. x e. On U. ( rank ` ( A X. B ) ) = suc x \/ Lim U. ( rank ` ( A X. B ) ) ) ) )
58 56 57 mpbi
 |-  ( U. ( rank ` ( A X. B ) ) = (/) \/ ( E. x e. On U. ( rank ` ( A X. B ) ) = suc x \/ Lim U. ( rank ` ( A X. B ) ) ) )
59 58 ori
 |-  ( -. U. ( rank ` ( A X. B ) ) = (/) -> ( E. x e. On U. ( rank ` ( A X. B ) ) = suc x \/ Lim U. ( rank ` ( A X. B ) ) ) )
60 51 59 sylbi
 |-  ( ( A X. B ) =/= (/) -> ( E. x e. On U. ( rank ` ( A X. B ) ) = suc x \/ Lim U. ( rank ` ( A X. B ) ) ) )
61 60 ord
 |-  ( ( A X. B ) =/= (/) -> ( -. E. x e. On U. ( rank ` ( A X. B ) ) = suc x -> Lim U. ( rank ` ( A X. B ) ) ) )
62 61 con1d
 |-  ( ( A X. B ) =/= (/) -> ( -. Lim U. ( rank ` ( A X. B ) ) -> E. x e. On U. ( rank ` ( A X. B ) ) = suc x ) )
63 45 62 syld
 |-  ( ( A X. B ) =/= (/) -> ( ( rank ` ( A u. B ) ) = suc C -> E. x e. On U. ( rank ` ( A X. B ) ) = suc x ) )
64 63 impcom
 |-  ( ( ( rank ` ( A u. B ) ) = suc C /\ ( A X. B ) =/= (/) ) -> E. x e. On U. ( rank ` ( A X. B ) ) = suc x )
65 onsucuni2
 |-  ( ( U. ( rank ` ( A X. B ) ) e. On /\ U. ( rank ` ( A X. B ) ) = suc x ) -> suc U. U. ( rank ` ( A X. B ) ) = U. ( rank ` ( A X. B ) ) )
66 53 65 mpan
 |-  ( U. ( rank ` ( A X. B ) ) = suc x -> suc U. U. ( rank ` ( A X. B ) ) = U. ( rank ` ( A X. B ) ) )
67 66 rexlimivw
 |-  ( E. x e. On U. ( rank ` ( A X. B ) ) = suc x -> suc U. U. ( rank ` ( A X. B ) ) = U. ( rank ` ( A X. B ) ) )
68 64 67 syl
 |-  ( ( ( rank ` ( A u. B ) ) = suc C /\ ( A X. B ) =/= (/) ) -> suc U. U. ( rank ` ( A X. B ) ) = U. ( rank ` ( A X. B ) ) )
69 12 68 eqtrd
 |-  ( ( ( rank ` ( A u. B ) ) = suc C /\ ( A X. B ) =/= (/) ) -> suc ( rank ` ( A u. B ) ) = U. ( rank ` ( A X. B ) ) )
70 suc11reg
 |-  ( suc suc ( rank ` ( A u. B ) ) = suc U. ( rank ` ( A X. B ) ) <-> suc ( rank ` ( A u. B ) ) = U. ( rank ` ( A X. B ) ) )
71 69 70 sylibr
 |-  ( ( ( rank ` ( A u. B ) ) = suc C /\ ( A X. B ) =/= (/) ) -> suc suc ( rank ` ( A u. B ) ) = suc U. ( rank ` ( A X. B ) ) )
72 37 imp
 |-  ( ( ( rank ` ( A u. B ) ) = suc C /\ ( A X. B ) =/= (/) ) -> E. x e. On ( rank ` ( A X. B ) ) = suc x )
73 onsucuni2
 |-  ( ( ( rank ` ( A X. B ) ) e. On /\ ( rank ` ( A X. B ) ) = suc x ) -> suc U. ( rank ` ( A X. B ) ) = ( rank ` ( A X. B ) ) )
74 27 73 mpan
 |-  ( ( rank ` ( A X. B ) ) = suc x -> suc U. ( rank ` ( A X. B ) ) = ( rank ` ( A X. B ) ) )
75 74 rexlimivw
 |-  ( E. x e. On ( rank ` ( A X. B ) ) = suc x -> suc U. ( rank ` ( A X. B ) ) = ( rank ` ( A X. B ) ) )
76 72 75 syl
 |-  ( ( ( rank ` ( A u. B ) ) = suc C /\ ( A X. B ) =/= (/) ) -> suc U. ( rank ` ( A X. B ) ) = ( rank ` ( A X. B ) ) )
77 71 76 eqtr2d
 |-  ( ( ( rank ` ( A u. B ) ) = suc C /\ ( A X. B ) =/= (/) ) -> ( rank ` ( A X. B ) ) = suc suc ( rank ` ( A u. B ) ) )