| Step | Hyp | Ref
| Expression |
| 1 | | limuni2 6446 |
. 2
⊢ (Lim
(rank‘(𝐴 ×
𝐵)) → Lim ∪ (rank‘(𝐴 × 𝐵))) |
| 2 | | 0ellim 6447 |
. . . 4
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ∅ ∈ ∪ (rank‘(𝐴 × 𝐵))) |
| 3 | | n0i 4340 |
. . . 4
⊢ (∅
∈ ∪ (rank‘(𝐴 × 𝐵)) → ¬ ∪
(rank‘(𝐴 ×
𝐵)) =
∅) |
| 4 | | unieq 4918 |
. . . . . 6
⊢
((rank‘(𝐴
× 𝐵)) = ∅
→ ∪ (rank‘(𝐴 × 𝐵)) = ∪
∅) |
| 5 | | uni0 4935 |
. . . . . 6
⊢ ∪ ∅ = ∅ |
| 6 | 4, 5 | eqtrdi 2793 |
. . . . 5
⊢
((rank‘(𝐴
× 𝐵)) = ∅
→ ∪ (rank‘(𝐴 × 𝐵)) = ∅) |
| 7 | 6 | con3i 154 |
. . . 4
⊢ (¬
∪ (rank‘(𝐴 × 𝐵)) = ∅ → ¬ (rank‘(𝐴 × 𝐵)) = ∅) |
| 8 | 2, 3, 7 | 3syl 18 |
. . 3
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ¬ (rank‘(𝐴 × 𝐵)) = ∅) |
| 9 | | rankon 9835 |
. . . . . . . . . 10
⊢
(rank‘(𝐴 ∪
𝐵)) ∈
On |
| 10 | 9 | onsuci 7859 |
. . . . . . . . 9
⊢ suc
(rank‘(𝐴 ∪ 𝐵)) ∈ On |
| 11 | 10 | onsuci 7859 |
. . . . . . . 8
⊢ suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ On |
| 12 | 11 | elexi 3503 |
. . . . . . 7
⊢ suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ V |
| 13 | 12 | sucid 6466 |
. . . . . 6
⊢ suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ suc suc suc
(rank‘(𝐴 ∪ 𝐵)) |
| 14 | 11 | onsuci 7859 |
. . . . . . . 8
⊢ suc suc
suc (rank‘(𝐴 ∪
𝐵)) ∈
On |
| 15 | | ontri1 6418 |
. . . . . . . 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 692 |
. . . . . . 7
⊢ (suc suc
suc (rank‘(𝐴 ∪
𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵)) ↔ ¬ suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ suc suc suc
(rank‘(𝐴 ∪ 𝐵))) |
| 17 | 16 | con2bii 357 |
. . . . . 6
⊢ (suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ suc suc suc
(rank‘(𝐴 ∪ 𝐵)) ↔ ¬ suc suc suc
(rank‘(𝐴 ∪ 𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵))) |
| 18 | 13, 17 | mpbi 230 |
. . . . 5
⊢ ¬
suc suc suc (rank‘(𝐴
∪ 𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵)) |
| 19 | | rankxplim.1 |
. . . . . . 7
⊢ 𝐴 ∈ V |
| 20 | | rankxplim.2 |
. . . . . . 7
⊢ 𝐵 ∈ V |
| 21 | 19, 20 | rankxpu 9916 |
. . . . . 6
⊢
(rank‘(𝐴
× 𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵)) |
| 22 | | sstr 3992 |
. . . . . 6
⊢ ((suc suc
suc (rank‘(𝐴 ∪
𝐵)) ⊆
(rank‘(𝐴 ×
𝐵)) ∧
(rank‘(𝐴 ×
𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵))) → suc suc suc
(rank‘(𝐴 ∪ 𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵))) |
| 23 | 21, 22 | mpan2 691 |
. . . . 5
⊢ (suc suc
suc (rank‘(𝐴 ∪
𝐵)) ⊆
(rank‘(𝐴 ×
𝐵)) → suc suc suc
(rank‘(𝐴 ∪ 𝐵)) ⊆ suc suc
(rank‘(𝐴 ∪ 𝐵))) |
| 24 | 18, 23 | mto 197 |
. . . 4
⊢ ¬
suc suc suc (rank‘(𝐴
∪ 𝐵)) ⊆
(rank‘(𝐴 ×
𝐵)) |
| 25 | | reeanv 3229 |
. . . . 5
⊢
(∃𝑥 ∈ On
∃𝑦 ∈ On
((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) ↔ (∃𝑥 ∈ On (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) |
| 26 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) |
| 27 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) → (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) |
| 28 | | df-ne 2941 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 × 𝐵) ≠ ∅ ↔ ¬ (𝐴 × 𝐵) = ∅) |
| 29 | 19, 20 | xpex 7773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 × 𝐵) ∈ V |
| 30 | 29 | rankeq0 9901 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 × 𝐵) = ∅ ↔ (rank‘(𝐴 × 𝐵)) = ∅) |
| 31 | 30 | notbii 320 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
(𝐴 × 𝐵) = ∅ ↔ ¬
(rank‘(𝐴 ×
𝐵)) =
∅) |
| 32 | 28, 31 | bitr2i 276 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ ↔ (𝐴 × 𝐵) ≠ ∅) |
| 33 | 8, 32 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (𝐴 × 𝐵) ≠ ∅) |
| 34 | | unixp 6302 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 × 𝐵) ≠ ∅ → ∪ ∪ (𝐴 × 𝐵) = (𝐴 ∪ 𝐵)) |
| 35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ∪ ∪ (𝐴
× 𝐵) = (𝐴 ∪ 𝐵)) |
| 36 | 35 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (rank‘∪ ∪ (𝐴 × 𝐵)) = (rank‘(𝐴 ∪ 𝐵))) |
| 37 | | rankuni 9903 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(rank‘∪ ∪
(𝐴 × 𝐵)) = ∪ (rank‘∪ (𝐴 × 𝐵)) |
| 38 | | rankuni 9903 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(rank‘∪ (𝐴 × 𝐵)) = ∪
(rank‘(𝐴 ×
𝐵)) |
| 39 | 38 | unieqi 4919 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ (rank‘∪ (𝐴 × 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵)) |
| 40 | 37, 39 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(rank‘∪ ∪
(𝐴 × 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵)) |
| 41 | 36, 40 | eqtr3di 2792 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴 ∪ 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵))) |
| 42 | | eqimss 4042 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((rank‘(𝐴
∪ 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴 ∪ 𝐵)) ⊆ ∪
∪ (rank‘(𝐴 × 𝐵))) |
| 43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (rank‘(𝐴 ∪ 𝐵)) ⊆ ∪
∪ (rank‘(𝐴 × 𝐵))) |
| 44 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) → (rank‘(𝐴 ∪ 𝐵)) ⊆ ∪
∪ (rank‘(𝐴 × 𝐵))) |
| 45 | 27, 44 | eqsstrrd 4019 |
. . . . . . . . . . . . . . . . 17
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) → suc 𝑥 ⊆ ∪ ∪ (rank‘(𝐴 × 𝐵))) |
| 46 | 45 | adantrr 717 |
. . . . . . . . . . . . . . . 16
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 ⊆ ∪ ∪ (rank‘(𝐴 × 𝐵))) |
| 47 | | limuni 6445 |
. . . . . . . . . . . . . . . . 17
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ∪
(rank‘(𝐴 ×
𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵))) |
| 48 | 47 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → ∪
(rank‘(𝐴 ×
𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵))) |
| 49 | 46, 48 | sseqtrrd 4021 |
. . . . . . . . . . . . . . 15
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 ⊆ ∪
(rank‘(𝐴 ×
𝐵))) |
| 50 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V |
| 51 | | rankon 9835 |
. . . . . . . . . . . . . . . . . 18
⊢
(rank‘(𝐴
× 𝐵)) ∈
On |
| 52 | 51 | onordi 6495 |
. . . . . . . . . . . . . . . . 17
⊢ Ord
(rank‘(𝐴 ×
𝐵)) |
| 53 | | orduni 7809 |
. . . . . . . . . . . . . . . . 17
⊢ (Ord
(rank‘(𝐴 ×
𝐵)) → Ord ∪ (rank‘(𝐴 × 𝐵))) |
| 54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ Ord ∪ (rank‘(𝐴 × 𝐵)) |
| 55 | | ordelsuc 7840 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ V ∧ Ord ∪ (rank‘(𝐴 × 𝐵))) → (𝑥 ∈ ∪
(rank‘(𝐴 ×
𝐵)) ↔ suc 𝑥 ⊆ ∪ (rank‘(𝐴 × 𝐵)))) |
| 56 | 50, 54, 55 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ∪ (rank‘(𝐴 × 𝐵)) ↔ suc 𝑥 ⊆ ∪
(rank‘(𝐴 ×
𝐵))) |
| 57 | 49, 56 | sylibr 234 |
. . . . . . . . . . . . . 14
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → 𝑥 ∈ ∪
(rank‘(𝐴 ×
𝐵))) |
| 58 | | limsuc 7870 |
. . . . . . . . . . . . . . 15
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (𝑥 ∈ ∪
(rank‘(𝐴 ×
𝐵)) ↔ suc 𝑥 ∈ ∪ (rank‘(𝐴 × 𝐵)))) |
| 59 | 58 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (𝑥 ∈ ∪
(rank‘(𝐴 ×
𝐵)) ↔ suc 𝑥 ∈ ∪ (rank‘(𝐴 × 𝐵)))) |
| 60 | 57, 59 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc 𝑥 ∈ ∪
(rank‘(𝐴 ×
𝐵))) |
| 61 | 26, 60 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (rank‘(𝐴 ∪ 𝐵)) ∈ ∪
(rank‘(𝐴 ×
𝐵))) |
| 62 | | limsuc 7870 |
. . . . . . . . . . . . 13
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ((rank‘(𝐴 ∪ 𝐵)) ∈ ∪
(rank‘(𝐴 ×
𝐵)) ↔ suc
(rank‘(𝐴 ∪ 𝐵)) ∈ ∪ (rank‘(𝐴 × 𝐵)))) |
| 63 | 62 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → ((rank‘(𝐴 ∪ 𝐵)) ∈ ∪
(rank‘(𝐴 ×
𝐵)) ↔ suc
(rank‘(𝐴 ∪ 𝐵)) ∈ ∪ (rank‘(𝐴 × 𝐵)))) |
| 64 | 61, 63 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc (rank‘(𝐴 ∪ 𝐵)) ∈ ∪
(rank‘(𝐴 ×
𝐵))) |
| 65 | | ordsucelsuc 7842 |
. . . . . . . . . . . 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 218 |
. . . . . . . . . 10
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc (rank‘(𝐴 ∪ 𝐵)) ∈ suc ∪
(rank‘(𝐴 ×
𝐵))) |
| 68 | | onsucuni2 7854 |
. . . . . . . . . . . 12
⊢
(((rank‘(𝐴
× 𝐵)) ∈ On ∧
(rank‘(𝐴 ×
𝐵)) = suc 𝑦) → suc ∪ (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))) |
| 69 | 51, 68 | mpan 690 |
. . . . . . . . . . 11
⊢
((rank‘(𝐴
× 𝐵)) = suc 𝑦 → suc ∪ (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))) |
| 70 | 69 | ad2antll 729 |
. . . . . . . . . 10
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc ∪
(rank‘(𝐴 ×
𝐵)) = (rank‘(𝐴 × 𝐵))) |
| 71 | 67, 70 | eleqtrd 2843 |
. . . . . . . . 9
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc (rank‘(𝐴 ∪ 𝐵)) ∈ (rank‘(𝐴 × 𝐵))) |
| 72 | 11, 51 | onsucssi 7862 |
. . . . . . . . 9
⊢ (suc suc
(rank‘(𝐴 ∪ 𝐵)) ∈ (rank‘(𝐴 × 𝐵)) ↔ suc suc suc (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵))) |
| 73 | 71, 72 | sylib 218 |
. . . . . . . 8
⊢ ((Lim
∪ (rank‘(𝐴 × 𝐵)) ∧ ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → suc suc suc (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵))) |
| 74 | 73 | ex 412 |
. . . . . . 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 3212 |
. . . . 5
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → (∃𝑥 ∈ On ∃𝑦 ∈ On ((rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))) |
| 77 | 25, 76 | biimtrrid 243 |
. . . 4
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ((∃𝑥 ∈ On (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → suc suc suc (rank‘(𝐴 ∪ 𝐵)) ⊆ (rank‘(𝐴 × 𝐵)))) |
| 78 | 24, 77 | mtoi 199 |
. . 3
⊢ (Lim
∪ (rank‘(𝐴 × 𝐵)) → ¬ (∃𝑥 ∈ On (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) |
| 79 | | ianor 984 |
. . . . . 6
⊢ (¬
(∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) ↔ (¬ ∃𝑥 ∈ On (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∨ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) |
| 80 | | un00 4445 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) ↔ (𝐴 ∪ 𝐵) = ∅) |
| 81 | | animorl 980 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → (𝐴 = ∅ ∨ 𝐵 = ∅)) |
| 82 | 80, 81 | sylbir 235 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∪ 𝐵) = ∅ → (𝐴 = ∅ ∨ 𝐵 = ∅)) |
| 83 | | xpeq0 6180 |
. . . . . . . . . . . . 13
⊢ ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅)) |
| 84 | 82, 83 | sylibr 234 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∪ 𝐵) = ∅ → (𝐴 × 𝐵) = ∅) |
| 85 | 84 | con3i 154 |
. . . . . . . . . . 11
⊢ (¬
(𝐴 × 𝐵) = ∅ → ¬ (𝐴 ∪ 𝐵) = ∅) |
| 86 | 31, 85 | sylbir 235 |
. . . . . . . . . 10
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → ¬
(𝐴 ∪ 𝐵) = ∅) |
| 87 | 19, 20 | unex 7764 |
. . . . . . . . . . . 12
⊢ (𝐴 ∪ 𝐵) ∈ V |
| 88 | 87 | rankeq0 9901 |
. . . . . . . . . . 11
⊢ ((𝐴 ∪ 𝐵) = ∅ ↔ (rank‘(𝐴 ∪ 𝐵)) = ∅) |
| 89 | 88 | notbii 320 |
. . . . . . . . . 10
⊢ (¬
(𝐴 ∪ 𝐵) = ∅ ↔ ¬ (rank‘(𝐴 ∪ 𝐵)) = ∅) |
| 90 | 86, 89 | sylib 218 |
. . . . . . . . 9
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → ¬
(rank‘(𝐴 ∪ 𝐵)) = ∅) |
| 91 | 9 | onordi 6495 |
. . . . . . . . . . 11
⊢ Ord
(rank‘(𝐴 ∪ 𝐵)) |
| 92 | | ordzsl 7866 |
. . . . . . . . . . 11
⊢ (Ord
(rank‘(𝐴 ∪ 𝐵)) ↔ ((rank‘(𝐴 ∪ 𝐵)) = ∅ ∨ ∃𝑥 ∈ On (rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 ∪ 𝐵)))) |
| 93 | 91, 92 | mpbi 230 |
. . . . . . . . . 10
⊢
((rank‘(𝐴
∪ 𝐵)) = ∅ ∨
∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 ∪ 𝐵))) |
| 94 | 93 | 3ori 1426 |
. . . . . . . . 9
⊢ ((¬
(rank‘(𝐴 ∪ 𝐵)) = ∅ ∧ ¬
∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) → Lim (rank‘(𝐴 ∪ 𝐵))) |
| 95 | 90, 94 | sylan 580 |
. . . . . . . 8
⊢ ((¬
(rank‘(𝐴 ×
𝐵)) = ∅ ∧ ¬
∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥) → Lim (rank‘(𝐴 ∪ 𝐵))) |
| 96 | 95 | ex 412 |
. . . . . . 7
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → (¬
∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 → Lim (rank‘(𝐴 ∪ 𝐵)))) |
| 97 | | ordzsl 7866 |
. . . . . . . . . 10
⊢ (Ord
(rank‘(𝐴 ×
𝐵)) ↔
((rank‘(𝐴 ×
𝐵)) = ∅ ∨
∃𝑦 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑦 ∨ Lim (rank‘(𝐴 × 𝐵)))) |
| 98 | 52, 97 | mpbi 230 |
. . . . . . . . 9
⊢
((rank‘(𝐴
× 𝐵)) = ∅ ∨
∃𝑦 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑦 ∨ Lim (rank‘(𝐴 × 𝐵))) |
| 99 | 98 | 3ori 1426 |
. . . . . . . 8
⊢ ((¬
(rank‘(𝐴 ×
𝐵)) = ∅ ∧ ¬
∃𝑦 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑦) → Lim (rank‘(𝐴 × 𝐵))) |
| 100 | 99 | ex 412 |
. . . . . . 7
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → (¬
∃𝑦 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑦 → Lim (rank‘(𝐴 × 𝐵)))) |
| 101 | 96, 100 | orim12d 967 |
. . . . . 6
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ →
((¬ ∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∨ ¬ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → (Lim (rank‘(𝐴 ∪ 𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))))) |
| 102 | 79, 101 | biimtrid 242 |
. . . . 5
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → (¬
(∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦) → (Lim (rank‘(𝐴 ∪ 𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))))) |
| 103 | 102 | imp 406 |
. . . 4
⊢ ((¬
(rank‘(𝐴 ×
𝐵)) = ∅ ∧ ¬
(∃𝑥 ∈ On
(rank‘(𝐴 ∪ 𝐵)) = suc 𝑥 ∧ ∃𝑦 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑦)) → (Lim (rank‘(𝐴 ∪ 𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵)))) |
| 104 | | simpl 482 |
. . . . . . . 8
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ ¬
(rank‘(𝐴 ×
𝐵)) = ∅) → Lim
(rank‘(𝐴 ∪ 𝐵))) |
| 105 | 30 | necon3abii 2987 |
. . . . . . . . . 10
⊢ ((𝐴 × 𝐵) ≠ ∅ ↔ ¬
(rank‘(𝐴 ×
𝐵)) =
∅) |
| 106 | 19, 20 | rankxplim 9919 |
. . . . . . . . . 10
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 ∪ 𝐵))) |
| 107 | 105, 106 | sylan2br 595 |
. . . . . . . . 9
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ ¬
(rank‘(𝐴 ×
𝐵)) = ∅) →
(rank‘(𝐴 ×
𝐵)) = (rank‘(𝐴 ∪ 𝐵))) |
| 108 | | limeq 6396 |
. . . . . . . . 9
⊢
((rank‘(𝐴
× 𝐵)) =
(rank‘(𝐴 ∪ 𝐵)) → (Lim
(rank‘(𝐴 ×
𝐵)) ↔ Lim
(rank‘(𝐴 ∪ 𝐵)))) |
| 109 | 107, 108 | syl 17 |
. . . . . . . 8
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ ¬
(rank‘(𝐴 ×
𝐵)) = ∅) → (Lim
(rank‘(𝐴 ×
𝐵)) ↔ Lim
(rank‘(𝐴 ∪ 𝐵)))) |
| 110 | 104, 109 | mpbird 257 |
. . . . . . 7
⊢ ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∧ ¬
(rank‘(𝐴 ×
𝐵)) = ∅) → Lim
(rank‘(𝐴 ×
𝐵))) |
| 111 | 110 | expcom 413 |
. . . . . 6
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → (Lim
(rank‘(𝐴 ∪ 𝐵)) → Lim (rank‘(𝐴 × 𝐵)))) |
| 112 | | idd 24 |
. . . . . 6
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → (Lim
(rank‘(𝐴 ×
𝐵)) → Lim
(rank‘(𝐴 ×
𝐵)))) |
| 113 | 111, 112 | jaod 860 |
. . . . 5
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ → ((Lim
(rank‘(𝐴 ∪ 𝐵)) ∨ Lim (rank‘(𝐴 × 𝐵))) → Lim (rank‘(𝐴 × 𝐵)))) |
| 114 | 113 | adantr 480 |
. . . 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 209 |
1
⊢ (Lim
(rank‘(𝐴 ×
𝐵)) ↔ Lim ∪ (rank‘(𝐴 × 𝐵))) |