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 ⊢ 𝐴 ∈ V
rankxplim.2 ⊢ 𝐵 ∈ V
Assertion rankxpsuc ( ( ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) = suc 𝐶 ∧ ( 𝐴 × 𝐵 ) ≠ ∅ ) → ( rank ‘ ( 𝐴 × 𝐵 ) ) = suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) )

Proof

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