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

Theorem rankxplim3 8627
 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 5703 . 2 (Lim (rank‘(𝐴 × 𝐵)) → Lim (rank‘(𝐴 × 𝐵)))
2 0ellim 5704 . . . 4 (Lim (rank‘(𝐴 × 𝐵)) → ∅ ∈ (rank‘(𝐴 × 𝐵)))
3 n0i 3879 . . . 4 (∅ ∈ (rank‘(𝐴 × 𝐵)) → ¬ (rank‘(𝐴 × 𝐵)) = ∅)
4 unieq 4380 . . . . . 6 ((rank‘(𝐴 × 𝐵)) = ∅ → (rank‘(𝐴 × 𝐵)) = ∅)
5 uni0 4401 . . . . . 6 ∅ = ∅
64, 5syl6eq 2660 . . . . 5 ((rank‘(𝐴 × 𝐵)) = ∅ → (rank‘(𝐴 × 𝐵)) = ∅)
76con3i 149 . . . 4 (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (rank‘(𝐴 × 𝐵)) = ∅)
82, 3, 73syl 18 . . 3 (Lim (rank‘(𝐴 × 𝐵)) → ¬ (rank‘(𝐴 × 𝐵)) = ∅)
9 rankon 8541 . . . . . . . . . 10 (rank‘(𝐴𝐵)) ∈ On
109onsuci 6930 . . . . . . . . 9 suc (rank‘(𝐴𝐵)) ∈ On
1110onsuci 6930 . . . . . . . 8 suc suc (rank‘(𝐴𝐵)) ∈ On
1211elexi 3186 . . . . . . 7 suc suc (rank‘(𝐴𝐵)) ∈ V
1312sucid 5721 . . . . . 6 suc suc (rank‘(𝐴𝐵)) ∈ suc suc suc (rank‘(𝐴𝐵))
1411onsuci 6930 . . . . . . . 8 suc suc suc (rank‘(𝐴𝐵)) ∈ On
15 ontri1 5674 . . . . . . . 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 704 . . . . . . 7 (suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵)) ↔ ¬ suc suc (rank‘(𝐴𝐵)) ∈ suc suc suc (rank‘(𝐴𝐵)))
1716con2bii 346 . . . . . 6 (suc suc (rank‘(𝐴𝐵)) ∈ suc suc suc (rank‘(𝐴𝐵)) ↔ ¬ suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵)))
1813, 17mpbi 219 . . . . 5 ¬ suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵))
19 rankxplim.1 . . . . . . 7 𝐴 ∈ V
20 rankxplim.2 . . . . . . 7 𝐵 ∈ V
2119, 20rankxpu 8622 . . . . . 6 (rank‘(𝐴 × 𝐵)) ⊆ suc suc (rank‘(𝐴𝐵))
22 sstr 3576 . . . . . 6 ((suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴 × 𝐵)) ⊆ suc suc (rank‘(𝐴𝐵))) → suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵)))
2321, 22mpan2 703 . . . . 5 (suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)) → suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵)))
2418, 23mto 187 . . . 4 ¬ suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵))
25 reeanv 3086 . . . . 5 (∃𝑥 ∈ On ∃𝑦 ∈ On ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) ↔ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦))
26 simprl 790 . . . . . . . . . . . . 13 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴𝐵)) = suc 𝑥)
27 simpr 476 . . . . . . . . . . . . . . . . . 18 ((Lim (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴𝐵)) = suc 𝑥) → (rank‘(𝐴𝐵)) = suc 𝑥)
28 rankuni 8609 . . . . . . . . . . . . . . . . . . . . . 22 (rank‘ (𝐴 × 𝐵)) = (rank‘ (𝐴 × 𝐵))
29 rankuni 8609 . . . . . . . . . . . . . . . . . . . . . . 23 (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))
3029unieqi 4381 . . . . . . . . . . . . . . . . . . . . . 22 (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))
3128, 30eqtri 2632 . . . . . . . . . . . . . . . . . . . . 21 (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))
32 df-ne 2782 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 × 𝐵) ≠ ∅ ↔ ¬ (𝐴 × 𝐵) = ∅)
3319, 20xpex 6860 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 × 𝐵) ∈ V
3433rankeq0 8607 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 × 𝐵) = ∅ ↔ (rank‘(𝐴 × 𝐵)) = ∅)
3534notbii 309 . . . . . . . . . . . . . . . . . . . . . . . . 25 (¬ (𝐴 × 𝐵) = ∅ ↔ ¬ (rank‘(𝐴 × 𝐵)) = ∅)
3632, 35bitr2i 264 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (rank‘(𝐴 × 𝐵)) = ∅ ↔ (𝐴 × 𝐵) ≠ ∅)
378, 36sylib 207 . . . . . . . . . . . . . . . . . . . . . . 23 (Lim (rank‘(𝐴 × 𝐵)) → (𝐴 × 𝐵) ≠ ∅)
38 unixp 5585 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 × 𝐵) ≠ ∅ → (𝐴 × 𝐵) = (𝐴𝐵))
3937, 38syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (Lim (rank‘(𝐴 × 𝐵)) → (𝐴 × 𝐵) = (𝐴𝐵))
4039fveq2d 6107 . . . . . . . . . . . . . . . . . . . . 21 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴𝐵)))
4131, 40syl5reqr 2659 . . . . . . . . . . . . . . . . . . . 20 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴𝐵)) = (rank‘(𝐴 × 𝐵)))
42 eqimss 3620 . . . . . . . . . . . . . . . . . . . 20 ((rank‘(𝐴𝐵)) = (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
4341, 42syl 17 . . . . . . . . . . . . . . . . . . 19 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
4443adantr 480 . . . . . . . . . . . . . . . . . 18 ((Lim (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴𝐵)) = suc 𝑥) → (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
4527, 44eqsstr3d 3603 . . . . . . . . . . . . . . . . 17 ((Lim (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴𝐵)) = suc 𝑥) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
4645adantrr 749 . . . . . . . . . . . . . . . 16 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
47 limuni 5702 . . . . . . . . . . . . . . . . 17 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
4847adantr 480 . . . . . . . . . . . . . . . 16 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
4946, 48sseqtr4d 3605 . . . . . . . . . . . . . . 15 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
50 vex 3176 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
51 rankon 8541 . . . . . . . . . . . . . . . . . 18 (rank‘(𝐴 × 𝐵)) ∈ On
5251onordi 5749 . . . . . . . . . . . . . . . . 17 Ord (rank‘(𝐴 × 𝐵))
53 orduni 6886 . . . . . . . . . . . . . . . . 17 (Ord (rank‘(𝐴 × 𝐵)) → Ord (rank‘(𝐴 × 𝐵)))
5452, 53ax-mp 5 . . . . . . . . . . . . . . . 16 Ord (rank‘(𝐴 × 𝐵))
55 ordelsuc 6912 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ V ∧ Ord (rank‘(𝐴 × 𝐵))) → (𝑥 (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 (rank‘(𝐴 × 𝐵))))
5650, 54, 55mp2an 704 . . . . . . . . . . . . . . 15 (𝑥 (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 (rank‘(𝐴 × 𝐵)))
5749, 56sylibr 223 . . . . . . . . . . . . . 14 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → 𝑥 (rank‘(𝐴 × 𝐵)))
58 limsuc 6941 . . . . . . . . . . . . . . 15 (Lim (rank‘(𝐴 × 𝐵)) → (𝑥 (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 (rank‘(𝐴 × 𝐵))))
5958adantr 480 . . . . . . . . . . . . . 14 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (𝑥 (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 (rank‘(𝐴 × 𝐵))))
6057, 59mpbid 221 . . . . . . . . . . . . 13 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
6126, 60eqeltrd 2688 . . . . . . . . . . . 12 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)))
62 limsuc 6941 . . . . . . . . . . . . 13 (Lim (rank‘(𝐴 × 𝐵)) → ((rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)) ↔ suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵))))
6362adantr 480 . . . . . . . . . . . 12 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → ((rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)) ↔ suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵))))
6461, 63mpbid 221 . . . . . . . . . . 11 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)))
65 ordsucelsuc 6914 . . . . . . . . . . . 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 207 . . . . . . . . . 10 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc (rank‘(𝐴𝐵)) ∈ suc (rank‘(𝐴 × 𝐵)))
68 onsucuni2 6926 . . . . . . . . . . . 12 (((rank‘(𝐴 × 𝐵)) ∈ On ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
6951, 68mpan 702 . . . . . . . . . . 11 ((rank‘(𝐴 × 𝐵)) = suc 𝑦 → suc (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
7069ad2antll 761 . . . . . . . . . 10 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
7167, 70eleqtrd 2690 . . . . . . . . 9 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)))
7211, 51onsucssi 6933 . . . . . . . . 9 (suc suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)) ↔ suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
7371, 72sylib 207 . . . . . . . 8 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
7473ex 449 . . . . . . 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 3019 . . . . 5 (Lim (rank‘(𝐴 × 𝐵)) → (∃𝑥 ∈ On ∃𝑦 ∈ On ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵))))
7725, 76syl5bir 232 . . . 4 (Lim (rank‘(𝐴 × 𝐵)) → ((∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵))))
7824, 77mtoi 189 . . 3 (Lim (rank‘(𝐴 × 𝐵)) → ¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦))
79 ianor 508 . . . . . 6 (¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) ↔ (¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∨ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦))
80 un00 3963 . . . . . . . . . . . . . 14 ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴𝐵) = ∅)
81 olc 398 . . . . . . . . . . . . . . 15 (𝐵 = ∅ → (𝐴 = ∅ ∨ 𝐵 = ∅))
8281adantl 481 . . . . . . . . . . . . . 14 ((𝐴 = ∅ ∧ 𝐵 = ∅) → (𝐴 = ∅ ∨ 𝐵 = ∅))
8380, 82sylbir 224 . . . . . . . . . . . . 13 ((𝐴𝐵) = ∅ → (𝐴 = ∅ ∨ 𝐵 = ∅))
84 xpeq0 5473 . . . . . . . . . . . . 13 ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))
8583, 84sylibr 223 . . . . . . . . . . . 12 ((𝐴𝐵) = ∅ → (𝐴 × 𝐵) = ∅)
8685con3i 149 . . . . . . . . . . 11 (¬ (𝐴 × 𝐵) = ∅ → ¬ (𝐴𝐵) = ∅)
8735, 86sylbir 224 . . . . . . . . . 10 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (𝐴𝐵) = ∅)
8819, 20unex 6854 . . . . . . . . . . . 12 (𝐴𝐵) ∈ V
8988rankeq0 8607 . . . . . . . . . . 11 ((𝐴𝐵) = ∅ ↔ (rank‘(𝐴𝐵)) = ∅)
9089notbii 309 . . . . . . . . . 10 (¬ (𝐴𝐵) = ∅ ↔ ¬ (rank‘(𝐴𝐵)) = ∅)
9187, 90sylib 207 . . . . . . . . 9 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (rank‘(𝐴𝐵)) = ∅)
929onordi 5749 . . . . . . . . . . 11 Ord (rank‘(𝐴𝐵))
93 ordzsl 6937 . . . . . . . . . . 11 (Ord (rank‘(𝐴𝐵)) ↔ ((rank‘(𝐴𝐵)) = ∅ ∨ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴𝐵))))
9492, 93mpbi 219 . . . . . . . . . 10 ((rank‘(𝐴𝐵)) = ∅ ∨ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴𝐵)))
95943ori 1380 . . . . . . . . 9 ((¬ (rank‘(𝐴𝐵)) = ∅ ∧ ¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥) → Lim (rank‘(𝐴𝐵)))
9691, 95sylan 487 . . . . . . . 8 ((¬ (rank‘(𝐴 × 𝐵)) = ∅ ∧ ¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥) → Lim (rank‘(𝐴𝐵)))
9796ex 449 . . . . . . 7 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 → Lim (rank‘(𝐴𝐵))))
98 ordzsl 6937 . . . . . . . . . 10 (Ord (rank‘(𝐴 × 𝐵)) ↔ ((rank‘(𝐴 × 𝐵)) = ∅ ∨ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦 ∨ Lim (rank‘(𝐴 × 𝐵))))
9952, 98mpbi 219 . . . . . . . . 9 ((rank‘(𝐴 × 𝐵)) = ∅ ∨ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦 ∨ Lim (rank‘(𝐴 × 𝐵)))
100993ori 1380 . . . . . . . 8 ((¬ (rank‘(𝐴 × 𝐵)) = ∅ ∧ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → Lim (rank‘(𝐴 × 𝐵)))
101100ex 449 . . . . . . 7 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦 → Lim (rank‘(𝐴 × 𝐵))))
10297, 101orim12d 879 . . . . . 6 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ((¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∨ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → (Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵)))))
10379, 102syl5bi 231 . . . . 5 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → (Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵)))))
104103imp 444 . . . 4 ((¬ (rank‘(𝐴 × 𝐵)) = ∅ ∧ ¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))))
105 simpl 472 . . . . . . . 8 ((Lim (rank‘(𝐴𝐵)) ∧ ¬ (rank‘(𝐴 × 𝐵)) = ∅) → Lim (rank‘(𝐴𝐵)))
10634necon3abii 2828 . . . . . . . . . 10 ((𝐴 × 𝐵) ≠ ∅ ↔ ¬ (rank‘(𝐴 × 𝐵)) = ∅)
10719, 20rankxplim 8625 . . . . . . . . . 10 ((Lim (rank‘(𝐴𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴𝐵)))
108106, 107sylan2br 492 . . . . . . . . 9 ((Lim (rank‘(𝐴𝐵)) ∧ ¬ (rank‘(𝐴 × 𝐵)) = ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴𝐵)))
109 limeq 5652 . . . . . . . . 9 ((rank‘(𝐴 × 𝐵)) = (rank‘(𝐴𝐵)) → (Lim (rank‘(𝐴 × 𝐵)) ↔ Lim (rank‘(𝐴𝐵))))
110108, 109syl 17 . . . . . . . 8 ((Lim (rank‘(𝐴𝐵)) ∧ ¬ (rank‘(𝐴 × 𝐵)) = ∅) → (Lim (rank‘(𝐴 × 𝐵)) ↔ Lim (rank‘(𝐴𝐵))))
111105, 110mpbird 246 . . . . . . 7 ((Lim (rank‘(𝐴𝐵)) ∧ ¬ (rank‘(𝐴 × 𝐵)) = ∅) → Lim (rank‘(𝐴 × 𝐵)))
112111expcom 450 . . . . . 6 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (Lim (rank‘(𝐴𝐵)) → Lim (rank‘(𝐴 × 𝐵))))
113 idd 24 . . . . . 6 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (Lim (rank‘(𝐴 × 𝐵)) → Lim (rank‘(𝐴 × 𝐵))))
114112, 113jaod 394 . . . . 5 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ((Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))) → Lim (rank‘(𝐴 × 𝐵))))
115114adantr 480 . . . 4 ((¬ (rank‘(𝐴 × 𝐵)) = ∅ ∧ ¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → ((Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))) → Lim (rank‘(𝐴 × 𝐵))))
116104, 115mpd 15 . . 3 ((¬ (rank‘(𝐴 × 𝐵)) = ∅ ∧ ¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → Lim (rank‘(𝐴 × 𝐵)))
1178, 78, 116syl2anc 691 . 2 (Lim (rank‘(𝐴 × 𝐵)) → Lim (rank‘(𝐴 × 𝐵)))
1181, 117impbii 198 1 (Lim (rank‘(𝐴 × 𝐵)) ↔ Lim (rank‘(𝐴 × 𝐵)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∨ w3o 1030   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897  Vcvv 3173   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  ∪ cuni 4372   × cxp 5036  Ord word 5639  Oncon0 5640  Lim wlim 5641  suc csuc 5642  ‘cfv 5804  rankcrnk 8509 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-reg 8380  ax-inf2 8421 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-r1 8510  df-rank 8511 This theorem is referenced by:  rankxpsuc  8628
 Copyright terms: Public domain W3C validator