Step | Hyp | Ref
| Expression |
1 | | limuni2 6320 |
. 2
⊢ (Lim
(rank‘(𝐴 ×
𝐵)) → Lim ∪ (rank‘(𝐴 × 𝐵))) |
2 | | 0ellim 6321 |
. . . 4
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ∅ ∈ ∪ (rank‘(𝐴 × 𝐵))) |
3 | | n0i 4267 |
. . . 4
⊢ (∅
∈ ∪ (rank‘(𝐴 × 𝐵)) → ¬ ∪
(rank‘(𝐴 ×
𝐵)) =
∅) |
4 | | unieq 4850 |
. . . . . 6
⊢
((rank‘(𝐴
× 𝐵)) = ∅
→ ∪ (rank‘(𝐴 × 𝐵)) = ∪
∅) |
5 | | uni0 4869 |
. . . . . 6
⊢ ∪ ∅ = ∅ |
6 | 4, 5 | eqtrdi 2794 |
. . . . 5
⊢
((rank‘(𝐴
× 𝐵)) = ∅
→ ∪ (rank‘(𝐴 × 𝐵)) = ∅) |
7 | 6 | con3i 154 |
. . . 4
⊢ (¬
∪ (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (rank‘(𝐴 × 𝐵)) = ∅) |
8 | 2, 3, 7 | 3syl 18 |
. . 3
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ¬ (rank‘(𝐴 × 𝐵)) = ∅) |
9 | | rankon 9563 |
. . . . . . . . . 10
⊢
(rank‘(𝐴 ∪
𝐵)) ∈
On |
10 | 9 | onsuci 7675 |
. . . . . . . . 9
⊢ suc
(rank‘(𝐴 ∪ 𝐵)) ∈ On |
11 | 10 | onsuci 7675 |
. . . . . . . 8
⊢ suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ On |
12 | 11 | elexi 3448 |
. . . . . . 7
⊢ suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ V |
13 | 12 | sucid 6338 |
. . . . . 6
⊢ suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ suc suc suc
(rank‘(𝐴 ∪ 𝐵)) |
14 | 11 | onsuci 7675 |
. . . . . . . 8
⊢ suc suc
suc (rank‘(𝐴 ∪
𝐵)) ∈
On |
15 | | ontri1 6293 |
. . . . . . . 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 689 |
. . . . . . 7
⊢ (suc suc
suc (rank‘(𝐴 ∪
𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵)) ↔ ¬ suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ suc suc suc
(rank‘(𝐴 ∪ 𝐵))) |
17 | 16 | con2bii 358 |
. . . . . 6
⊢ (suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ suc suc suc
(rank‘(𝐴 ∪ 𝐵)) ↔ ¬ suc suc suc
(rank‘(𝐴 ∪ 𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵))) |
18 | 13, 17 | mpbi 229 |
. . . . 5
⊢ ¬
suc suc suc (rank‘(𝐴
∪ 𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵)) |
19 | | rankxplim.1 |
. . . . . . 7
⊢ 𝐴 ∈ V |
20 | | rankxplim.2 |
. . . . . . 7
⊢ 𝐵 ∈ V |
21 | 19, 20 | rankxpu 9644 |
. . . . . 6
⊢
(rank‘(𝐴
× 𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵)) |
22 | | sstr 3928 |
. . . . . 6
⊢ ((suc suc
suc (rank‘(𝐴 ∪
𝐵)) ⊆
(rank‘(𝐴 ×
𝐵)) ∧
(rank‘(𝐴 ×
𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵))) → suc suc suc
(rank‘(𝐴 ∪ 𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵))) |
23 | 21, 22 | mpan2 688 |
. . . . 5
⊢ (suc suc
suc (rank‘(𝐴 ∪
𝐵)) ⊆
(rank‘(𝐴 ×
𝐵)) → suc suc suc
(rank‘(𝐴 ∪ 𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵))) |
24 | 18, 23 | mto 196 |
. . . 4
⊢ ¬
suc suc suc (rank‘(𝐴
∪ 𝐵)) ⊆
(rank‘(𝐴 ×
𝐵)) |
25 | | reeanv 3292 |
. . . . 5
⊢
(∃𝑥 ∈ On
∃𝑦 ∈ On
((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) ↔ (∃𝑥 ∈ On (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) |
26 | | simprl 768 |
. . . . . . . . . . . . 13
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) |
27 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) → (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) |
28 | | df-ne 2944 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 × 𝐵) ≠ ∅ ↔ ¬ (𝐴 × 𝐵) = ∅) |
29 | 19, 20 | xpex 7593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 × 𝐵) ∈ V |
30 | 29 | rankeq0 9629 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 × 𝐵) = ∅ ↔ (rank‘(𝐴 × 𝐵)) = ∅) |
31 | 30 | notbii 320 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
(𝐴 × 𝐵) = ∅ ↔ ¬
(rank‘(𝐴 ×
𝐵)) =
∅) |
32 | 28, 31 | bitr2i 275 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ ↔ (𝐴 × 𝐵) ≠ ∅) |
33 | 8, 32 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (𝐴 × 𝐵) ≠ ∅) |
34 | | unixp 6178 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 × 𝐵) ≠ ∅ → ∪ ∪ (𝐴 × 𝐵) = (𝐴 ∪ 𝐵)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ∪ ∪ (𝐴
× 𝐵) = (𝐴 ∪ 𝐵)) |
36 | 35 | fveq2d 6770 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (rank‘∪ ∪ (𝐴 × 𝐵)) = (rank‘(𝐴 ∪ 𝐵))) |
37 | | rankuni 9631 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(rank‘∪ ∪
(𝐴 × 𝐵)) = ∪ (rank‘∪ (𝐴 × 𝐵)) |
38 | | rankuni 9631 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(rank‘∪ (𝐴 × 𝐵)) = ∪
(rank‘(𝐴 ×
𝐵)) |
39 | 38 | unieqi 4852 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ (rank‘∪ (𝐴 × 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵)) |
40 | 37, 39 | eqtri 2766 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(rank‘∪ ∪
(𝐴 × 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵)) |
41 | 36, 40 | eqtr3di 2793 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴 ∪ 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵))) |
42 | | eqimss 3976 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((rank‘(𝐴
∪ 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴 ∪ 𝐵)) ⊆ ∪
∪ (rank‘(𝐴 × 𝐵))) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴 ∪ 𝐵)) ⊆ ∪
∪ (rank‘(𝐴 × 𝐵))) |
44 | 43 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) → (rank‘(𝐴 ∪ 𝐵)) ⊆ ∪
∪ (rank‘(𝐴 × 𝐵))) |
45 | 27, 44 | eqsstrrd 3959 |
. . . . . . . . . . . . . . . . 17
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) → suc 𝑥 ⊆ ∪ ∪ (rank‘(𝐴 × 𝐵))) |
46 | 45 | adantrr 714 |
. . . . . . . . . . . . . . . 16
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 ⊆ ∪ ∪ (rank‘(𝐴 × 𝐵))) |
47 | | limuni 6319 |
. . . . . . . . . . . . . . . . 17
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ∪
(rank‘(𝐴 ×
𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵))) |
48 | 47 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → ∪
(rank‘(𝐴 ×
𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵))) |
49 | 46, 48 | sseqtrrd 3961 |
. . . . . . . . . . . . . . 15
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 ⊆ ∪
(rank‘(𝐴 ×
𝐵))) |
50 | | vex 3433 |
. . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V |
51 | | rankon 9563 |
. . . . . . . . . . . . . . . . . 18
⊢
(rank‘(𝐴
× 𝐵)) ∈
On |
52 | 51 | onordi 6364 |
. . . . . . . . . . . . . . . . 17
⊢ Ord
(rank‘(𝐴 ×
𝐵)) |
53 | | orduni 7629 |
. . . . . . . . . . . . . . . . 17
⊢ (Ord
(rank‘(𝐴 ×
𝐵)) → Ord ∪ (rank‘(𝐴 × 𝐵))) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ Ord ∪ (rank‘(𝐴 × 𝐵)) |
55 | | ordelsuc 7657 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ V ∧ Ord ∪ (rank‘(𝐴 × 𝐵))) → (𝑥 ∈ ∪
(rank‘(𝐴 ×
𝐵)) ↔ suc 𝑥 ⊆ ∪ (rank‘(𝐴 × 𝐵)))) |
56 | 50, 54, 55 | mp2an 689 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ∪ (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 ⊆ ∪
(rank‘(𝐴 ×
𝐵))) |
57 | 49, 56 | sylibr 233 |
. . . . . . . . . . . . . 14
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → 𝑥 ∈ ∪
(rank‘(𝐴 ×
𝐵))) |
58 | | limsuc 7686 |
. . . . . . . . . . . . . . 15
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (𝑥 ∈ ∪
(rank‘(𝐴 ×
𝐵)) ↔ suc 𝑥 ∈ ∪ (rank‘(𝐴 × 𝐵)))) |
59 | 58 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (𝑥 ∈ ∪
(rank‘(𝐴 ×
𝐵)) ↔ suc 𝑥 ∈ ∪ (rank‘(𝐴 × 𝐵)))) |
60 | 57, 59 | mpbid 231 |
. . . . . . . . . . . . 13
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 ∈ ∪
(rank‘(𝐴 ×
𝐵))) |
61 | 26, 60 | eqeltrd 2839 |
. . . . . . . . . . . 12
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴 ∪ 𝐵)) ∈ ∪
(rank‘(𝐴 ×
𝐵))) |
62 | | limsuc 7686 |
. . . . . . . . . . . . 13
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ((rank‘(𝐴 ∪ 𝐵)) ∈ ∪
(rank‘(𝐴 ×
𝐵)) ↔ suc
(rank‘(𝐴 ∪ 𝐵)) ∈ ∪ (rank‘(𝐴 × 𝐵)))) |
63 | 62 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → ((rank‘(𝐴 ∪ 𝐵)) ∈ ∪
(rank‘(𝐴 ×
𝐵)) ↔ suc
(rank‘(𝐴 ∪ 𝐵)) ∈ ∪ (rank‘(𝐴 × 𝐵)))) |
64 | 61, 63 | mpbid 231 |
. . . . . . . . . . 11
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc (rank‘(𝐴 ∪ 𝐵)) ∈ ∪
(rank‘(𝐴 ×
𝐵))) |
65 | | ordsucelsuc 7659 |
. . . . . . . . . . . 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 217 |
. . . . . . . . . 10
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc (rank‘(𝐴 ∪ 𝐵)) ∈ suc ∪
(rank‘(𝐴 ×
𝐵))) |
68 | | onsucuni2 7671 |
. . . . . . . . . . . 12
⊢
(((rank‘(𝐴
× 𝐵)) ∈ On ∧
(rank‘(𝐴 ×
𝐵)) = suc 𝑦) → suc ∪ (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))) |
69 | 51, 68 | mpan 687 |
. . . . . . . . . . 11
⊢
((rank‘(𝐴
× 𝐵)) = suc 𝑦 → suc ∪ (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))) |
70 | 69 | ad2antll 726 |
. . . . . . . . . 10
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc ∪
(rank‘(𝐴 ×
𝐵)) = (rank‘(𝐴 × 𝐵))) |
71 | 67, 70 | eleqtrd 2841 |
. . . . . . . . 9
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc (rank‘(𝐴 ∪ 𝐵)) ∈ (rank‘(𝐴 × 𝐵))) |
72 | 11, 51 | onsucssi 7678 |
. . . . . . . . 9
⊢ (suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ (rank‘(𝐴 × 𝐵)) ↔ suc suc suc (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵))) |
73 | 71, 72 | sylib 217 |
. . . . . . . 8
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc suc (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵))) |
74 | 73 | ex 413 |
. . . . . . 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 3220 |
. . . . 5
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (∃𝑥 ∈ On ∃𝑦 ∈ On ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))) |
77 | 25, 76 | syl5bir 242 |
. . . 4
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ((∃𝑥 ∈ On (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))) |
78 | 24, 77 | mtoi 198 |
. . 3
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ¬ (∃𝑥 ∈ On (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) |
79 | | ianor 979 |
. . . . . 6
⊢ (¬
(∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) ↔ (¬ ∃𝑥 ∈ On (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∨ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) |
80 | | un00 4376 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 ∪ 𝐵) = ∅) |
81 | | animorl 975 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → (𝐴 = ∅ ∨ 𝐵 = ∅)) |
82 | 80, 81 | sylbir 234 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∪ 𝐵) = ∅ → (𝐴 = ∅ ∨ 𝐵 = ∅)) |
83 | | xpeq0 6056 |
. . . . . . . . . . . . 13
⊢ ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅)) |
84 | 82, 83 | sylibr 233 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∪ 𝐵) = ∅ → (𝐴 × 𝐵) = ∅) |
85 | 84 | con3i 154 |
. . . . . . . . . . 11
⊢ (¬
(𝐴 × 𝐵) = ∅ → ¬ (𝐴 ∪ 𝐵) = ∅) |
86 | 31, 85 | sylbir 234 |
. . . . . . . . . 10
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → ¬
(𝐴 ∪ 𝐵) = ∅) |
87 | 19, 20 | unex 7586 |
. . . . . . . . . . . 12
⊢ (𝐴 ∪ 𝐵) ∈ V |
88 | 87 | rankeq0 9629 |
. . . . . . . . . . 11
⊢ ((𝐴 ∪ 𝐵) = ∅ ↔ (rank‘(𝐴 ∪ 𝐵)) = ∅) |
89 | 88 | notbii 320 |
. . . . . . . . . 10
⊢ (¬
(𝐴 ∪ 𝐵) = ∅ ↔ ¬ (rank‘(𝐴 ∪ 𝐵)) = ∅) |
90 | 86, 89 | sylib 217 |
. . . . . . . . 9
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → ¬
(rank‘(𝐴 ∪ 𝐵)) = ∅) |
91 | 9 | onordi 6364 |
. . . . . . . . . . 11
⊢ Ord
(rank‘(𝐴 ∪ 𝐵)) |
92 | | ordzsl 7682 |
. . . . . . . . . . 11
⊢ (Ord
(rank‘(𝐴 ∪ 𝐵)) ↔ ((rank‘(𝐴 ∪ 𝐵)) = ∅ ∨ ∃𝑥 ∈ On (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 ∪ 𝐵)))) |
93 | 91, 92 | mpbi 229 |
. . . . . . . . . 10
⊢
((rank‘(𝐴
∪ 𝐵)) = ∅ ∨
∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 ∪ 𝐵))) |
94 | 93 | 3ori 1423 |
. . . . . . . . 9
⊢ ((¬
(rank‘(𝐴 ∪ 𝐵)) = ∅ ∧ ¬
∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) → Lim (rank‘(𝐴 ∪ 𝐵))) |
95 | 90, 94 | sylan 580 |
. . . . . . . 8
⊢ ((¬
(rank‘(𝐴 ×
𝐵)) = ∅ ∧ ¬
∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) → Lim (rank‘(𝐴 ∪ 𝐵))) |
96 | 95 | ex 413 |
. . . . . . 7
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → (¬
∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 → Lim (rank‘(𝐴 ∪ 𝐵)))) |
97 | | ordzsl 7682 |
. . . . . . . . . 10
⊢ (Ord
(rank‘(𝐴 ×
𝐵)) ↔
((rank‘(𝐴 ×
𝐵)) = ∅ ∨
∃𝑦 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑦 ∨ Lim (rank‘(𝐴 × 𝐵)))) |
98 | 52, 97 | mpbi 229 |
. . . . . . . . 9
⊢
((rank‘(𝐴
× 𝐵)) = ∅ ∨
∃𝑦 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑦 ∨ Lim (rank‘(𝐴 × 𝐵))) |
99 | 98 | 3ori 1423 |
. . . . . . . 8
⊢ ((¬
(rank‘(𝐴 ×
𝐵)) = ∅ ∧ ¬
∃𝑦 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑦) → Lim (rank‘(𝐴 × 𝐵))) |
100 | 99 | ex 413 |
. . . . . . 7
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → (¬
∃𝑦 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑦 → Lim (rank‘(𝐴 × 𝐵)))) |
101 | 96, 100 | orim12d 962 |
. . . . . 6
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ →
((¬ ∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∨ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → (Lim (rank‘(𝐴 ∪ 𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))))) |
102 | 79, 101 | syl5bi 241 |
. . . . 5
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → (¬
(∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → (Lim (rank‘(𝐴 ∪ 𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))))) |
103 | 102 | imp 407 |
. . . 4
⊢ ((¬
(rank‘(𝐴 ×
𝐵)) = ∅ ∧ ¬
(∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (Lim (rank‘(𝐴 ∪ 𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵)))) |
104 | | simpl 483 |
. . . . . . . 8
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ ¬
(rank‘(𝐴 ×
𝐵)) = ∅) → Lim
(rank‘(𝐴 ∪ 𝐵))) |
105 | 30 | necon3abii 2990 |
. . . . . . . . . 10
⊢ ((𝐴 × 𝐵) ≠ ∅ ↔ ¬
(rank‘(𝐴 ×
𝐵)) =
∅) |
106 | 19, 20 | rankxplim 9647 |
. . . . . . . . . 10
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 ∪ 𝐵))) |
107 | 105, 106 | sylan2br 595 |
. . . . . . . . 9
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ ¬
(rank‘(𝐴 ×
𝐵)) = ∅) →
(rank‘(𝐴 ×
𝐵)) = (rank‘(𝐴 ∪ 𝐵))) |
108 | | limeq 6271 |
. . . . . . . . 9
⊢
((rank‘(𝐴
× 𝐵)) =
(rank‘(𝐴 ∪ 𝐵)) → (Lim
(rank‘(𝐴 ×
𝐵)) ↔ Lim
(rank‘(𝐴 ∪ 𝐵)))) |
109 | 107, 108 | syl 17 |
. . . . . . . 8
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ ¬
(rank‘(𝐴 ×
𝐵)) = ∅) → (Lim
(rank‘(𝐴 ×
𝐵)) ↔ Lim
(rank‘(𝐴 ∪ 𝐵)))) |
110 | 104, 109 | mpbird 256 |
. . . . . . 7
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ ¬
(rank‘(𝐴 ×
𝐵)) = ∅) → Lim
(rank‘(𝐴 ×
𝐵))) |
111 | 110 | expcom 414 |
. . . . . 6
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → (Lim
(rank‘(𝐴 ∪ 𝐵)) → Lim (rank‘(𝐴 × 𝐵)))) |
112 | | idd 24 |
. . . . . 6
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → (Lim
(rank‘(𝐴 ×
𝐵)) → Lim
(rank‘(𝐴 ×
𝐵)))) |
113 | 111, 112 | jaod 856 |
. . . . 5
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))) → Lim (rank‘(𝐴 × 𝐵)))) |
114 | 113 | adantr 481 |
. . . 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 584 |
. 2
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → Lim (rank‘(𝐴 × 𝐵))) |
117 | 1, 116 | impbii 208 |
1
⊢ (Lim
(rank‘(𝐴 ×
𝐵)) ↔ Lim ∪ (rank‘(𝐴 × 𝐵))) |