MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rankxplim3 Structured version   Visualization version   GIF version

Theorem rankxplim3 9817
Description: The rank of a Cartesian product is a limit ordinal iff its union is. (Contributed by NM, 19-Sep-2006.)
Hypotheses
Ref Expression
rankxplim.1 𝐴 ∈ V
rankxplim.2 𝐵 ∈ V
Assertion
Ref Expression
rankxplim3 (Lim (rank‘(𝐴 × 𝐵)) ↔ Lim (rank‘(𝐴 × 𝐵)))

Proof of Theorem rankxplim3
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limuni2 6379 . 2 (Lim (rank‘(𝐴 × 𝐵)) → Lim (rank‘(𝐴 × 𝐵)))
2 0ellim 6380 . . . 4 (Lim (rank‘(𝐴 × 𝐵)) → ∅ ∈ (rank‘(𝐴 × 𝐵)))
3 n0i 4293 . . . 4 (∅ ∈ (rank‘(𝐴 × 𝐵)) → ¬ (rank‘(𝐴 × 𝐵)) = ∅)
4 unieq 4876 . . . . . 6 ((rank‘(𝐴 × 𝐵)) = ∅ → (rank‘(𝐴 × 𝐵)) = ∅)
5 uni0 4896 . . . . . 6 ∅ = ∅
64, 5eqtrdi 2792 . . . . 5 ((rank‘(𝐴 × 𝐵)) = ∅ → (rank‘(𝐴 × 𝐵)) = ∅)
76con3i 154 . . . 4 (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (rank‘(𝐴 × 𝐵)) = ∅)
82, 3, 73syl 18 . . 3 (Lim (rank‘(𝐴 × 𝐵)) → ¬ (rank‘(𝐴 × 𝐵)) = ∅)
9 rankon 9731 . . . . . . . . . 10 (rank‘(𝐴𝐵)) ∈ On
109onsuci 7774 . . . . . . . . 9 suc (rank‘(𝐴𝐵)) ∈ On
1110onsuci 7774 . . . . . . . 8 suc suc (rank‘(𝐴𝐵)) ∈ On
1211elexi 3464 . . . . . . 7 suc suc (rank‘(𝐴𝐵)) ∈ V
1312sucid 6399 . . . . . 6 suc suc (rank‘(𝐴𝐵)) ∈ suc suc suc (rank‘(𝐴𝐵))
1411onsuci 7774 . . . . . . . 8 suc suc suc (rank‘(𝐴𝐵)) ∈ On
15 ontri1 6351 . . . . . . . 8 ((suc suc suc (rank‘(𝐴𝐵)) ∈ On ∧ suc suc (rank‘(𝐴𝐵)) ∈ On) → (suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵)) ↔ ¬ suc suc (rank‘(𝐴𝐵)) ∈ suc suc suc (rank‘(𝐴𝐵))))
1614, 11, 15mp2an 690 . . . . . . 7 (suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵)) ↔ ¬ suc suc (rank‘(𝐴𝐵)) ∈ suc suc suc (rank‘(𝐴𝐵)))
1716con2bii 357 . . . . . 6 (suc suc (rank‘(𝐴𝐵)) ∈ suc suc suc (rank‘(𝐴𝐵)) ↔ ¬ suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵)))
1813, 17mpbi 229 . . . . 5 ¬ suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵))
19 rankxplim.1 . . . . . . 7 𝐴 ∈ V
20 rankxplim.2 . . . . . . 7 𝐵 ∈ V
2119, 20rankxpu 9812 . . . . . 6 (rank‘(𝐴 × 𝐵)) ⊆ suc suc (rank‘(𝐴𝐵))
22 sstr 3952 . . . . . 6 ((suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴 × 𝐵)) ⊆ suc suc (rank‘(𝐴𝐵))) → suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵)))
2321, 22mpan2 689 . . . . 5 (suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)) → suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵)))
2418, 23mto 196 . . . 4 ¬ suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵))
25 reeanv 3217 . . . . 5 (∃𝑥 ∈ On ∃𝑦 ∈ On ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) ↔ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦))
26 simprl 769 . . . . . . . . . . . . 13 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴𝐵)) = suc 𝑥)
27 simpr 485 . . . . . . . . . . . . . . . . . 18 ((Lim (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴𝐵)) = suc 𝑥) → (rank‘(𝐴𝐵)) = suc 𝑥)
28 df-ne 2944 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 × 𝐵) ≠ ∅ ↔ ¬ (𝐴 × 𝐵) = ∅)
2919, 20xpex 7687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 × 𝐵) ∈ V
3029rankeq0 9797 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 × 𝐵) = ∅ ↔ (rank‘(𝐴 × 𝐵)) = ∅)
3130notbii 319 . . . . . . . . . . . . . . . . . . . . . . . . 25 (¬ (𝐴 × 𝐵) = ∅ ↔ ¬ (rank‘(𝐴 × 𝐵)) = ∅)
3228, 31bitr2i 275 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (rank‘(𝐴 × 𝐵)) = ∅ ↔ (𝐴 × 𝐵) ≠ ∅)
338, 32sylib 217 . . . . . . . . . . . . . . . . . . . . . . 23 (Lim (rank‘(𝐴 × 𝐵)) → (𝐴 × 𝐵) ≠ ∅)
34 unixp 6234 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 × 𝐵) ≠ ∅ → (𝐴 × 𝐵) = (𝐴𝐵))
3533, 34syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (Lim (rank‘(𝐴 × 𝐵)) → (𝐴 × 𝐵) = (𝐴𝐵))
3635fveq2d 6846 . . . . . . . . . . . . . . . . . . . . 21 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴𝐵)))
37 rankuni 9799 . . . . . . . . . . . . . . . . . . . . . 22 (rank‘ (𝐴 × 𝐵)) = (rank‘ (𝐴 × 𝐵))
38 rankuni 9799 . . . . . . . . . . . . . . . . . . . . . . 23 (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))
3938unieqi 4878 . . . . . . . . . . . . . . . . . . . . . 22 (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))
4037, 39eqtri 2764 . . . . . . . . . . . . . . . . . . . . 21 (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))
4136, 40eqtr3di 2791 . . . . . . . . . . . . . . . . . . . 20 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴𝐵)) = (rank‘(𝐴 × 𝐵)))
42 eqimss 4000 . . . . . . . . . . . . . . . . . . . 20 ((rank‘(𝐴𝐵)) = (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
4341, 42syl 17 . . . . . . . . . . . . . . . . . . 19 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
4443adantr 481 . . . . . . . . . . . . . . . . . 18 ((Lim (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴𝐵)) = suc 𝑥) → (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
4527, 44eqsstrrd 3983 . . . . . . . . . . . . . . . . 17 ((Lim (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴𝐵)) = suc 𝑥) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
4645adantrr 715 . . . . . . . . . . . . . . . 16 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
47 limuni 6378 . . . . . . . . . . . . . . . . 17 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
4847adantr 481 . . . . . . . . . . . . . . . 16 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
4946, 48sseqtrrd 3985 . . . . . . . . . . . . . . 15 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
50 vex 3449 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
51 rankon 9731 . . . . . . . . . . . . . . . . . 18 (rank‘(𝐴 × 𝐵)) ∈ On
5251onordi 6428 . . . . . . . . . . . . . . . . 17 Ord (rank‘(𝐴 × 𝐵))
53 orduni 7724 . . . . . . . . . . . . . . . . 17 (Ord (rank‘(𝐴 × 𝐵)) → Ord (rank‘(𝐴 × 𝐵)))
5452, 53ax-mp 5 . . . . . . . . . . . . . . . 16 Ord (rank‘(𝐴 × 𝐵))
55 ordelsuc 7755 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ V ∧ Ord (rank‘(𝐴 × 𝐵))) → (𝑥 (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 (rank‘(𝐴 × 𝐵))))
5650, 54, 55mp2an 690 . . . . . . . . . . . . . . 15 (𝑥 (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 (rank‘(𝐴 × 𝐵)))
5749, 56sylibr 233 . . . . . . . . . . . . . 14 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → 𝑥 (rank‘(𝐴 × 𝐵)))
58 limsuc 7785 . . . . . . . . . . . . . . 15 (Lim (rank‘(𝐴 × 𝐵)) → (𝑥 (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 (rank‘(𝐴 × 𝐵))))
5958adantr 481 . . . . . . . . . . . . . 14 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (𝑥 (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 (rank‘(𝐴 × 𝐵))))
6057, 59mpbid 231 . . . . . . . . . . . . 13 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
6126, 60eqeltrd 2838 . . . . . . . . . . . 12 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)))
62 limsuc 7785 . . . . . . . . . . . . 13 (Lim (rank‘(𝐴 × 𝐵)) → ((rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)) ↔ suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵))))
6362adantr 481 . . . . . . . . . . . 12 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → ((rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)) ↔ suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵))))
6461, 63mpbid 231 . . . . . . . . . . 11 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)))
65 ordsucelsuc 7757 . . . . . . . . . . . 12 (Ord (rank‘(𝐴 × 𝐵)) → (suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)) ↔ suc suc (rank‘(𝐴𝐵)) ∈ suc (rank‘(𝐴 × 𝐵))))
6654, 65ax-mp 5 . . . . . . . . . . 11 (suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)) ↔ suc suc (rank‘(𝐴𝐵)) ∈ suc (rank‘(𝐴 × 𝐵)))
6764, 66sylib 217 . . . . . . . . . 10 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc (rank‘(𝐴𝐵)) ∈ suc (rank‘(𝐴 × 𝐵)))
68 onsucuni2 7769 . . . . . . . . . . . 12 (((rank‘(𝐴 × 𝐵)) ∈ On ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
6951, 68mpan 688 . . . . . . . . . . 11 ((rank‘(𝐴 × 𝐵)) = suc 𝑦 → suc (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
7069ad2antll 727 . . . . . . . . . 10 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
7167, 70eleqtrd 2840 . . . . . . . . 9 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)))
7211, 51onsucssi 7777 . . . . . . . . 9 (suc suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)) ↔ suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
7371, 72sylib 217 . . . . . . . 8 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
7473ex 413 . . . . . . 7 (Lim (rank‘(𝐴 × 𝐵)) → (((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵))))
7574a1d 25 . . . . . 6 (Lim (rank‘(𝐴 × 𝐵)) → ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))))
7675rexlimdvv 3204 . . . . 5 (Lim (rank‘(𝐴 × 𝐵)) → (∃𝑥 ∈ On ∃𝑦 ∈ On ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵))))
7725, 76biimtrrid 242 . . . 4 (Lim (rank‘(𝐴 × 𝐵)) → ((∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵))))
7824, 77mtoi 198 . . 3 (Lim (rank‘(𝐴 × 𝐵)) → ¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦))
79 ianor 980 . . . . . 6 (¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) ↔ (¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∨ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦))
80 un00 4402 . . . . . . . . . . . . . 14 ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴𝐵) = ∅)
81 animorl 976 . . . . . . . . . . . . . 14 ((𝐴 = ∅ ∧ 𝐵 = ∅) → (𝐴 = ∅ ∨ 𝐵 = ∅))
8280, 81sylbir 234 . . . . . . . . . . . . 13 ((𝐴𝐵) = ∅ → (𝐴 = ∅ ∨ 𝐵 = ∅))
83 xpeq0 6112 . . . . . . . . . . . . 13 ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))
8482, 83sylibr 233 . . . . . . . . . . . 12 ((𝐴𝐵) = ∅ → (𝐴 × 𝐵) = ∅)
8584con3i 154 . . . . . . . . . . 11 (¬ (𝐴 × 𝐵) = ∅ → ¬ (𝐴𝐵) = ∅)
8631, 85sylbir 234 . . . . . . . . . 10 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (𝐴𝐵) = ∅)
8719, 20unex 7680 . . . . . . . . . . . 12 (𝐴𝐵) ∈ V
8887rankeq0 9797 . . . . . . . . . . 11 ((𝐴𝐵) = ∅ ↔ (rank‘(𝐴𝐵)) = ∅)
8988notbii 319 . . . . . . . . . 10 (¬ (𝐴𝐵) = ∅ ↔ ¬ (rank‘(𝐴𝐵)) = ∅)
9086, 89sylib 217 . . . . . . . . 9 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (rank‘(𝐴𝐵)) = ∅)
919onordi 6428 . . . . . . . . . . 11 Ord (rank‘(𝐴𝐵))
92 ordzsl 7781 . . . . . . . . . . 11 (Ord (rank‘(𝐴𝐵)) ↔ ((rank‘(𝐴𝐵)) = ∅ ∨ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴𝐵))))
9391, 92mpbi 229 . . . . . . . . . 10 ((rank‘(𝐴𝐵)) = ∅ ∨ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴𝐵)))
94933ori 1424 . . . . . . . . 9 ((¬ (rank‘(𝐴𝐵)) = ∅ ∧ ¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥) → Lim (rank‘(𝐴𝐵)))
9590, 94sylan 580 . . . . . . . 8 ((¬ (rank‘(𝐴 × 𝐵)) = ∅ ∧ ¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥) → Lim (rank‘(𝐴𝐵)))
9695ex 413 . . . . . . 7 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 → Lim (rank‘(𝐴𝐵))))
97 ordzsl 7781 . . . . . . . . . 10 (Ord (rank‘(𝐴 × 𝐵)) ↔ ((rank‘(𝐴 × 𝐵)) = ∅ ∨ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦 ∨ Lim (rank‘(𝐴 × 𝐵))))
9852, 97mpbi 229 . . . . . . . . 9 ((rank‘(𝐴 × 𝐵)) = ∅ ∨ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦 ∨ Lim (rank‘(𝐴 × 𝐵)))
99983ori 1424 . . . . . . . 8 ((¬ (rank‘(𝐴 × 𝐵)) = ∅ ∧ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → Lim (rank‘(𝐴 × 𝐵)))
10099ex 413 . . . . . . 7 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦 → Lim (rank‘(𝐴 × 𝐵))))
10196, 100orim12d 963 . . . . . 6 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ((¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∨ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → (Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵)))))
10279, 101biimtrid 241 . . . . 5 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → (Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵)))))
103102imp 407 . . . 4 ((¬ (rank‘(𝐴 × 𝐵)) = ∅ ∧ ¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))))
104 simpl 483 . . . . . . . 8 ((Lim (rank‘(𝐴𝐵)) ∧ ¬ (rank‘(𝐴 × 𝐵)) = ∅) → Lim (rank‘(𝐴𝐵)))
10530necon3abii 2990 . . . . . . . . . 10 ((𝐴 × 𝐵) ≠ ∅ ↔ ¬ (rank‘(𝐴 × 𝐵)) = ∅)
10619, 20rankxplim 9815 . . . . . . . . . 10 ((Lim (rank‘(𝐴𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴𝐵)))
107105, 106sylan2br 595 . . . . . . . . 9 ((Lim (rank‘(𝐴𝐵)) ∧ ¬ (rank‘(𝐴 × 𝐵)) = ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴𝐵)))
108 limeq 6329 . . . . . . . . 9 ((rank‘(𝐴 × 𝐵)) = (rank‘(𝐴𝐵)) → (Lim (rank‘(𝐴 × 𝐵)) ↔ Lim (rank‘(𝐴𝐵))))
109107, 108syl 17 . . . . . . . 8 ((Lim (rank‘(𝐴𝐵)) ∧ ¬ (rank‘(𝐴 × 𝐵)) = ∅) → (Lim (rank‘(𝐴 × 𝐵)) ↔ Lim (rank‘(𝐴𝐵))))
110104, 109mpbird 256 . . . . . . 7 ((Lim (rank‘(𝐴𝐵)) ∧ ¬ (rank‘(𝐴 × 𝐵)) = ∅) → Lim (rank‘(𝐴 × 𝐵)))
111110expcom 414 . . . . . 6 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (Lim (rank‘(𝐴𝐵)) → Lim (rank‘(𝐴 × 𝐵))))
112 idd 24 . . . . . 6 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (Lim (rank‘(𝐴 × 𝐵)) → Lim (rank‘(𝐴 × 𝐵))))
113111, 112jaod 857 . . . . 5 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ((Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))) → Lim (rank‘(𝐴 × 𝐵))))
114113adantr 481 . . . 4 ((¬ (rank‘(𝐴 × 𝐵)) = ∅ ∧ ¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → ((Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))) → Lim (rank‘(𝐴 × 𝐵))))
115103, 114mpd 15 . . 3 ((¬ (rank‘(𝐴 × 𝐵)) = ∅ ∧ ¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → Lim (rank‘(𝐴 × 𝐵)))
1168, 78, 115syl2anc 584 . 2 (Lim (rank‘(𝐴 × 𝐵)) → Lim (rank‘(𝐴 × 𝐵)))
1171, 116impbii 208 1 (Lim (rank‘(𝐴 × 𝐵)) ↔ Lim (rank‘(𝐴 × 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3o 1086   = wceq 1541  wcel 2106  wne 2943  wrex 3073  Vcvv 3445  cun 3908  wss 3910  c0 4282   cuni 4865   × cxp 5631  Ord word 6316  Oncon0 6317  Lim wlim 6318  suc csuc 6319  cfv 6496  rankcrnk 9699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-reg 9528  ax-inf2 9577
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-r1 9700  df-rank 9701
This theorem is referenced by:  rankxpsuc  9818
  Copyright terms: Public domain W3C validator