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

Theorem rankxplim3 9824
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 6384 . 2 (Lim (rankβ€˜(𝐴 Γ— 𝐡)) β†’ Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
2 0ellim 6385 . . . 4 (Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) β†’ βˆ… ∈ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
3 n0i 4298 . . . 4 (βˆ… ∈ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) β†’ Β¬ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…)
4 unieq 4881 . . . . . 6 ((rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… β†’ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆͺ βˆ…)
5 uni0 4901 . . . . . 6 βˆͺ βˆ… = βˆ…
64, 5eqtrdi 2793 . . . . 5 ((rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… β†’ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…)
76con3i 154 . . . 4 (Β¬ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… β†’ Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…)
82, 3, 73syl 18 . . 3 (Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) β†’ Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…)
9 rankon 9738 . . . . . . . . . 10 (rankβ€˜(𝐴 βˆͺ 𝐡)) ∈ On
109onsuci 7779 . . . . . . . . 9 suc (rankβ€˜(𝐴 βˆͺ 𝐡)) ∈ On
1110onsuci 7779 . . . . . . . 8 suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)) ∈ On
1211elexi 3467 . . . . . . 7 suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)) ∈ V
1312sucid 6404 . . . . . 6 suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)) ∈ suc suc suc (rankβ€˜(𝐴 βˆͺ 𝐡))
1411onsuci 7779 . . . . . . . 8 suc suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)) ∈ On
15 ontri1 6356 . . . . . . . 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 691 . . . . . . 7 (suc suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)) βŠ† suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)) ↔ Β¬ suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)) ∈ suc suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)))
1716con2bii 358 . . . . . 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 9819 . . . . . 6 (rankβ€˜(𝐴 Γ— 𝐡)) βŠ† suc suc (rankβ€˜(𝐴 βˆͺ 𝐡))
22 sstr 3957 . . . . . 6 ((suc suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)) βŠ† (rankβ€˜(𝐴 Γ— 𝐡)) ∧ (rankβ€˜(𝐴 Γ— 𝐡)) βŠ† suc suc (rankβ€˜(𝐴 βˆͺ 𝐡))) β†’ suc suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)) βŠ† suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)))
2321, 22mpan2 690 . . . . 5 (suc suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)) βŠ† (rankβ€˜(𝐴 Γ— 𝐡)) β†’ suc suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)) βŠ† suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)))
2418, 23mto 196 . . . 4 Β¬ suc suc suc (rankβ€˜(𝐴 βˆͺ 𝐡)) βŠ† (rankβ€˜(𝐴 Γ— 𝐡))
25 reeanv 3220 . . . . 5 (βˆƒπ‘₯ ∈ On βˆƒπ‘¦ ∈ On ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯ ∧ (rankβ€˜(𝐴 Γ— 𝐡)) = suc 𝑦) ↔ (βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯ ∧ βˆƒπ‘¦ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc 𝑦))
26 simprl 770 . . . . . . . . . . . . 13 ((Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ∧ ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯ ∧ (rankβ€˜(𝐴 Γ— 𝐡)) = suc 𝑦)) β†’ (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯)
27 simpr 486 . . . . . . . . . . . . . . . . . 18 ((Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ∧ (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯) β†’ (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯)
28 df-ne 2945 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴 Γ— 𝐡) β‰  βˆ… ↔ Β¬ (𝐴 Γ— 𝐡) = βˆ…)
2919, 20xpex 7692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴 Γ— 𝐡) ∈ V
3029rankeq0 9804 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴 Γ— 𝐡) = βˆ… ↔ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…)
3130notbii 320 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Β¬ (𝐴 Γ— 𝐡) = βˆ… ↔ Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…)
3228, 31bitr2i 276 . . . . . . . . . . . . . . . . . . . . . . . 24 (Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ↔ (𝐴 Γ— 𝐡) β‰  βˆ…)
338, 32sylib 217 . . . . . . . . . . . . . . . . . . . . . . 23 (Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) β†’ (𝐴 Γ— 𝐡) β‰  βˆ…)
34 unixp 6239 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 Γ— 𝐡) β‰  βˆ… β†’ βˆͺ βˆͺ (𝐴 Γ— 𝐡) = (𝐴 βˆͺ 𝐡))
3533, 34syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) β†’ βˆͺ βˆͺ (𝐴 Γ— 𝐡) = (𝐴 βˆͺ 𝐡))
3635fveq2d 6851 . . . . . . . . . . . . . . . . . . . . 21 (Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) β†’ (rankβ€˜βˆͺ βˆͺ (𝐴 Γ— 𝐡)) = (rankβ€˜(𝐴 βˆͺ 𝐡)))
37 rankuni 9806 . . . . . . . . . . . . . . . . . . . . . 22 (rankβ€˜βˆͺ βˆͺ (𝐴 Γ— 𝐡)) = βˆͺ (rankβ€˜βˆͺ (𝐴 Γ— 𝐡))
38 rankuni 9806 . . . . . . . . . . . . . . . . . . . . . . 23 (rankβ€˜βˆͺ (𝐴 Γ— 𝐡)) = βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))
3938unieqi 4883 . . . . . . . . . . . . . . . . . . . . . 22 βˆͺ (rankβ€˜βˆͺ (𝐴 Γ— 𝐡)) = βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))
4037, 39eqtri 2765 . . . . . . . . . . . . . . . . . . . . 21 (rankβ€˜βˆͺ βˆͺ (𝐴 Γ— 𝐡)) = βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))
4136, 40eqtr3di 2792 . . . . . . . . . . . . . . . . . . . 20 (Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) β†’ (rankβ€˜(𝐴 βˆͺ 𝐡)) = βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
42 eqimss 4005 . . . . . . . . . . . . . . . . . . . 20 ((rankβ€˜(𝐴 βˆͺ 𝐡)) = βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) β†’ (rankβ€˜(𝐴 βˆͺ 𝐡)) βŠ† βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
4341, 42syl 17 . . . . . . . . . . . . . . . . . . 19 (Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) β†’ (rankβ€˜(𝐴 βˆͺ 𝐡)) βŠ† βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
4443adantr 482 . . . . . . . . . . . . . . . . . 18 ((Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ∧ (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯) β†’ (rankβ€˜(𝐴 βˆͺ 𝐡)) βŠ† βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
4527, 44eqsstrrd 3988 . . . . . . . . . . . . . . . . 17 ((Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ∧ (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯) β†’ suc π‘₯ βŠ† βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
4645adantrr 716 . . . . . . . . . . . . . . . 16 ((Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ∧ ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯ ∧ (rankβ€˜(𝐴 Γ— 𝐡)) = suc 𝑦)) β†’ suc π‘₯ βŠ† βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
47 limuni 6383 . . . . . . . . . . . . . . . . 17 (Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) β†’ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
4847adantr 482 . . . . . . . . . . . . . . . 16 ((Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ∧ ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯ ∧ (rankβ€˜(𝐴 Γ— 𝐡)) = suc 𝑦)) β†’ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆͺ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
4946, 48sseqtrrd 3990 . . . . . . . . . . . . . . 15 ((Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ∧ ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯ ∧ (rankβ€˜(𝐴 Γ— 𝐡)) = suc 𝑦)) β†’ suc π‘₯ βŠ† βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
50 vex 3452 . . . . . . . . . . . . . . . 16 π‘₯ ∈ V
51 rankon 9738 . . . . . . . . . . . . . . . . . 18 (rankβ€˜(𝐴 Γ— 𝐡)) ∈ On
5251onordi 6433 . . . . . . . . . . . . . . . . 17 Ord (rankβ€˜(𝐴 Γ— 𝐡))
53 orduni 7729 . . . . . . . . . . . . . . . . 17 (Ord (rankβ€˜(𝐴 Γ— 𝐡)) β†’ Ord βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
5452, 53ax-mp 5 . . . . . . . . . . . . . . . 16 Ord βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))
55 ordelsuc 7760 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ V ∧ Ord βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))) β†’ (π‘₯ ∈ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ↔ suc π‘₯ βŠ† βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))))
5650, 54, 55mp2an 691 . . . . . . . . . . . . . . 15 (π‘₯ ∈ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ↔ suc π‘₯ βŠ† βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
5749, 56sylibr 233 . . . . . . . . . . . . . 14 ((Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ∧ ((rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯ ∧ (rankβ€˜(𝐴 Γ— 𝐡)) = suc 𝑦)) β†’ π‘₯ ∈ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)))
58 limsuc 7790 . . . . . . . . . . . . . . 15 (Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) β†’ (π‘₯ ∈ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ↔ suc π‘₯ ∈ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))))
5958adantr 482 . . . . . . . . . . . . . 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 7790 . . . . . . . . . . . . 13 (Lim βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) β†’ ((rankβ€˜(𝐴 βˆͺ 𝐡)) ∈ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) ↔ suc (rankβ€˜(𝐴 βˆͺ 𝐡)) ∈ βˆͺ (rankβ€˜(𝐴 Γ— 𝐡))))
6362adantr 482 . . . . . . . . . . . 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 7762 . . . . . . . . . . . 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 7774 . . . . . . . . . . . 12 (((rankβ€˜(𝐴 Γ— 𝐡)) ∈ On ∧ (rankβ€˜(𝐴 Γ— 𝐡)) = suc 𝑦) β†’ suc βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = (rankβ€˜(𝐴 Γ— 𝐡)))
6951, 68mpan 689 . . . . . . . . . . 11 ((rankβ€˜(𝐴 Γ— 𝐡)) = suc 𝑦 β†’ suc βˆͺ (rankβ€˜(𝐴 Γ— 𝐡)) = (rankβ€˜(𝐴 Γ— 𝐡)))
7069ad2antll 728 . . . . . . . . . 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 7782 . . . . . . . . 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 414 . . . . . . 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 3205 . . . . 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 981 . . . . . 6 (Β¬ (βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯ ∧ βˆƒπ‘¦ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc 𝑦) ↔ (Β¬ βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯ ∨ Β¬ βˆƒπ‘¦ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc 𝑦))
80 un00 4407 . . . . . . . . . . . . . 14 ((𝐴 = βˆ… ∧ 𝐡 = βˆ…) ↔ (𝐴 βˆͺ 𝐡) = βˆ…)
81 animorl 977 . . . . . . . . . . . . . 14 ((𝐴 = βˆ… ∧ 𝐡 = βˆ…) β†’ (𝐴 = βˆ… ∨ 𝐡 = βˆ…))
8280, 81sylbir 234 . . . . . . . . . . . . 13 ((𝐴 βˆͺ 𝐡) = βˆ… β†’ (𝐴 = βˆ… ∨ 𝐡 = βˆ…))
83 xpeq0 6117 . . . . . . . . . . . . 13 ((𝐴 Γ— 𝐡) = βˆ… ↔ (𝐴 = βˆ… ∨ 𝐡 = βˆ…))
8482, 83sylibr 233 . . . . . . . . . . . 12 ((𝐴 βˆͺ 𝐡) = βˆ… β†’ (𝐴 Γ— 𝐡) = βˆ…)
8584con3i 154 . . . . . . . . . . 11 (Β¬ (𝐴 Γ— 𝐡) = βˆ… β†’ Β¬ (𝐴 βˆͺ 𝐡) = βˆ…)
8631, 85sylbir 234 . . . . . . . . . 10 (Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… β†’ Β¬ (𝐴 βˆͺ 𝐡) = βˆ…)
8719, 20unex 7685 . . . . . . . . . . . 12 (𝐴 βˆͺ 𝐡) ∈ V
8887rankeq0 9804 . . . . . . . . . . 11 ((𝐴 βˆͺ 𝐡) = βˆ… ↔ (rankβ€˜(𝐴 βˆͺ 𝐡)) = βˆ…)
8988notbii 320 . . . . . . . . . 10 (Β¬ (𝐴 βˆͺ 𝐡) = βˆ… ↔ Β¬ (rankβ€˜(𝐴 βˆͺ 𝐡)) = βˆ…)
9086, 89sylib 217 . . . . . . . . 9 (Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… β†’ Β¬ (rankβ€˜(𝐴 βˆͺ 𝐡)) = βˆ…)
919onordi 6433 . . . . . . . . . . 11 Ord (rankβ€˜(𝐴 βˆͺ 𝐡))
92 ordzsl 7786 . . . . . . . . . . 11 (Ord (rankβ€˜(𝐴 βˆͺ 𝐡)) ↔ ((rankβ€˜(𝐴 βˆͺ 𝐡)) = βˆ… ∨ βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯ ∨ Lim (rankβ€˜(𝐴 βˆͺ 𝐡))))
9391, 92mpbi 229 . . . . . . . . . 10 ((rankβ€˜(𝐴 βˆͺ 𝐡)) = βˆ… ∨ βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯ ∨ Lim (rankβ€˜(𝐴 βˆͺ 𝐡)))
94933ori 1425 . . . . . . . . 9 ((Β¬ (rankβ€˜(𝐴 βˆͺ 𝐡)) = βˆ… ∧ Β¬ βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯) β†’ Lim (rankβ€˜(𝐴 βˆͺ 𝐡)))
9590, 94sylan 581 . . . . . . . 8 ((Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∧ Β¬ βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯) β†’ Lim (rankβ€˜(𝐴 βˆͺ 𝐡)))
9695ex 414 . . . . . . 7 (Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… β†’ (Β¬ βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯ β†’ Lim (rankβ€˜(𝐴 βˆͺ 𝐡))))
97 ordzsl 7786 . . . . . . . . . 10 (Ord (rankβ€˜(𝐴 Γ— 𝐡)) ↔ ((rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ βˆƒπ‘¦ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc 𝑦 ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡))))
9852, 97mpbi 229 . . . . . . . . 9 ((rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∨ βˆƒπ‘¦ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc 𝑦 ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡)))
99983ori 1425 . . . . . . . 8 ((Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∧ Β¬ βˆƒπ‘¦ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc 𝑦) β†’ Lim (rankβ€˜(𝐴 Γ— 𝐡)))
10099ex 414 . . . . . . 7 (Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… β†’ (Β¬ βˆƒπ‘¦ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc 𝑦 β†’ Lim (rankβ€˜(𝐴 Γ— 𝐡))))
10196, 100orim12d 964 . . . . . 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 408 . . . 4 ((Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… ∧ Β¬ (βˆƒπ‘₯ ∈ On (rankβ€˜(𝐴 βˆͺ 𝐡)) = suc π‘₯ ∧ βˆƒπ‘¦ ∈ On (rankβ€˜(𝐴 Γ— 𝐡)) = suc 𝑦)) β†’ (Lim (rankβ€˜(𝐴 βˆͺ 𝐡)) ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡))))
104 simpl 484 . . . . . . . 8 ((Lim (rankβ€˜(𝐴 βˆͺ 𝐡)) ∧ Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…) β†’ Lim (rankβ€˜(𝐴 βˆͺ 𝐡)))
10530necon3abii 2991 . . . . . . . . . 10 ((𝐴 Γ— 𝐡) β‰  βˆ… ↔ Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…)
10619, 20rankxplim 9822 . . . . . . . . . 10 ((Lim (rankβ€˜(𝐴 βˆͺ 𝐡)) ∧ (𝐴 Γ— 𝐡) β‰  βˆ…) β†’ (rankβ€˜(𝐴 Γ— 𝐡)) = (rankβ€˜(𝐴 βˆͺ 𝐡)))
107105, 106sylan2br 596 . . . . . . . . 9 ((Lim (rankβ€˜(𝐴 βˆͺ 𝐡)) ∧ Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ…) β†’ (rankβ€˜(𝐴 Γ— 𝐡)) = (rankβ€˜(𝐴 βˆͺ 𝐡)))
108 limeq 6334 . . . . . . . . 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 415 . . . . . 6 (Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… β†’ (Lim (rankβ€˜(𝐴 βˆͺ 𝐡)) β†’ Lim (rankβ€˜(𝐴 Γ— 𝐡))))
112 idd 24 . . . . . 6 (Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… β†’ (Lim (rankβ€˜(𝐴 Γ— 𝐡)) β†’ Lim (rankβ€˜(𝐴 Γ— 𝐡))))
113111, 112jaod 858 . . . . 5 (Β¬ (rankβ€˜(𝐴 Γ— 𝐡)) = βˆ… β†’ ((Lim (rankβ€˜(𝐴 βˆͺ 𝐡)) ∨ Lim (rankβ€˜(𝐴 Γ— 𝐡))) β†’ Lim (rankβ€˜(𝐴 Γ— 𝐡))))
114113adantr 482 . . . 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 585 . 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 397   ∨ wo 846   ∨ w3o 1087   = wceq 1542   ∈ wcel 2107   β‰  wne 2944  βˆƒwrex 3074  Vcvv 3448   βˆͺ cun 3913   βŠ† wss 3915  βˆ…c0 4287  βˆͺ cuni 4870   Γ— cxp 5636  Ord word 6321  Oncon0 6322  Lim wlim 6323  suc csuc 6324  β€˜cfv 6501  rankcrnk 9706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-reg 9535  ax-inf2 9584
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-om 7808  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-r1 9707  df-rank 9708
This theorem is referenced by:  rankxpsuc  9825
  Copyright terms: Public domain W3C validator