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 ⊢ 𝐴 ∈ V
rankxplim.2 ⊢ 𝐵 ∈ V
Assertion rankxplim3 ( Lim ( rank ‘ ( 𝐴 × 𝐵 ) ) ↔ Lim ∪ ( rank ‘ ( 𝐴 × 𝐵 ) ) )

Proof

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