This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )