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

Theorem rankxplim3 8696
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 5750 . 2 (Lim (rank‘(𝐴 × 𝐵)) → Lim (rank‘(𝐴 × 𝐵)))
2 0ellim 5751 . . . 4 (Lim (rank‘(𝐴 × 𝐵)) → ∅ ∈ (rank‘(𝐴 × 𝐵)))
3 n0i 3901 . . . 4 (∅ ∈ (rank‘(𝐴 × 𝐵)) → ¬ (rank‘(𝐴 × 𝐵)) = ∅)
4 unieq 4415 . . . . . 6 ((rank‘(𝐴 × 𝐵)) = ∅ → (rank‘(𝐴 × 𝐵)) = ∅)
5 uni0 4436 . . . . . 6 ∅ = ∅
64, 5syl6eq 2671 . . . . 5 ((rank‘(𝐴 × 𝐵)) = ∅ → (rank‘(𝐴 × 𝐵)) = ∅)
76con3i 150 . . . 4 (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (rank‘(𝐴 × 𝐵)) = ∅)
82, 3, 73syl 18 . . 3 (Lim (rank‘(𝐴 × 𝐵)) → ¬ (rank‘(𝐴 × 𝐵)) = ∅)
9 rankon 8610 . . . . . . . . . 10 (rank‘(𝐴𝐵)) ∈ On
109onsuci 6992 . . . . . . . . 9 suc (rank‘(𝐴𝐵)) ∈ On
1110onsuci 6992 . . . . . . . 8 suc suc (rank‘(𝐴𝐵)) ∈ On
1211elexi 3202 . . . . . . 7 suc suc (rank‘(𝐴𝐵)) ∈ V
1312sucid 5768 . . . . . 6 suc suc (rank‘(𝐴𝐵)) ∈ suc suc suc (rank‘(𝐴𝐵))
1411onsuci 6992 . . . . . . . 8 suc suc suc (rank‘(𝐴𝐵)) ∈ On
15 ontri1 5721 . . . . . . . 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 8691 . . . . . 6 (rank‘(𝐴 × 𝐵)) ⊆ suc suc (rank‘(𝐴𝐵))
22 sstr 3595 . . . . . 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 3100 . . . . 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 8678 . . . . . . . . . . . . . . . . . . . . . 22 (rank‘ (𝐴 × 𝐵)) = (rank‘ (𝐴 × 𝐵))
29 rankuni 8678 . . . . . . . . . . . . . . . . . . . . . . 23 (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))
3029unieqi 4416 . . . . . . . . . . . . . . . . . . . . . 22 (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))
3128, 30eqtri 2643 . . . . . . . . . . . . . . . . . . . . 21 (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))
32 df-ne 2791 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 × 𝐵) ≠ ∅ ↔ ¬ (𝐴 × 𝐵) = ∅)
3319, 20xpex 6922 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 × 𝐵) ∈ V
3433rankeq0 8676 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 × 𝐵) = ∅ ↔ (rank‘(𝐴 × 𝐵)) = ∅)
3534notbii 310 . . . . . . . . . . . . . . . . . . . . . . . . 25 (¬ (𝐴 × 𝐵) = ∅ ↔ ¬ (rank‘(𝐴 × 𝐵)) = ∅)
3632, 35bitr2i 265 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ (rank‘(𝐴 × 𝐵)) = ∅ ↔ (𝐴 × 𝐵) ≠ ∅)
378, 36sylib 208 . . . . . . . . . . . . . . . . . . . . . . 23 (Lim (rank‘(𝐴 × 𝐵)) → (𝐴 × 𝐵) ≠ ∅)
38 unixp 5632 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 × 𝐵) ≠ ∅ → (𝐴 × 𝐵) = (𝐴𝐵))
3937, 38syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (Lim (rank‘(𝐴 × 𝐵)) → (𝐴 × 𝐵) = (𝐴𝐵))
4039fveq2d 6157 . . . . . . . . . . . . . . . . . . . . 21 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘ (𝐴 × 𝐵)) = (rank‘(𝐴𝐵)))
4131, 40syl5reqr 2670 . . . . . . . . . . . . . . . . . . . 20 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴𝐵)) = (rank‘(𝐴 × 𝐵)))
42 eqimss 3641 . . . . . . . . . . . . . . . . . . . 20 ((rank‘(𝐴𝐵)) = (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
4341, 42syl 17 . . . . . . . . . . . . . . . . . . 19 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
4443adantr 481 . . . . . . . . . . . . . . . . . 18 ((Lim (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴𝐵)) = suc 𝑥) → (rank‘(𝐴𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))
4527, 44eqsstr3d 3624 . . . . . . . . . . . . . . . . 17 ((Lim (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴𝐵)) = suc 𝑥) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
4645adantrr 752 . . . . . . . . . . . . . . . 16 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
47 limuni 5749 . . . . . . . . . . . . . . . . 17 (Lim (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
4847adantr 481 . . . . . . . . . . . . . . . 16 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵)))
4946, 48sseqtr4d 3626 . . . . . . . . . . . . . . 15 ((Lim (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 (rank‘(𝐴 × 𝐵)))
50 vex 3192 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
51 rankon 8610 . . . . . . . . . . . . . . . . . 18 (rank‘(𝐴 × 𝐵)) ∈ On
5251onordi 5796 . . . . . . . . . . . . . . . . 17 Ord (rank‘(𝐴 × 𝐵))
53 orduni 6948 . . . . . . . . . . . . . . . . 17 (Ord (rank‘(𝐴 × 𝐵)) → Ord (rank‘(𝐴 × 𝐵)))
5452, 53ax-mp 5 . . . . . . . . . . . . . . . 16 Ord (rank‘(𝐴 × 𝐵))
55 ordelsuc 6974 . . . . . . . . . . . . . . . 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 7003 . . . . . . . . . . . . . . 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 7003 . . . . . . . . . . . . 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 6976 . . . . . . . . . . . 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 6988 . . . . . . . . . . . 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 6995 . . . . . . . . 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 3031 . . . . 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 3988 . . . . . . . . . . . . . 14 ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴𝐵) = ∅)
81 olc 399 . . . . . . . . . . . . . . 15 (𝐵 = ∅ → (𝐴 = ∅ ∨ 𝐵 = ∅))
8281adantl 482 . . . . . . . . . . . . . 14 ((𝐴 = ∅ ∧ 𝐵 = ∅) → (𝐴 = ∅ ∨ 𝐵 = ∅))
8380, 82sylbir 225 . . . . . . . . . . . . 13 ((𝐴𝐵) = ∅ → (𝐴 = ∅ ∨ 𝐵 = ∅))
84 xpeq0 5518 . . . . . . . . . . . . 13 ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))
8583, 84sylibr 224 . . . . . . . . . . . 12 ((𝐴𝐵) = ∅ → (𝐴 × 𝐵) = ∅)
8685con3i 150 . . . . . . . . . . 11 (¬ (𝐴 × 𝐵) = ∅ → ¬ (𝐴𝐵) = ∅)
8735, 86sylbir 225 . . . . . . . . . 10 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (𝐴𝐵) = ∅)
8819, 20unex 6916 . . . . . . . . . . . 12 (𝐴𝐵) ∈ V
8988rankeq0 8676 . . . . . . . . . . 11 ((𝐴𝐵) = ∅ ↔ (rank‘(𝐴𝐵)) = ∅)
9089notbii 310 . . . . . . . . . 10 (¬ (𝐴𝐵) = ∅ ↔ ¬ (rank‘(𝐴𝐵)) = ∅)
9187, 90sylib 208 . . . . . . . . 9 (¬ (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (rank‘(𝐴𝐵)) = ∅)
929onordi 5796 . . . . . . . . . . 11 Ord (rank‘(𝐴𝐵))
93 ordzsl 6999 . . . . . . . . . . 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 6999 . . . . . . . . . 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 8694 . . . . . . . . . 10 ((Lim (rank‘(𝐴𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴𝐵)))
108106, 107sylan2br 493 . . . . . . . . 9 ((Lim (rank‘(𝐴𝐵)) ∧ ¬ (rank‘(𝐴 × 𝐵)) = ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴𝐵)))
109 limeq 5699 . . . . . . . . 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 2908  Vcvv 3189  cun 3557  wss 3559  c0 3896   cuni 4407   × cxp 5077  Ord word 5686  Oncon0 5687  Lim wlim 5688  suc csuc 5689  cfv 5852  rankcrnk 8578
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 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-reg 8449  ax-inf2 8490
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 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-om 7020  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-r1 8579  df-rank 8580
This theorem is referenced by:  rankxpsuc  8697
  Copyright terms: Public domain W3C validator