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

Theorem rankxplim3 9918
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 6447 . 2 (Lim (rank‘(𝐴 × 𝐵)) → Lim (rank‘(𝐴 × 𝐵)))
2 0ellim 6448 . . . 4 (Lim (rank‘(𝐴 × 𝐵)) → ∅ ∈ (rank‘(𝐴 × 𝐵)))
3 n0i 4345 . . . 4 (∅ ∈ (rank‘(𝐴 × 𝐵)) → ¬ (rank‘(𝐴 × 𝐵)) = ∅)
4 unieq 4922 . . . . . 6 ((rank‘(𝐴 × 𝐵)) = ∅ → (rank‘(𝐴 × 𝐵)) = ∅)
5 uni0 4939 . . . . . 6 ∅ = ∅
64, 5eqtrdi 2790 . . . . 5 ((rank‘(𝐴 × 𝐵)) = ∅ → (rank‘(𝐴 × 𝐵)) = ∅)
76con3i 154 . . . 4 (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (rank‘(𝐴 × 𝐵)) = ∅)
82, 3, 73syl 18 . . 3 (Lim (rank‘(𝐴 × 𝐵)) → ¬ (rank‘(𝐴 × 𝐵)) = ∅)
9 rankon 9832 . . . . . . . . . 10 (rank‘(𝐴𝐵)) ∈ On
109onsuci 7858 . . . . . . . . 9 suc (rank‘(𝐴𝐵)) ∈ On
1110onsuci 7858 . . . . . . . 8 suc suc (rank‘(𝐴𝐵)) ∈ On
1211elexi 3500 . . . . . . 7 suc suc (rank‘(𝐴𝐵)) ∈ V
1312sucid 6467 . . . . . 6 suc suc (rank‘(𝐴𝐵)) ∈ suc suc suc (rank‘(𝐴𝐵))
1411onsuci 7858 . . . . . . . 8 suc suc suc (rank‘(𝐴𝐵)) ∈ On
15 ontri1 6419 . . . . . . . 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 692 . . . . . . 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 230 . . . . 5 ¬ suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵))
19 rankxplim.1 . . . . . . 7 𝐴 ∈ V
20 rankxplim.2 . . . . . . 7 𝐵 ∈ V
2119, 20rankxpu 9913 . . . . . 6 (rank‘(𝐴 × 𝐵)) ⊆ suc suc (rank‘(𝐴𝐵))
22 sstr 4003 . . . . . 6 ((suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴 × 𝐵)) ⊆ suc suc (rank‘(𝐴𝐵))) → suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵)))
2321, 22mpan2 691 . . . . 5 (suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)) → suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵)))
2418, 23mto 197 . . . 4 ¬ suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵))
25 reeanv 3226 . . . . 5 (∃𝑥 ∈ On ∃𝑦 ∈ On ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) ↔ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦))
26 simprl 771 . . . . . . . . . . . . 13 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴𝐵)) = suc 𝑥)
27 simpr 484 . . . . . . . . . . . . . . . . . 18 ((Lim (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴𝐵)) = suc 𝑥) → (rank‘(𝐴𝐵)) = suc 𝑥)
28 df-ne 2938 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 × 𝐵) ≠ ∅ ↔ ¬ (𝐴 × 𝐵) = ∅)
2919, 20xpex 7771 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 × 𝐵) ∈ V
3029rankeq0 9898 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 × 𝐵) = ∅ ↔ (rank‘(𝐴 × 𝐵)) = ∅)
3130notbii 320 . . . . . . . . . . . . . . . . . . . . . . . . 25 (¬ (𝐴 × 𝐵) = ∅ ↔ ¬ (rank‘(𝐴 × 𝐵)) = ∅)
3228, 31bitr2i 276 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (rank‘(𝐴 × 𝐵)) = ∅ ↔ (𝐴 × 𝐵) ≠ ∅)
338, 32sylib 218 . . . . . . . . . . . . . . . . . . . . . . 23 (Lim (rank‘(𝐴 × 𝐵)) → (𝐴 × 𝐵) ≠ ∅)
34 unixp 6303 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 × 𝐵) ≠ ∅ → (𝐴 × 𝐵) = (𝐴𝐵))
3533, 34syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (Lim (rank‘(𝐴 × 𝐵)) → (𝐴 × 𝐵) = (𝐴𝐵))
3635fveq2d 6910 . . . . . . . . . . . . . . . . . . . . 21 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴𝐵)))
37 rankuni 9900 . . . . . . . . . . . . . . . . . . . . . 22 (rank‘ (𝐴 × 𝐵)) = (rank‘ (𝐴 × 𝐵))
38 rankuni 9900 . . . . . . . . . . . . . . . . . . . . . . 23 (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))
3938unieqi 4923 . . . . . . . . . . . . . . . . . . . . . 22 (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))
4037, 39eqtri 2762 . . . . . . . . . . . . . . . . . . . . 21 (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))
4136, 40eqtr3di 2789 . . . . . . . . . . . . . . . . . . . 20 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴𝐵)) = (rank‘(𝐴 × 𝐵)))
42 eqimss 4053 . . . . . . . . . . . . . . . . . . . 20 ((rank‘(𝐴𝐵)) = (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
4341, 42syl 17 . . . . . . . . . . . . . . . . . . 19 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
4443adantr 480 . . . . . . . . . . . . . . . . . 18 ((Lim (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴𝐵)) = suc 𝑥) → (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
4527, 44eqsstrrd 4034 . . . . . . . . . . . . . . . . 17 ((Lim (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴𝐵)) = suc 𝑥) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
4645adantrr 717 . . . . . . . . . . . . . . . 16 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
47 limuni 6446 . . . . . . . . . . . . . . . . 17 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
4847adantr 480 . . . . . . . . . . . . . . . 16 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
4946, 48sseqtrrd 4036 . . . . . . . . . . . . . . 15 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
50 vex 3481 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
51 rankon 9832 . . . . . . . . . . . . . . . . . 18 (rank‘(𝐴 × 𝐵)) ∈ On
5251onordi 6496 . . . . . . . . . . . . . . . . 17 Ord (rank‘(𝐴 × 𝐵))
53 orduni 7808 . . . . . . . . . . . . . . . . 17 (Ord (rank‘(𝐴 × 𝐵)) → Ord (rank‘(𝐴 × 𝐵)))
5452, 53ax-mp 5 . . . . . . . . . . . . . . . 16 Ord (rank‘(𝐴 × 𝐵))
55 ordelsuc 7839 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ V ∧ Ord (rank‘(𝐴 × 𝐵))) → (𝑥 (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 (rank‘(𝐴 × 𝐵))))
5650, 54, 55mp2an 692 . . . . . . . . . . . . . . 15 (𝑥 (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 (rank‘(𝐴 × 𝐵)))
5749, 56sylibr 234 . . . . . . . . . . . . . 14 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → 𝑥 (rank‘(𝐴 × 𝐵)))
58 limsuc 7869 . . . . . . . . . . . . . . 15 (Lim (rank‘(𝐴 × 𝐵)) → (𝑥 (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 (rank‘(𝐴 × 𝐵))))
5958adantr 480 . . . . . . . . . . . . . 14 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (𝑥 (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 (rank‘(𝐴 × 𝐵))))
6057, 59mpbid 232 . . . . . . . . . . . . 13 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
6126, 60eqeltrd 2838 . . . . . . . . . . . 12 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)))
62 limsuc 7869 . . . . . . . . . . . . 13 (Lim (rank‘(𝐴 × 𝐵)) → ((rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)) ↔ suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵))))
6362adantr 480 . . . . . . . . . . . 12 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → ((rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)) ↔ suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵))))
6461, 63mpbid 232 . . . . . . . . . . 11 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)))
65 ordsucelsuc 7841 . . . . . . . . . . . 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 218 . . . . . . . . . 10 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc (rank‘(𝐴𝐵)) ∈ suc (rank‘(𝐴 × 𝐵)))
68 onsucuni2 7853 . . . . . . . . . . . 12 (((rank‘(𝐴 × 𝐵)) ∈ On ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
6951, 68mpan 690 . . . . . . . . . . 11 ((rank‘(𝐴 × 𝐵)) = suc 𝑦 → suc (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
7069ad2antll 729 . . . . . . . . . 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 7861 . . . . . . . . 9 (suc suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)) ↔ suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
7371, 72sylib 218 . . . . . . . 8 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
7473ex 412 . . . . . . 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 3209 . . . . 5 (Lim (rank‘(𝐴 × 𝐵)) → (∃𝑥 ∈ On ∃𝑦 ∈ On ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵))))
7725, 76biimtrrid 243 . . . 4 (Lim (rank‘(𝐴 × 𝐵)) → ((∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵))))
7824, 77mtoi 199 . . 3 (Lim (rank‘(𝐴 × 𝐵)) → ¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦))
79 ianor 983 . . . . . 6 (¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) ↔ (¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∨ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦))
80 un00 4450 . . . . . . . . . . . . . 14 ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴𝐵) = ∅)
81 animorl 979 . . . . . . . . . . . . . 14 ((𝐴 = ∅ ∧ 𝐵 = ∅) → (𝐴 = ∅ ∨ 𝐵 = ∅))
8280, 81sylbir 235 . . . . . . . . . . . . 13 ((𝐴𝐵) = ∅ → (𝐴 = ∅ ∨ 𝐵 = ∅))
83 xpeq0 6181 . . . . . . . . . . . . 13 ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))
8482, 83sylibr 234 . . . . . . . . . . . 12 ((𝐴𝐵) = ∅ → (𝐴 × 𝐵) = ∅)
8584con3i 154 . . . . . . . . . . 11 (¬ (𝐴 × 𝐵) = ∅ → ¬ (𝐴𝐵) = ∅)
8631, 85sylbir 235 . . . . . . . . . 10 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (𝐴𝐵) = ∅)
8719, 20unex 7762 . . . . . . . . . . . 12 (𝐴𝐵) ∈ V
8887rankeq0 9898 . . . . . . . . . . 11 ((𝐴𝐵) = ∅ ↔ (rank‘(𝐴𝐵)) = ∅)
8988notbii 320 . . . . . . . . . 10 (¬ (𝐴𝐵) = ∅ ↔ ¬ (rank‘(𝐴𝐵)) = ∅)
9086, 89sylib 218 . . . . . . . . 9 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (rank‘(𝐴𝐵)) = ∅)
919onordi 6496 . . . . . . . . . . 11 Ord (rank‘(𝐴𝐵))
92 ordzsl 7865 . . . . . . . . . . 11 (Ord (rank‘(𝐴𝐵)) ↔ ((rank‘(𝐴𝐵)) = ∅ ∨ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴𝐵))))
9391, 92mpbi 230 . . . . . . . . . 10 ((rank‘(𝐴𝐵)) = ∅ ∨ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴𝐵)))
94933ori 1423 . . . . . . . . 9 ((¬ (rank‘(𝐴𝐵)) = ∅ ∧ ¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥) → Lim (rank‘(𝐴𝐵)))
9590, 94sylan 580 . . . . . . . 8 ((¬ (rank‘(𝐴 × 𝐵)) = ∅ ∧ ¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥) → Lim (rank‘(𝐴𝐵)))
9695ex 412 . . . . . . 7 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 → Lim (rank‘(𝐴𝐵))))
97 ordzsl 7865 . . . . . . . . . 10 (Ord (rank‘(𝐴 × 𝐵)) ↔ ((rank‘(𝐴 × 𝐵)) = ∅ ∨ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦 ∨ Lim (rank‘(𝐴 × 𝐵))))
9852, 97mpbi 230 . . . . . . . . 9 ((rank‘(𝐴 × 𝐵)) = ∅ ∨ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦 ∨ Lim (rank‘(𝐴 × 𝐵)))
99983ori 1423 . . . . . . . 8 ((¬ (rank‘(𝐴 × 𝐵)) = ∅ ∧ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → Lim (rank‘(𝐴 × 𝐵)))
10099ex 412 . . . . . . 7 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦 → Lim (rank‘(𝐴 × 𝐵))))
10196, 100orim12d 966 . . . . . 6 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ((¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∨ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → (Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵)))))
10279, 101biimtrid 242 . . . . 5 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → (Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵)))))
103102imp 406 . . . 4 ((¬ (rank‘(𝐴 × 𝐵)) = ∅ ∧ ¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))))
104 simpl 482 . . . . . . . 8 ((Lim (rank‘(𝐴𝐵)) ∧ ¬ (rank‘(𝐴 × 𝐵)) = ∅) → Lim (rank‘(𝐴𝐵)))
10530necon3abii 2984 . . . . . . . . . 10 ((𝐴 × 𝐵) ≠ ∅ ↔ ¬ (rank‘(𝐴 × 𝐵)) = ∅)
10619, 20rankxplim 9916 . . . . . . . . . 10 ((Lim (rank‘(𝐴𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴𝐵)))
107105, 106sylan2br 595 . . . . . . . . 9 ((Lim (rank‘(𝐴𝐵)) ∧ ¬ (rank‘(𝐴 × 𝐵)) = ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴𝐵)))
108 limeq 6397 . . . . . . . . 9 ((rank‘(𝐴 × 𝐵)) = (rank‘(𝐴𝐵)) → (Lim (rank‘(𝐴 × 𝐵)) ↔ Lim (rank‘(𝐴𝐵))))
109107, 108syl 17 . . . . . . . 8 ((Lim (rank‘(𝐴𝐵)) ∧ ¬ (rank‘(𝐴 × 𝐵)) = ∅) → (Lim (rank‘(𝐴 × 𝐵)) ↔ Lim (rank‘(𝐴𝐵))))
110104, 109mpbird 257 . . . . . . 7 ((Lim (rank‘(𝐴𝐵)) ∧ ¬ (rank‘(𝐴 × 𝐵)) = ∅) → Lim (rank‘(𝐴 × 𝐵)))
111110expcom 413 . . . . . 6 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (Lim (rank‘(𝐴𝐵)) → Lim (rank‘(𝐴 × 𝐵))))
112 idd 24 . . . . . 6 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (Lim (rank‘(𝐴 × 𝐵)) → Lim (rank‘(𝐴 × 𝐵))))
113111, 112jaod 859 . . . . 5 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ((Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))) → Lim (rank‘(𝐴 × 𝐵))))
114113adantr 480 . . . 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 209 1 (Lim (rank‘(𝐴 × 𝐵)) ↔ Lim (rank‘(𝐴 × 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3o 1085   = wceq 1536  wcel 2105  wne 2937  wrex 3067  Vcvv 3477  cun 3960  wss 3962  c0 4338   cuni 4911   × cxp 5686  Ord word 6384  Oncon0 6385  Lim wlim 6386  suc csuc 6387  cfv 6562  rankcrnk 9800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-reg 9629  ax-inf2 9678
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-r1 9801  df-rank 9802
This theorem is referenced by:  rankxpsuc  9919
  Copyright terms: Public domain W3C validator