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

Theorem rankxplim3 8704
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 5755 . 2 (Lim (rank‘(𝐴 × 𝐵)) → Lim (rank‘(𝐴 × 𝐵)))
2 0ellim 5756 . . . 4 (Lim (rank‘(𝐴 × 𝐵)) → ∅ ∈ (rank‘(𝐴 × 𝐵)))
3 n0i 3902 . . . 4 (∅ ∈ (rank‘(𝐴 × 𝐵)) → ¬ (rank‘(𝐴 × 𝐵)) = ∅)
4 unieq 4417 . . . . . 6 ((rank‘(𝐴 × 𝐵)) = ∅ → (rank‘(𝐴 × 𝐵)) = ∅)
5 uni0 4438 . . . . . 6 ∅ = ∅
64, 5syl6eq 2671 . . . . 5 ((rank‘(𝐴 × 𝐵)) = ∅ → (rank‘(𝐴 × 𝐵)) = ∅)
76con3i 150 . . . 4 (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (rank‘(𝐴 × 𝐵)) = ∅)
82, 3, 73syl 18 . . 3 (Lim (rank‘(𝐴 × 𝐵)) → ¬ (rank‘(𝐴 × 𝐵)) = ∅)
9 rankon 8618 . . . . . . . . . 10 (rank‘(𝐴𝐵)) ∈ On
109onsuci 7000 . . . . . . . . 9 suc (rank‘(𝐴𝐵)) ∈ On
1110onsuci 7000 . . . . . . . 8 suc suc (rank‘(𝐴𝐵)) ∈ On
1211elexi 3203 . . . . . . 7 suc suc (rank‘(𝐴𝐵)) ∈ V
1312sucid 5773 . . . . . 6 suc suc (rank‘(𝐴𝐵)) ∈ suc suc suc (rank‘(𝐴𝐵))
1411onsuci 7000 . . . . . . . 8 suc suc suc (rank‘(𝐴𝐵)) ∈ On
15 ontri1 5726 . . . . . . . 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 707 . . . . . . 7 (suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵)) ↔ ¬ suc suc (rank‘(𝐴𝐵)) ∈ suc suc suc (rank‘(𝐴𝐵)))
1716con2bii 347 . . . . . 6 (suc suc (rank‘(𝐴𝐵)) ∈ suc suc suc (rank‘(𝐴𝐵)) ↔ ¬ suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵)))
1813, 17mpbi 220 . . . . 5 ¬ suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵))
19 rankxplim.1 . . . . . . 7 𝐴 ∈ V
20 rankxplim.2 . . . . . . 7 𝐵 ∈ V
2119, 20rankxpu 8699 . . . . . 6 (rank‘(𝐴 × 𝐵)) ⊆ suc suc (rank‘(𝐴𝐵))
22 sstr 3596 . . . . . 6 ((suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴 × 𝐵)) ⊆ suc suc (rank‘(𝐴𝐵))) → suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵)))
2321, 22mpan2 706 . . . . 5 (suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)) → suc suc suc (rank‘(𝐴𝐵)) ⊆ suc suc (rank‘(𝐴𝐵)))
2418, 23mto 188 . . . 4 ¬ suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵))
25 reeanv 3101 . . . . 5 (∃𝑥 ∈ On ∃𝑦 ∈ On ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) ↔ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦))
26 simprl 793 . . . . . . . . . . . . 13 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴𝐵)) = suc 𝑥)
27 simpr 477 . . . . . . . . . . . . . . . . . 18 ((Lim (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴𝐵)) = suc 𝑥) → (rank‘(𝐴𝐵)) = suc 𝑥)
28 rankuni 8686 . . . . . . . . . . . . . . . . . . . . . 22 (rank‘ (𝐴 × 𝐵)) = (rank‘ (𝐴 × 𝐵))
29 rankuni 8686 . . . . . . . . . . . . . . . . . . . . . . 23 (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))
3029unieqi 4418 . . . . . . . . . . . . . . . . . . . . . 22 (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))
3128, 30eqtri 2643 . . . . . . . . . . . . . . . . . . . . 21 (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))
32 df-ne 2791 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 × 𝐵) ≠ ∅ ↔ ¬ (𝐴 × 𝐵) = ∅)
3319, 20xpex 6927 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 × 𝐵) ∈ V
3433rankeq0 8684 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 × 𝐵) = ∅ ↔ (rank‘(𝐴 × 𝐵)) = ∅)
3534notbii 310 . . . . . . . . . . . . . . . . . . . . . . . . 25 (¬ (𝐴 × 𝐵) = ∅ ↔ ¬ (rank‘(𝐴 × 𝐵)) = ∅)
3632, 35bitr2i 265 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (rank‘(𝐴 × 𝐵)) = ∅ ↔ (𝐴 × 𝐵) ≠ ∅)
378, 36sylib 208 . . . . . . . . . . . . . . . . . . . . . . 23 (Lim (rank‘(𝐴 × 𝐵)) → (𝐴 × 𝐵) ≠ ∅)
38 unixp 5637 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 × 𝐵) ≠ ∅ → (𝐴 × 𝐵) = (𝐴𝐵))
3937, 38syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (Lim (rank‘(𝐴 × 𝐵)) → (𝐴 × 𝐵) = (𝐴𝐵))
4039fveq2d 6162 . . . . . . . . . . . . . . . . . . . . 21 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴𝐵)))
4131, 40syl5reqr 2670 . . . . . . . . . . . . . . . . . . . 20 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴𝐵)) = (rank‘(𝐴 × 𝐵)))
42 eqimss 3642 . . . . . . . . . . . . . . . . . . . 20 ((rank‘(𝐴𝐵)) = (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
4341, 42syl 17 . . . . . . . . . . . . . . . . . . 19 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
4443adantr 481 . . . . . . . . . . . . . . . . . 18 ((Lim (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴𝐵)) = suc 𝑥) → (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
4527, 44eqsstr3d 3625 . . . . . . . . . . . . . . . . 17 ((Lim (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴𝐵)) = suc 𝑥) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
4645adantrr 752 . . . . . . . . . . . . . . . 16 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
47 limuni 5754 . . . . . . . . . . . . . . . . 17 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
4847adantr 481 . . . . . . . . . . . . . . . 16 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
4946, 48sseqtr4d 3627 . . . . . . . . . . . . . . 15 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
50 vex 3193 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
51 rankon 8618 . . . . . . . . . . . . . . . . . 18 (rank‘(𝐴 × 𝐵)) ∈ On
5251onordi 5801 . . . . . . . . . . . . . . . . 17 Ord (rank‘(𝐴 × 𝐵))
53 orduni 6956 . . . . . . . . . . . . . . . . 17 (Ord (rank‘(𝐴 × 𝐵)) → Ord (rank‘(𝐴 × 𝐵)))
5452, 53ax-mp 5 . . . . . . . . . . . . . . . 16 Ord (rank‘(𝐴 × 𝐵))
55 ordelsuc 6982 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ V ∧ Ord (rank‘(𝐴 × 𝐵))) → (𝑥 (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 (rank‘(𝐴 × 𝐵))))
5650, 54, 55mp2an 707 . . . . . . . . . . . . . . 15 (𝑥 (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 (rank‘(𝐴 × 𝐵)))
5749, 56sylibr 224 . . . . . . . . . . . . . 14 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → 𝑥 (rank‘(𝐴 × 𝐵)))
58 limsuc 7011 . . . . . . . . . . . . . . 15 (Lim (rank‘(𝐴 × 𝐵)) → (𝑥 (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 (rank‘(𝐴 × 𝐵))))
5958adantr 481 . . . . . . . . . . . . . 14 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (𝑥 (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 (rank‘(𝐴 × 𝐵))))
6057, 59mpbid 222 . . . . . . . . . . . . 13 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
6126, 60eqeltrd 2698 . . . . . . . . . . . 12 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)))
62 limsuc 7011 . . . . . . . . . . . . 13 (Lim (rank‘(𝐴 × 𝐵)) → ((rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)) ↔ suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵))))
6362adantr 481 . . . . . . . . . . . 12 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → ((rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)) ↔ suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵))))
6461, 63mpbid 222 . . . . . . . . . . 11 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)))
65 ordsucelsuc 6984 . . . . . . . . . . . 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 208 . . . . . . . . . 10 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc (rank‘(𝐴𝐵)) ∈ suc (rank‘(𝐴 × 𝐵)))
68 onsucuni2 6996 . . . . . . . . . . . 12 (((rank‘(𝐴 × 𝐵)) ∈ On ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
6951, 68mpan 705 . . . . . . . . . . 11 ((rank‘(𝐴 × 𝐵)) = suc 𝑦 → suc (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
7069ad2antll 764 . . . . . . . . . 10 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
7167, 70eleqtrd 2700 . . . . . . . . 9 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)))
7211, 51onsucssi 7003 . . . . . . . . 9 (suc suc (rank‘(𝐴𝐵)) ∈ (rank‘(𝐴 × 𝐵)) ↔ suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
7371, 72sylib 208 . . . . . . . 8 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
7473ex 450 . . . . . . 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 3032 . . . . 5 (Lim (rank‘(𝐴 × 𝐵)) → (∃𝑥 ∈ On ∃𝑦 ∈ On ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵))))
7725, 76syl5bir 233 . . . 4 (Lim (rank‘(𝐴 × 𝐵)) → ((∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵))))
7824, 77mtoi 190 . . 3 (Lim (rank‘(𝐴 × 𝐵)) → ¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦))
79 ianor 509 . . . . . 6 (¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) ↔ (¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∨ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦))
80 un00 3989 . . . . . . . . . . . . . 14 ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴𝐵) = ∅)
81 olc 399 . . . . . . . . . . . . . . 15 (𝐵 = ∅ → (𝐴 = ∅ ∨ 𝐵 = ∅))
8281adantl 482 . . . . . . . . . . . . . 14 ((𝐴 = ∅ ∧ 𝐵 = ∅) → (𝐴 = ∅ ∨ 𝐵 = ∅))
8380, 82sylbir 225 . . . . . . . . . . . . 13 ((𝐴𝐵) = ∅ → (𝐴 = ∅ ∨ 𝐵 = ∅))
84 xpeq0 5523 . . . . . . . . . . . . 13 ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))
8583, 84sylibr 224 . . . . . . . . . . . 12 ((𝐴𝐵) = ∅ → (𝐴 × 𝐵) = ∅)
8685con3i 150 . . . . . . . . . . 11 (¬ (𝐴 × 𝐵) = ∅ → ¬ (𝐴𝐵) = ∅)
8735, 86sylbir 225 . . . . . . . . . 10 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (𝐴𝐵) = ∅)
8819, 20unex 6921 . . . . . . . . . . . 12 (𝐴𝐵) ∈ V
8988rankeq0 8684 . . . . . . . . . . 11 ((𝐴𝐵) = ∅ ↔ (rank‘(𝐴𝐵)) = ∅)
9089notbii 310 . . . . . . . . . 10 (¬ (𝐴𝐵) = ∅ ↔ ¬ (rank‘(𝐴𝐵)) = ∅)
9187, 90sylib 208 . . . . . . . . 9 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (rank‘(𝐴𝐵)) = ∅)
929onordi 5801 . . . . . . . . . . 11 Ord (rank‘(𝐴𝐵))
93 ordzsl 7007 . . . . . . . . . . 11 (Ord (rank‘(𝐴𝐵)) ↔ ((rank‘(𝐴𝐵)) = ∅ ∨ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴𝐵))))
9492, 93mpbi 220 . . . . . . . . . 10 ((rank‘(𝐴𝐵)) = ∅ ∨ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴𝐵)))
95943ori 1385 . . . . . . . . 9 ((¬ (rank‘(𝐴𝐵)) = ∅ ∧ ¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥) → Lim (rank‘(𝐴𝐵)))
9691, 95sylan 488 . . . . . . . 8 ((¬ (rank‘(𝐴 × 𝐵)) = ∅ ∧ ¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥) → Lim (rank‘(𝐴𝐵)))
9796ex 450 . . . . . . 7 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 → Lim (rank‘(𝐴𝐵))))
98 ordzsl 7007 . . . . . . . . . 10 (Ord (rank‘(𝐴 × 𝐵)) ↔ ((rank‘(𝐴 × 𝐵)) = ∅ ∨ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦 ∨ Lim (rank‘(𝐴 × 𝐵))))
9952, 98mpbi 220 . . . . . . . . 9 ((rank‘(𝐴 × 𝐵)) = ∅ ∨ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦 ∨ Lim (rank‘(𝐴 × 𝐵)))
100993ori 1385 . . . . . . . 8 ((¬ (rank‘(𝐴 × 𝐵)) = ∅ ∧ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → Lim (rank‘(𝐴 × 𝐵)))
101100ex 450 . . . . . . 7 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦 → Lim (rank‘(𝐴 × 𝐵))))
10297, 101orim12d 882 . . . . . 6 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ((¬ ∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∨ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → (Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵)))))
10379, 102syl5bi 232 . . . . 5 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → (Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵)))))
104103imp 445 . . . 4 ((¬ (rank‘(𝐴 × 𝐵)) = ∅ ∧ ¬ (∃𝑥 ∈ On (rank‘(𝐴𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))))
105 simpl 473 . . . . . . . 8 ((Lim (rank‘(𝐴𝐵)) ∧ ¬ (rank‘(𝐴 × 𝐵)) = ∅) → Lim (rank‘(𝐴𝐵)))
10634necon3abii 2836 . . . . . . . . . 10 ((𝐴 × 𝐵) ≠ ∅ ↔ ¬ (rank‘(𝐴 × 𝐵)) = ∅)
10719, 20rankxplim 8702 . . . . . . . . . 10 ((Lim (rank‘(𝐴𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴𝐵)))
108106, 107sylan2br 493 . . . . . . . . 9 ((Lim (rank‘(𝐴𝐵)) ∧ ¬ (rank‘(𝐴 × 𝐵)) = ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴𝐵)))
109 limeq 5704 . . . . . . . . 9 ((rank‘(𝐴 × 𝐵)) = (rank‘(𝐴𝐵)) → (Lim (rank‘(𝐴 × 𝐵)) ↔ Lim (rank‘(𝐴𝐵))))
110108, 109syl 17 . . . . . . . 8 ((Lim (rank‘(𝐴𝐵)) ∧ ¬ (rank‘(𝐴 × 𝐵)) = ∅) → (Lim (rank‘(𝐴 × 𝐵)) ↔ Lim (rank‘(𝐴𝐵))))
111105, 110mpbird 247 . . . . . . 7 ((Lim (rank‘(𝐴𝐵)) ∧ ¬ (rank‘(𝐴 × 𝐵)) = ∅) → Lim (rank‘(𝐴 × 𝐵)))
112111expcom 451 . . . . . 6 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (Lim (rank‘(𝐴𝐵)) → Lim (rank‘(𝐴 × 𝐵))))
113 idd 24 . . . . . 6 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → (Lim (rank‘(𝐴 × 𝐵)) → Lim (rank‘(𝐴 × 𝐵))))
114112, 113jaod 395 . . . . 5 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ((Lim (rank‘(𝐴𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))) → Lim (rank‘(𝐴 × 𝐵))))
115114adantr 481 . . . 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 692 . 2 (Lim (rank‘(𝐴 × 𝐵)) → Lim (rank‘(𝐴 × 𝐵)))
1181, 117impbii 199 1 (Lim (rank‘(𝐴 × 𝐵)) ↔ Lim (rank‘(𝐴 × 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3o 1035   = wceq 1480  wcel 1987  wne 2790  wrex 2909  Vcvv 3190  cun 3558  wss 3560  c0 3897   cuni 4409   × cxp 5082  Ord word 5691  Oncon0 5692  Lim wlim 5693  suc csuc 5694  cfv 5857  rankcrnk 8586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-reg 8457  ax-inf2 8498
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-reu 2915  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-om 7028  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-r1 8587  df-rank 8588
This theorem is referenced by:  rankxpsuc  8705
  Copyright terms: Public domain W3C validator