| Step | Hyp | Ref
| Expression |
| 1 | | unixp 6302 |
. . . . . . . 8
⊢ ((𝐴 × 𝐵) ≠ ∅ → ∪ ∪ (𝐴 × 𝐵) = (𝐴 ∪ 𝐵)) |
| 2 | 1 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ≠ ∅ → (rank‘∪ ∪ (𝐴 × 𝐵)) = (rank‘(𝐴 ∪ 𝐵))) |
| 3 | | rankuni 9903 |
. . . . . . . 8
⊢
(rank‘∪ ∪
(𝐴 × 𝐵)) = ∪ (rank‘∪ (𝐴 × 𝐵)) |
| 4 | | rankuni 9903 |
. . . . . . . . 9
⊢
(rank‘∪ (𝐴 × 𝐵)) = ∪
(rank‘(𝐴 ×
𝐵)) |
| 5 | 4 | unieqi 4919 |
. . . . . . . 8
⊢ ∪ (rank‘∪ (𝐴 × 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵)) |
| 6 | 3, 5 | eqtri 2765 |
. . . . . . 7
⊢
(rank‘∪ ∪
(𝐴 × 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵)) |
| 7 | 2, 6 | eqtr3di 2792 |
. . . . . 6
⊢ ((𝐴 × 𝐵) ≠ ∅ → (rank‘(𝐴 ∪ 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵))) |
| 8 | | suc11reg 9659 |
. . . . . 6
⊢ (suc
(rank‘(𝐴 ∪ 𝐵)) = suc ∪ ∪ (rank‘(𝐴 × 𝐵)) ↔ (rank‘(𝐴 ∪ 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵))) |
| 9 | 7, 8 | sylibr 234 |
. . . . 5
⊢ ((𝐴 × 𝐵) ≠ ∅ → suc (rank‘(𝐴 ∪ 𝐵)) = suc ∪ ∪ (rank‘(𝐴 × 𝐵))) |
| 10 | 9 | adantl 481 |
. . . 4
⊢
(((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → suc
(rank‘(𝐴 ∪ 𝐵)) = suc ∪ ∪ (rank‘(𝐴 × 𝐵))) |
| 11 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢
(rank‘(𝐴 ∪
𝐵)) ∈
V |
| 12 | | eleq1 2829 |
. . . . . . . . . . . . . 14
⊢
((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 → ((rank‘(𝐴 ∪ 𝐵)) ∈ V ↔ suc 𝐶 ∈ V)) |
| 13 | 11, 12 | mpbii 233 |
. . . . . . . . . . . . 13
⊢
((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 → suc 𝐶 ∈ V) |
| 14 | | sucexb 7824 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ V ↔ suc 𝐶 ∈ V) |
| 15 | 13, 14 | sylibr 234 |
. . . . . . . . . . . 12
⊢
((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 → 𝐶 ∈ V) |
| 16 | | nlimsucg 7863 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ V → ¬ Lim suc
𝐶) |
| 17 | 15, 16 | syl 17 |
. . . . . . . . . . 11
⊢
((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 → ¬ Lim suc 𝐶) |
| 18 | | limeq 6396 |
. . . . . . . . . . 11
⊢
((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 → (Lim (rank‘(𝐴 ∪ 𝐵)) ↔ Lim suc 𝐶)) |
| 19 | 17, 18 | mtbird 325 |
. . . . . . . . . 10
⊢
((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 → ¬ Lim
(rank‘(𝐴 ∪ 𝐵))) |
| 20 | | rankxplim.1 |
. . . . . . . . . . 11
⊢ 𝐴 ∈ V |
| 21 | | rankxplim.2 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ V |
| 22 | 20, 21 | rankxplim2 9920 |
. . . . . . . . . 10
⊢ (Lim
(rank‘(𝐴 ×
𝐵)) → Lim
(rank‘(𝐴 ∪ 𝐵))) |
| 23 | 19, 22 | nsyl 140 |
. . . . . . . . 9
⊢
((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 → ¬ Lim
(rank‘(𝐴 ×
𝐵))) |
| 24 | 20, 21 | xpex 7773 |
. . . . . . . . . . . . . 14
⊢ (𝐴 × 𝐵) ∈ V |
| 25 | 24 | rankeq0 9901 |
. . . . . . . . . . . . 13
⊢ ((𝐴 × 𝐵) = ∅ ↔ (rank‘(𝐴 × 𝐵)) = ∅) |
| 26 | 25 | necon3abii 2987 |
. . . . . . . . . . . 12
⊢ ((𝐴 × 𝐵) ≠ ∅ ↔ ¬
(rank‘(𝐴 ×
𝐵)) =
∅) |
| 27 | | rankon 9835 |
. . . . . . . . . . . . . . . 16
⊢
(rank‘(𝐴
× 𝐵)) ∈
On |
| 28 | 27 | onordi 6495 |
. . . . . . . . . . . . . . 15
⊢ Ord
(rank‘(𝐴 ×
𝐵)) |
| 29 | | ordzsl 7866 |
. . . . . . . . . . . . . . 15
⊢ (Ord
(rank‘(𝐴 ×
𝐵)) ↔
((rank‘(𝐴 ×
𝐵)) = ∅ ∨
∃𝑥 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 × 𝐵)))) |
| 30 | 28, 29 | mpbi 230 |
. . . . . . . . . . . . . 14
⊢
((rank‘(𝐴
× 𝐵)) = ∅ ∨
∃𝑥 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 × 𝐵))) |
| 31 | | 3orass 1090 |
. . . . . . . . . . . . . 14
⊢
(((rank‘(𝐴
× 𝐵)) = ∅ ∨
∃𝑥 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 × 𝐵))) ↔ ((rank‘(𝐴 × 𝐵)) = ∅ ∨ (∃𝑥 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 × 𝐵))))) |
| 32 | 30, 31 | mpbi 230 |
. . . . . . . . . . . . 13
⊢
((rank‘(𝐴
× 𝐵)) = ∅ ∨
(∃𝑥 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 × 𝐵)))) |
| 33 | 32 | ori 862 |
. . . . . . . . . . . 12
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ →
(∃𝑥 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 × 𝐵)))) |
| 34 | 26, 33 | sylbi 217 |
. . . . . . . . . . 11
⊢ ((𝐴 × 𝐵) ≠ ∅ → (∃𝑥 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 × 𝐵)))) |
| 35 | 34 | ord 865 |
. . . . . . . . . 10
⊢ ((𝐴 × 𝐵) ≠ ∅ → (¬ ∃𝑥 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑥 → Lim (rank‘(𝐴 × 𝐵)))) |
| 36 | 35 | con1d 145 |
. . . . . . . . 9
⊢ ((𝐴 × 𝐵) ≠ ∅ → (¬ Lim
(rank‘(𝐴 ×
𝐵)) → ∃𝑥 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑥)) |
| 37 | 23, 36 | syl5com 31 |
. . . . . . . 8
⊢
((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 → ((𝐴 × 𝐵) ≠ ∅ → ∃𝑥 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑥)) |
| 38 | | nlimsucg 7863 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ V → ¬ Lim suc
𝑥) |
| 39 | 38 | elv 3485 |
. . . . . . . . . . 11
⊢ ¬
Lim suc 𝑥 |
| 40 | | limeq 6396 |
. . . . . . . . . . 11
⊢
((rank‘(𝐴
× 𝐵)) = suc 𝑥 → (Lim (rank‘(𝐴 × 𝐵)) ↔ Lim suc 𝑥)) |
| 41 | 39, 40 | mtbiri 327 |
. . . . . . . . . 10
⊢
((rank‘(𝐴
× 𝐵)) = suc 𝑥 → ¬ Lim
(rank‘(𝐴 ×
𝐵))) |
| 42 | 41 | rexlimivw 3151 |
. . . . . . . . 9
⊢
(∃𝑥 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 → ¬ Lim
(rank‘(𝐴 ×
𝐵))) |
| 43 | 20, 21 | rankxplim3 9921 |
. . . . . . . . 9
⊢ (Lim
(rank‘(𝐴 ×
𝐵)) ↔ Lim ∪ (rank‘(𝐴 × 𝐵))) |
| 44 | 42, 43 | sylnib 328 |
. . . . . . . 8
⊢
(∃𝑥 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 → ¬ Lim ∪ (rank‘(𝐴 × 𝐵))) |
| 45 | 37, 44 | syl6com 37 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ≠ ∅ → ((rank‘(𝐴 ∪ 𝐵)) = suc 𝐶 → ¬ Lim ∪ (rank‘(𝐴 × 𝐵)))) |
| 46 | | unixp0 6303 |
. . . . . . . . . . . 12
⊢ ((𝐴 × 𝐵) = ∅ ↔ ∪ (𝐴
× 𝐵) =
∅) |
| 47 | 24 | uniex 7761 |
. . . . . . . . . . . . 13
⊢ ∪ (𝐴
× 𝐵) ∈
V |
| 48 | 47 | rankeq0 9901 |
. . . . . . . . . . . 12
⊢ (∪ (𝐴
× 𝐵) = ∅ ↔
(rank‘∪ (𝐴 × 𝐵)) = ∅) |
| 49 | 4 | eqeq1i 2742 |
. . . . . . . . . . . 12
⊢
((rank‘∪ (𝐴 × 𝐵)) = ∅ ↔ ∪ (rank‘(𝐴 × 𝐵)) = ∅) |
| 50 | 46, 48, 49 | 3bitri 297 |
. . . . . . . . . . 11
⊢ ((𝐴 × 𝐵) = ∅ ↔ ∪ (rank‘(𝐴 × 𝐵)) = ∅) |
| 51 | 50 | necon3abii 2987 |
. . . . . . . . . 10
⊢ ((𝐴 × 𝐵) ≠ ∅ ↔ ¬ ∪ (rank‘(𝐴 × 𝐵)) = ∅) |
| 52 | | onuni 7808 |
. . . . . . . . . . . . . . 15
⊢
((rank‘(𝐴
× 𝐵)) ∈ On
→ ∪ (rank‘(𝐴 × 𝐵)) ∈ On) |
| 53 | 27, 52 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ∪ (rank‘(𝐴 × 𝐵)) ∈ On |
| 54 | 53 | onordi 6495 |
. . . . . . . . . . . . 13
⊢ Ord ∪ (rank‘(𝐴 × 𝐵)) |
| 55 | | ordzsl 7866 |
. . . . . . . . . . . . 13
⊢ (Ord
∪ (rank‘(𝐴 × 𝐵)) ↔ (∪
(rank‘(𝐴 ×
𝐵)) = ∅ ∨
∃𝑥 ∈ On ∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥 ∨ Lim ∪
(rank‘(𝐴 ×
𝐵)))) |
| 56 | 54, 55 | mpbi 230 |
. . . . . . . . . . . 12
⊢ (∪ (rank‘(𝐴 × 𝐵)) = ∅ ∨ ∃𝑥 ∈ On ∪
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 ∨ Lim ∪ (rank‘(𝐴 × 𝐵))) |
| 57 | | 3orass 1090 |
. . . . . . . . . . . 12
⊢ ((∪ (rank‘(𝐴 × 𝐵)) = ∅ ∨ ∃𝑥 ∈ On ∪
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 ∨ Lim ∪ (rank‘(𝐴 × 𝐵))) ↔ (∪
(rank‘(𝐴 ×
𝐵)) = ∅ ∨
(∃𝑥 ∈ On ∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥 ∨ Lim ∪
(rank‘(𝐴 ×
𝐵))))) |
| 58 | 56, 57 | mpbi 230 |
. . . . . . . . . . 11
⊢ (∪ (rank‘(𝐴 × 𝐵)) = ∅ ∨ (∃𝑥 ∈ On ∪
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 ∨ Lim ∪ (rank‘(𝐴 × 𝐵)))) |
| 59 | 58 | ori 862 |
. . . . . . . . . 10
⊢ (¬
∪ (rank‘(𝐴 × 𝐵)) = ∅ → (∃𝑥 ∈ On ∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥 ∨ Lim ∪
(rank‘(𝐴 ×
𝐵)))) |
| 60 | 51, 59 | sylbi 217 |
. . . . . . . . 9
⊢ ((𝐴 × 𝐵) ≠ ∅ → (∃𝑥 ∈ On ∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥 ∨ Lim ∪
(rank‘(𝐴 ×
𝐵)))) |
| 61 | 60 | ord 865 |
. . . . . . . 8
⊢ ((𝐴 × 𝐵) ≠ ∅ → (¬ ∃𝑥 ∈ On ∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥 → Lim ∪
(rank‘(𝐴 ×
𝐵)))) |
| 62 | 61 | con1d 145 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ≠ ∅ → (¬ Lim ∪ (rank‘(𝐴 × 𝐵)) → ∃𝑥 ∈ On ∪
(rank‘(𝐴 ×
𝐵)) = suc 𝑥)) |
| 63 | 45, 62 | syld 47 |
. . . . . 6
⊢ ((𝐴 × 𝐵) ≠ ∅ → ((rank‘(𝐴 ∪ 𝐵)) = suc 𝐶 → ∃𝑥 ∈ On ∪
(rank‘(𝐴 ×
𝐵)) = suc 𝑥)) |
| 64 | 63 | impcom 407 |
. . . . 5
⊢
(((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → ∃𝑥 ∈ On ∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥) |
| 65 | | onsucuni2 7854 |
. . . . . . 7
⊢ ((∪ (rank‘(𝐴 × 𝐵)) ∈ On ∧ ∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥) → suc ∪
∪ (rank‘(𝐴 × 𝐵)) = ∪
(rank‘(𝐴 ×
𝐵))) |
| 66 | 53, 65 | mpan 690 |
. . . . . 6
⊢ (∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥 → suc ∪
∪ (rank‘(𝐴 × 𝐵)) = ∪
(rank‘(𝐴 ×
𝐵))) |
| 67 | 66 | rexlimivw 3151 |
. . . . 5
⊢
(∃𝑥 ∈ On
∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥 → suc ∪
∪ (rank‘(𝐴 × 𝐵)) = ∪
(rank‘(𝐴 ×
𝐵))) |
| 68 | 64, 67 | syl 17 |
. . . 4
⊢
(((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → suc ∪ ∪ (rank‘(𝐴 × 𝐵)) = ∪
(rank‘(𝐴 ×
𝐵))) |
| 69 | 10, 68 | eqtrd 2777 |
. . 3
⊢
(((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → suc
(rank‘(𝐴 ∪ 𝐵)) = ∪ (rank‘(𝐴 × 𝐵))) |
| 70 | | suc11reg 9659 |
. . 3
⊢ (suc suc
(rank‘(𝐴 ∪ 𝐵)) = suc ∪ (rank‘(𝐴 × 𝐵)) ↔ suc (rank‘(𝐴 ∪ 𝐵)) = ∪
(rank‘(𝐴 ×
𝐵))) |
| 71 | 69, 70 | sylibr 234 |
. 2
⊢
(((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → suc suc
(rank‘(𝐴 ∪ 𝐵)) = suc ∪ (rank‘(𝐴 × 𝐵))) |
| 72 | 37 | imp 406 |
. . 3
⊢
(((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → ∃𝑥 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑥) |
| 73 | | onsucuni2 7854 |
. . . . 5
⊢
(((rank‘(𝐴
× 𝐵)) ∈ On ∧
(rank‘(𝐴 ×
𝐵)) = suc 𝑥) → suc ∪ (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))) |
| 74 | 27, 73 | mpan 690 |
. . . 4
⊢
((rank‘(𝐴
× 𝐵)) = suc 𝑥 → suc ∪ (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))) |
| 75 | 74 | rexlimivw 3151 |
. . 3
⊢
(∃𝑥 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 → suc ∪ (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))) |
| 76 | 72, 75 | syl 17 |
. 2
⊢
(((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → suc ∪ (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))) |
| 77 | 71, 76 | eqtr2d 2778 |
1
⊢
(((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = suc suc (rank‘(𝐴 ∪ 𝐵))) |