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 V
rankxplim.2 B V
Assertion rankxpsuc rank A B = suc C A × B rank A × B = suc suc rank A B

Proof

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