Step | Hyp | Ref
| Expression |
1 | | limuni2 6252 |
. 2
⊢ (Lim
(rank‘(𝐴 ×
𝐵)) → Lim ∪ (rank‘(𝐴 × 𝐵))) |
2 | | 0ellim 6253 |
. . . 4
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ∅ ∈ ∪ (rank‘(𝐴 × 𝐵))) |
3 | | n0i 4299 |
. . . 4
⊢ (∅
∈ ∪ (rank‘(𝐴 × 𝐵)) → ¬ ∪
(rank‘(𝐴 ×
𝐵)) =
∅) |
4 | | unieq 4849 |
. . . . . 6
⊢
((rank‘(𝐴
× 𝐵)) = ∅
→ ∪ (rank‘(𝐴 × 𝐵)) = ∪
∅) |
5 | | uni0 4866 |
. . . . . 6
⊢ ∪ ∅ = ∅ |
6 | 4, 5 | syl6eq 2872 |
. . . . 5
⊢
((rank‘(𝐴
× 𝐵)) = ∅
→ ∪ (rank‘(𝐴 × 𝐵)) = ∅) |
7 | 6 | con3i 157 |
. . . 4
⊢ (¬
∪ (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (rank‘(𝐴 × 𝐵)) = ∅) |
8 | 2, 3, 7 | 3syl 18 |
. . 3
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ¬ (rank‘(𝐴 × 𝐵)) = ∅) |
9 | | rankon 9224 |
. . . . . . . . . 10
⊢
(rank‘(𝐴 ∪
𝐵)) ∈
On |
10 | 9 | onsuci 7553 |
. . . . . . . . 9
⊢ suc
(rank‘(𝐴 ∪ 𝐵)) ∈ On |
11 | 10 | onsuci 7553 |
. . . . . . . 8
⊢ suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ On |
12 | 11 | elexi 3513 |
. . . . . . 7
⊢ suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ V |
13 | 12 | sucid 6270 |
. . . . . 6
⊢ suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ suc suc suc
(rank‘(𝐴 ∪ 𝐵)) |
14 | 11 | onsuci 7553 |
. . . . . . . 8
⊢ suc suc
suc (rank‘(𝐴 ∪
𝐵)) ∈
On |
15 | | ontri1 6225 |
. . . . . . . 8
⊢ ((suc suc
suc (rank‘(𝐴 ∪
𝐵)) ∈ On ∧ suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ On) → (suc suc
suc (rank‘(𝐴 ∪
𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵)) ↔ ¬ suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ suc suc suc
(rank‘(𝐴 ∪ 𝐵)))) |
16 | 14, 11, 15 | mp2an 690 |
. . . . . . 7
⊢ (suc suc
suc (rank‘(𝐴 ∪
𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵)) ↔ ¬ suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ suc suc suc
(rank‘(𝐴 ∪ 𝐵))) |
17 | 16 | con2bii 360 |
. . . . . 6
⊢ (suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ suc suc suc
(rank‘(𝐴 ∪ 𝐵)) ↔ ¬ suc suc suc
(rank‘(𝐴 ∪ 𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵))) |
18 | 13, 17 | mpbi 232 |
. . . . 5
⊢ ¬
suc suc suc (rank‘(𝐴
∪ 𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵)) |
19 | | rankxplim.1 |
. . . . . . 7
⊢ 𝐴 ∈ V |
20 | | rankxplim.2 |
. . . . . . 7
⊢ 𝐵 ∈ V |
21 | 19, 20 | rankxpu 9305 |
. . . . . 6
⊢
(rank‘(𝐴
× 𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵)) |
22 | | sstr 3975 |
. . . . . 6
⊢ ((suc suc
suc (rank‘(𝐴 ∪
𝐵)) ⊆
(rank‘(𝐴 ×
𝐵)) ∧
(rank‘(𝐴 ×
𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵))) → suc suc suc
(rank‘(𝐴 ∪ 𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵))) |
23 | 21, 22 | mpan2 689 |
. . . . 5
⊢ (suc suc
suc (rank‘(𝐴 ∪
𝐵)) ⊆
(rank‘(𝐴 ×
𝐵)) → suc suc suc
(rank‘(𝐴 ∪ 𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵))) |
24 | 18, 23 | mto 199 |
. . . 4
⊢ ¬
suc suc suc (rank‘(𝐴
∪ 𝐵)) ⊆
(rank‘(𝐴 ×
𝐵)) |
25 | | reeanv 3367 |
. . . . 5
⊢
(∃𝑥 ∈ On
∃𝑦 ∈ On
((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) ↔ (∃𝑥 ∈ On (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) |
26 | | simprl 769 |
. . . . . . . . . . . . 13
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) |
27 | | simpr 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) → (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) |
28 | | rankuni 9292 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(rank‘∪ ∪
(𝐴 × 𝐵)) = ∪ (rank‘∪ (𝐴 × 𝐵)) |
29 | | rankuni 9292 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(rank‘∪ (𝐴 × 𝐵)) = ∪
(rank‘(𝐴 ×
𝐵)) |
30 | 29 | unieqi 4851 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ (rank‘∪ (𝐴 × 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵)) |
31 | 28, 30 | eqtri 2844 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(rank‘∪ ∪
(𝐴 × 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵)) |
32 | | df-ne 3017 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 × 𝐵) ≠ ∅ ↔ ¬ (𝐴 × 𝐵) = ∅) |
33 | 19, 20 | xpex 7476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 × 𝐵) ∈ V |
34 | 33 | rankeq0 9290 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 × 𝐵) = ∅ ↔ (rank‘(𝐴 × 𝐵)) = ∅) |
35 | 34 | notbii 322 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
(𝐴 × 𝐵) = ∅ ↔ ¬
(rank‘(𝐴 ×
𝐵)) =
∅) |
36 | 32, 35 | bitr2i 278 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ ↔ (𝐴 × 𝐵) ≠ ∅) |
37 | 8, 36 | sylib 220 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (𝐴 × 𝐵) ≠ ∅) |
38 | | unixp 6133 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 × 𝐵) ≠ ∅ → ∪ ∪ (𝐴 × 𝐵) = (𝐴 ∪ 𝐵)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ∪ ∪ (𝐴
× 𝐵) = (𝐴 ∪ 𝐵)) |
40 | 39 | fveq2d 6674 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (rank‘∪ ∪ (𝐴 × 𝐵)) = (rank‘(𝐴 ∪ 𝐵))) |
41 | 31, 40 | syl5reqr 2871 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴 ∪ 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵))) |
42 | | eqimss 4023 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((rank‘(𝐴
∪ 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴 ∪ 𝐵)) ⊆ ∪
∪ (rank‘(𝐴 × 𝐵))) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴 ∪ 𝐵)) ⊆ ∪
∪ (rank‘(𝐴 × 𝐵))) |
44 | 43 | adantr 483 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) → (rank‘(𝐴 ∪ 𝐵)) ⊆ ∪
∪ (rank‘(𝐴 × 𝐵))) |
45 | 27, 44 | eqsstrrd 4006 |
. . . . . . . . . . . . . . . . 17
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) → suc 𝑥 ⊆ ∪ ∪ (rank‘(𝐴 × 𝐵))) |
46 | 45 | adantrr 715 |
. . . . . . . . . . . . . . . 16
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 ⊆ ∪ ∪ (rank‘(𝐴 × 𝐵))) |
47 | | limuni 6251 |
. . . . . . . . . . . . . . . . 17
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ∪
(rank‘(𝐴 ×
𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵))) |
48 | 47 | adantr 483 |
. . . . . . . . . . . . . . . 16
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → ∪
(rank‘(𝐴 ×
𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵))) |
49 | 46, 48 | sseqtrrd 4008 |
. . . . . . . . . . . . . . 15
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 ⊆ ∪
(rank‘(𝐴 ×
𝐵))) |
50 | | vex 3497 |
. . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V |
51 | | rankon 9224 |
. . . . . . . . . . . . . . . . . 18
⊢
(rank‘(𝐴
× 𝐵)) ∈
On |
52 | 51 | onordi 6295 |
. . . . . . . . . . . . . . . . 17
⊢ Ord
(rank‘(𝐴 ×
𝐵)) |
53 | | orduni 7509 |
. . . . . . . . . . . . . . . . 17
⊢ (Ord
(rank‘(𝐴 ×
𝐵)) → Ord ∪ (rank‘(𝐴 × 𝐵))) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ Ord ∪ (rank‘(𝐴 × 𝐵)) |
55 | | ordelsuc 7535 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ V ∧ Ord ∪ (rank‘(𝐴 × 𝐵))) → (𝑥 ∈ ∪
(rank‘(𝐴 ×
𝐵)) ↔ suc 𝑥 ⊆ ∪ (rank‘(𝐴 × 𝐵)))) |
56 | 50, 54, 55 | mp2an 690 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ∪ (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 ⊆ ∪
(rank‘(𝐴 ×
𝐵))) |
57 | 49, 56 | sylibr 236 |
. . . . . . . . . . . . . 14
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → 𝑥 ∈ ∪
(rank‘(𝐴 ×
𝐵))) |
58 | | limsuc 7564 |
. . . . . . . . . . . . . . 15
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (𝑥 ∈ ∪
(rank‘(𝐴 ×
𝐵)) ↔ suc 𝑥 ∈ ∪ (rank‘(𝐴 × 𝐵)))) |
59 | 58 | adantr 483 |
. . . . . . . . . . . . . 14
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (𝑥 ∈ ∪
(rank‘(𝐴 ×
𝐵)) ↔ suc 𝑥 ∈ ∪ (rank‘(𝐴 × 𝐵)))) |
60 | 57, 59 | mpbid 234 |
. . . . . . . . . . . . 13
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 ∈ ∪
(rank‘(𝐴 ×
𝐵))) |
61 | 26, 60 | eqeltrd 2913 |
. . . . . . . . . . . 12
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴 ∪ 𝐵)) ∈ ∪
(rank‘(𝐴 ×
𝐵))) |
62 | | limsuc 7564 |
. . . . . . . . . . . . 13
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ((rank‘(𝐴 ∪ 𝐵)) ∈ ∪
(rank‘(𝐴 ×
𝐵)) ↔ suc
(rank‘(𝐴 ∪ 𝐵)) ∈ ∪ (rank‘(𝐴 × 𝐵)))) |
63 | 62 | adantr 483 |
. . . . . . . . . . . 12
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → ((rank‘(𝐴 ∪ 𝐵)) ∈ ∪
(rank‘(𝐴 ×
𝐵)) ↔ suc
(rank‘(𝐴 ∪ 𝐵)) ∈ ∪ (rank‘(𝐴 × 𝐵)))) |
64 | 61, 63 | mpbid 234 |
. . . . . . . . . . 11
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc (rank‘(𝐴 ∪ 𝐵)) ∈ ∪
(rank‘(𝐴 ×
𝐵))) |
65 | | ordsucelsuc 7537 |
. . . . . . . . . . . 12
⊢ (Ord
∪ (rank‘(𝐴 × 𝐵)) → (suc (rank‘(𝐴 ∪ 𝐵)) ∈ ∪
(rank‘(𝐴 ×
𝐵)) ↔ suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ suc ∪ (rank‘(𝐴 × 𝐵)))) |
66 | 54, 65 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (suc
(rank‘(𝐴 ∪ 𝐵)) ∈ ∪ (rank‘(𝐴 × 𝐵)) ↔ suc suc (rank‘(𝐴 ∪ 𝐵)) ∈ suc ∪
(rank‘(𝐴 ×
𝐵))) |
67 | 64, 66 | sylib 220 |
. . . . . . . . . 10
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc (rank‘(𝐴 ∪ 𝐵)) ∈ suc ∪
(rank‘(𝐴 ×
𝐵))) |
68 | | onsucuni2 7549 |
. . . . . . . . . . . 12
⊢
(((rank‘(𝐴
× 𝐵)) ∈ On ∧
(rank‘(𝐴 ×
𝐵)) = suc 𝑦) → suc ∪ (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))) |
69 | 51, 68 | mpan 688 |
. . . . . . . . . . 11
⊢
((rank‘(𝐴
× 𝐵)) = suc 𝑦 → suc ∪ (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))) |
70 | 69 | ad2antll 727 |
. . . . . . . . . 10
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc ∪
(rank‘(𝐴 ×
𝐵)) = (rank‘(𝐴 × 𝐵))) |
71 | 67, 70 | eleqtrd 2915 |
. . . . . . . . 9
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc (rank‘(𝐴 ∪ 𝐵)) ∈ (rank‘(𝐴 × 𝐵))) |
72 | 11, 51 | onsucssi 7556 |
. . . . . . . . 9
⊢ (suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ (rank‘(𝐴 × 𝐵)) ↔ suc suc suc (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵))) |
73 | 71, 72 | sylib 220 |
. . . . . . . 8
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc suc (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵))) |
74 | 73 | ex 415 |
. . . . . . 7
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))) |
75 | 74 | a1d 25 |
. . . . . 6
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵))))) |
76 | 75 | rexlimdvv 3293 |
. . . . 5
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (∃𝑥 ∈ On ∃𝑦 ∈ On ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))) |
77 | 25, 76 | syl5bir 245 |
. . . 4
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ((∃𝑥 ∈ On (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))) |
78 | 24, 77 | mtoi 201 |
. . 3
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ¬ (∃𝑥 ∈ On (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) |
79 | | ianor 978 |
. . . . . 6
⊢ (¬
(∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) ↔ (¬ ∃𝑥 ∈ On (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∨ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) |
80 | | un00 4394 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 ∪ 𝐵) = ∅) |
81 | | animorl 974 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → (𝐴 = ∅ ∨ 𝐵 = ∅)) |
82 | 80, 81 | sylbir 237 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∪ 𝐵) = ∅ → (𝐴 = ∅ ∨ 𝐵 = ∅)) |
83 | | xpeq0 6017 |
. . . . . . . . . . . . 13
⊢ ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅)) |
84 | 82, 83 | sylibr 236 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∪ 𝐵) = ∅ → (𝐴 × 𝐵) = ∅) |
85 | 84 | con3i 157 |
. . . . . . . . . . 11
⊢ (¬
(𝐴 × 𝐵) = ∅ → ¬ (𝐴 ∪ 𝐵) = ∅) |
86 | 35, 85 | sylbir 237 |
. . . . . . . . . 10
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → ¬
(𝐴 ∪ 𝐵) = ∅) |
87 | 19, 20 | unex 7469 |
. . . . . . . . . . . 12
⊢ (𝐴 ∪ 𝐵) ∈ V |
88 | 87 | rankeq0 9290 |
. . . . . . . . . . 11
⊢ ((𝐴 ∪ 𝐵) = ∅ ↔ (rank‘(𝐴 ∪ 𝐵)) = ∅) |
89 | 88 | notbii 322 |
. . . . . . . . . 10
⊢ (¬
(𝐴 ∪ 𝐵) = ∅ ↔ ¬ (rank‘(𝐴 ∪ 𝐵)) = ∅) |
90 | 86, 89 | sylib 220 |
. . . . . . . . 9
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → ¬
(rank‘(𝐴 ∪ 𝐵)) = ∅) |
91 | 9 | onordi 6295 |
. . . . . . . . . . 11
⊢ Ord
(rank‘(𝐴 ∪ 𝐵)) |
92 | | ordzsl 7560 |
. . . . . . . . . . 11
⊢ (Ord
(rank‘(𝐴 ∪ 𝐵)) ↔ ((rank‘(𝐴 ∪ 𝐵)) = ∅ ∨ ∃𝑥 ∈ On (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 ∪ 𝐵)))) |
93 | 91, 92 | mpbi 232 |
. . . . . . . . . 10
⊢
((rank‘(𝐴
∪ 𝐵)) = ∅ ∨
∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 ∪ 𝐵))) |
94 | 93 | 3ori 1420 |
. . . . . . . . 9
⊢ ((¬
(rank‘(𝐴 ∪ 𝐵)) = ∅ ∧ ¬
∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) → Lim (rank‘(𝐴 ∪ 𝐵))) |
95 | 90, 94 | sylan 582 |
. . . . . . . 8
⊢ ((¬
(rank‘(𝐴 ×
𝐵)) = ∅ ∧ ¬
∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) → Lim (rank‘(𝐴 ∪ 𝐵))) |
96 | 95 | ex 415 |
. . . . . . 7
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → (¬
∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 → Lim (rank‘(𝐴 ∪ 𝐵)))) |
97 | | ordzsl 7560 |
. . . . . . . . . 10
⊢ (Ord
(rank‘(𝐴 ×
𝐵)) ↔
((rank‘(𝐴 ×
𝐵)) = ∅ ∨
∃𝑦 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑦 ∨ Lim (rank‘(𝐴 × 𝐵)))) |
98 | 52, 97 | mpbi 232 |
. . . . . . . . 9
⊢
((rank‘(𝐴
× 𝐵)) = ∅ ∨
∃𝑦 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑦 ∨ Lim (rank‘(𝐴 × 𝐵))) |
99 | 98 | 3ori 1420 |
. . . . . . . 8
⊢ ((¬
(rank‘(𝐴 ×
𝐵)) = ∅ ∧ ¬
∃𝑦 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑦) → Lim (rank‘(𝐴 × 𝐵))) |
100 | 99 | ex 415 |
. . . . . . 7
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → (¬
∃𝑦 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑦 → Lim (rank‘(𝐴 × 𝐵)))) |
101 | 96, 100 | orim12d 961 |
. . . . . 6
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ →
((¬ ∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∨ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → (Lim (rank‘(𝐴 ∪ 𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))))) |
102 | 79, 101 | syl5bi 244 |
. . . . 5
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → (¬
(∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → (Lim (rank‘(𝐴 ∪ 𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))))) |
103 | 102 | imp 409 |
. . . 4
⊢ ((¬
(rank‘(𝐴 ×
𝐵)) = ∅ ∧ ¬
(∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (Lim (rank‘(𝐴 ∪ 𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵)))) |
104 | | simpl 485 |
. . . . . . . 8
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ ¬
(rank‘(𝐴 ×
𝐵)) = ∅) → Lim
(rank‘(𝐴 ∪ 𝐵))) |
105 | 34 | necon3abii 3062 |
. . . . . . . . . 10
⊢ ((𝐴 × 𝐵) ≠ ∅ ↔ ¬
(rank‘(𝐴 ×
𝐵)) =
∅) |
106 | 19, 20 | rankxplim 9308 |
. . . . . . . . . 10
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 ∪ 𝐵))) |
107 | 105, 106 | sylan2br 596 |
. . . . . . . . 9
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ ¬
(rank‘(𝐴 ×
𝐵)) = ∅) →
(rank‘(𝐴 ×
𝐵)) = (rank‘(𝐴 ∪ 𝐵))) |
108 | | limeq 6203 |
. . . . . . . . 9
⊢
((rank‘(𝐴
× 𝐵)) =
(rank‘(𝐴 ∪ 𝐵)) → (Lim
(rank‘(𝐴 ×
𝐵)) ↔ Lim
(rank‘(𝐴 ∪ 𝐵)))) |
109 | 107, 108 | syl 17 |
. . . . . . . 8
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ ¬
(rank‘(𝐴 ×
𝐵)) = ∅) → (Lim
(rank‘(𝐴 ×
𝐵)) ↔ Lim
(rank‘(𝐴 ∪ 𝐵)))) |
110 | 104, 109 | mpbird 259 |
. . . . . . 7
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ ¬
(rank‘(𝐴 ×
𝐵)) = ∅) → Lim
(rank‘(𝐴 ×
𝐵))) |
111 | 110 | expcom 416 |
. . . . . 6
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → (Lim
(rank‘(𝐴 ∪ 𝐵)) → Lim (rank‘(𝐴 × 𝐵)))) |
112 | | idd 24 |
. . . . . 6
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → (Lim
(rank‘(𝐴 ×
𝐵)) → Lim
(rank‘(𝐴 ×
𝐵)))) |
113 | 111, 112 | jaod 855 |
. . . . 5
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))) → Lim (rank‘(𝐴 × 𝐵)))) |
114 | 113 | adantr 483 |
. . . 4
⊢ ((¬
(rank‘(𝐴 ×
𝐵)) = ∅ ∧ ¬
(∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → ((Lim (rank‘(𝐴 ∪ 𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))) → Lim (rank‘(𝐴 × 𝐵)))) |
115 | 103, 114 | mpd 15 |
. . 3
⊢ ((¬
(rank‘(𝐴 ×
𝐵)) = ∅ ∧ ¬
(∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → Lim (rank‘(𝐴 × 𝐵))) |
116 | 8, 78, 115 | syl2anc 586 |
. 2
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → Lim (rank‘(𝐴 × 𝐵))) |
117 | 1, 116 | impbii 211 |
1
⊢ (Lim
(rank‘(𝐴 ×
𝐵)) ↔ Lim ∪ (rank‘(𝐴 × 𝐵))) |