Step | Hyp | Ref
| Expression |
1 | | rankuni 8609 |
. . . . . . . 8
⊢
(rank‘∪ ∪
(𝐴 × 𝐵)) = ∪ (rank‘∪ (𝐴 × 𝐵)) |
2 | | rankuni 8609 |
. . . . . . . . 9
⊢
(rank‘∪ (𝐴 × 𝐵)) = ∪
(rank‘(𝐴 ×
𝐵)) |
3 | 2 | unieqi 4381 |
. . . . . . . 8
⊢ ∪ (rank‘∪ (𝐴 × 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵)) |
4 | 1, 3 | eqtri 2632 |
. . . . . . 7
⊢
(rank‘∪ ∪
(𝐴 × 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵)) |
5 | | unixp 5585 |
. . . . . . . 8
⊢ ((𝐴 × 𝐵) ≠ ∅ → ∪ ∪ (𝐴 × 𝐵) = (𝐴 ∪ 𝐵)) |
6 | 5 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ≠ ∅ → (rank‘∪ ∪ (𝐴 × 𝐵)) = (rank‘(𝐴 ∪ 𝐵))) |
7 | 4, 6 | syl5reqr 2659 |
. . . . . 6
⊢ ((𝐴 × 𝐵) ≠ ∅ → (rank‘(𝐴 ∪ 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵))) |
8 | | suc11reg 8399 |
. . . . . 6
⊢ (suc
(rank‘(𝐴 ∪ 𝐵)) = suc ∪ ∪ (rank‘(𝐴 × 𝐵)) ↔ (rank‘(𝐴 ∪ 𝐵)) = ∪ ∪ (rank‘(𝐴 × 𝐵))) |
9 | 7, 8 | sylibr 223 |
. . . . 5
⊢ ((𝐴 × 𝐵) ≠ ∅ → suc (rank‘(𝐴 ∪ 𝐵)) = suc ∪ ∪ (rank‘(𝐴 × 𝐵))) |
10 | 9 | adantl 481 |
. . . 4
⊢
(((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → suc
(rank‘(𝐴 ∪ 𝐵)) = suc ∪ ∪ (rank‘(𝐴 × 𝐵))) |
11 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(rank‘(𝐴 ∪
𝐵)) ∈
V |
12 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢
((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 → ((rank‘(𝐴 ∪ 𝐵)) ∈ V ↔ suc 𝐶 ∈ V)) |
13 | 11, 12 | mpbii 222 |
. . . . . . . . . . . . 13
⊢
((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 → suc 𝐶 ∈ V) |
14 | | sucexb 6901 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ V ↔ suc 𝐶 ∈ V) |
15 | 13, 14 | sylibr 223 |
. . . . . . . . . . . 12
⊢
((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 → 𝐶 ∈ V) |
16 | | nlimsucg 6934 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ V → ¬ Lim suc
𝐶) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . 11
⊢
((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 → ¬ Lim suc 𝐶) |
18 | | limeq 5652 |
. . . . . . . . . . 11
⊢
((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 → (Lim (rank‘(𝐴 ∪ 𝐵)) ↔ Lim suc 𝐶)) |
19 | 17, 18 | mtbird 314 |
. . . . . . . . . 10
⊢
((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 → ¬ Lim
(rank‘(𝐴 ∪ 𝐵))) |
20 | | rankxplim.1 |
. . . . . . . . . . 11
⊢ 𝐴 ∈ V |
21 | | rankxplim.2 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ V |
22 | 20, 21 | rankxplim2 8626 |
. . . . . . . . . 10
⊢ (Lim
(rank‘(𝐴 ×
𝐵)) → Lim
(rank‘(𝐴 ∪ 𝐵))) |
23 | 19, 22 | nsyl 134 |
. . . . . . . . 9
⊢
((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 → ¬ Lim
(rank‘(𝐴 ×
𝐵))) |
24 | 20, 21 | xpex 6860 |
. . . . . . . . . . . . . 14
⊢ (𝐴 × 𝐵) ∈ V |
25 | 24 | rankeq0 8607 |
. . . . . . . . . . . . 13
⊢ ((𝐴 × 𝐵) = ∅ ↔ (rank‘(𝐴 × 𝐵)) = ∅) |
26 | 25 | necon3abii 2828 |
. . . . . . . . . . . 12
⊢ ((𝐴 × 𝐵) ≠ ∅ ↔ ¬
(rank‘(𝐴 ×
𝐵)) =
∅) |
27 | | rankon 8541 |
. . . . . . . . . . . . . . . 16
⊢
(rank‘(𝐴
× 𝐵)) ∈
On |
28 | 27 | onordi 5749 |
. . . . . . . . . . . . . . 15
⊢ Ord
(rank‘(𝐴 ×
𝐵)) |
29 | | ordzsl 6937 |
. . . . . . . . . . . . . . 15
⊢ (Ord
(rank‘(𝐴 ×
𝐵)) ↔
((rank‘(𝐴 ×
𝐵)) = ∅ ∨
∃𝑥 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 × 𝐵)))) |
30 | 28, 29 | mpbi 219 |
. . . . . . . . . . . . . 14
⊢
((rank‘(𝐴
× 𝐵)) = ∅ ∨
∃𝑥 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 × 𝐵))) |
31 | | 3orass 1034 |
. . . . . . . . . . . . . 14
⊢
(((rank‘(𝐴
× 𝐵)) = ∅ ∨
∃𝑥 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 × 𝐵))) ↔ ((rank‘(𝐴 × 𝐵)) = ∅ ∨ (∃𝑥 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 × 𝐵))))) |
32 | 30, 31 | mpbi 219 |
. . . . . . . . . . . . 13
⊢
((rank‘(𝐴
× 𝐵)) = ∅ ∨
(∃𝑥 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 × 𝐵)))) |
33 | 32 | ori 389 |
. . . . . . . . . . . 12
⊢ (¬
(rank‘(𝐴 ×
𝐵)) = ∅ →
(∃𝑥 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 × 𝐵)))) |
34 | 26, 33 | sylbi 206 |
. . . . . . . . . . 11
⊢ ((𝐴 × 𝐵) ≠ ∅ → (∃𝑥 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑥 ∨ Lim (rank‘(𝐴 × 𝐵)))) |
35 | 34 | ord 391 |
. . . . . . . . . 10
⊢ ((𝐴 × 𝐵) ≠ ∅ → (¬ ∃𝑥 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑥 → Lim (rank‘(𝐴 × 𝐵)))) |
36 | 35 | con1d 138 |
. . . . . . . . 9
⊢ ((𝐴 × 𝐵) ≠ ∅ → (¬ Lim
(rank‘(𝐴 ×
𝐵)) → ∃𝑥 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑥)) |
37 | 23, 36 | syl5com 31 |
. . . . . . . 8
⊢
((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 → ((𝐴 × 𝐵) ≠ ∅ → ∃𝑥 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑥)) |
38 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
39 | | nlimsucg 6934 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ V → ¬ Lim suc
𝑥) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ¬
Lim suc 𝑥 |
41 | | limeq 5652 |
. . . . . . . . . . 11
⊢
((rank‘(𝐴
× 𝐵)) = suc 𝑥 → (Lim (rank‘(𝐴 × 𝐵)) ↔ Lim suc 𝑥)) |
42 | 40, 41 | mtbiri 316 |
. . . . . . . . . 10
⊢
((rank‘(𝐴
× 𝐵)) = suc 𝑥 → ¬ Lim
(rank‘(𝐴 ×
𝐵))) |
43 | 42 | rexlimivw 3011 |
. . . . . . . . 9
⊢
(∃𝑥 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 → ¬ Lim
(rank‘(𝐴 ×
𝐵))) |
44 | 20, 21 | rankxplim3 8627 |
. . . . . . . . 9
⊢ (Lim
(rank‘(𝐴 ×
𝐵)) ↔ Lim ∪ (rank‘(𝐴 × 𝐵))) |
45 | 43, 44 | sylnib 317 |
. . . . . . . 8
⊢
(∃𝑥 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 → ¬ Lim ∪ (rank‘(𝐴 × 𝐵))) |
46 | 37, 45 | syl6com 36 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ≠ ∅ → ((rank‘(𝐴 ∪ 𝐵)) = suc 𝐶 → ¬ Lim ∪ (rank‘(𝐴 × 𝐵)))) |
47 | | unixp0 5586 |
. . . . . . . . . . . 12
⊢ ((𝐴 × 𝐵) = ∅ ↔ ∪ (𝐴
× 𝐵) =
∅) |
48 | 24 | uniex 6851 |
. . . . . . . . . . . . 13
⊢ ∪ (𝐴
× 𝐵) ∈
V |
49 | 48 | rankeq0 8607 |
. . . . . . . . . . . 12
⊢ (∪ (𝐴
× 𝐵) = ∅ ↔
(rank‘∪ (𝐴 × 𝐵)) = ∅) |
50 | 2 | eqeq1i 2615 |
. . . . . . . . . . . 12
⊢
((rank‘∪ (𝐴 × 𝐵)) = ∅ ↔ ∪ (rank‘(𝐴 × 𝐵)) = ∅) |
51 | 47, 49, 50 | 3bitri 285 |
. . . . . . . . . . 11
⊢ ((𝐴 × 𝐵) = ∅ ↔ ∪ (rank‘(𝐴 × 𝐵)) = ∅) |
52 | 51 | necon3abii 2828 |
. . . . . . . . . 10
⊢ ((𝐴 × 𝐵) ≠ ∅ ↔ ¬ ∪ (rank‘(𝐴 × 𝐵)) = ∅) |
53 | | onuni 6885 |
. . . . . . . . . . . . . . 15
⊢
((rank‘(𝐴
× 𝐵)) ∈ On
→ ∪ (rank‘(𝐴 × 𝐵)) ∈ On) |
54 | 27, 53 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ∪ (rank‘(𝐴 × 𝐵)) ∈ On |
55 | 54 | onordi 5749 |
. . . . . . . . . . . . 13
⊢ Ord ∪ (rank‘(𝐴 × 𝐵)) |
56 | | ordzsl 6937 |
. . . . . . . . . . . . 13
⊢ (Ord
∪ (rank‘(𝐴 × 𝐵)) ↔ (∪
(rank‘(𝐴 ×
𝐵)) = ∅ ∨
∃𝑥 ∈ On ∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥 ∨ Lim ∪
(rank‘(𝐴 ×
𝐵)))) |
57 | 55, 56 | mpbi 219 |
. . . . . . . . . . . 12
⊢ (∪ (rank‘(𝐴 × 𝐵)) = ∅ ∨ ∃𝑥 ∈ On ∪
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 ∨ Lim ∪ (rank‘(𝐴 × 𝐵))) |
58 | | 3orass 1034 |
. . . . . . . . . . . 12
⊢ ((∪ (rank‘(𝐴 × 𝐵)) = ∅ ∨ ∃𝑥 ∈ On ∪
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 ∨ Lim ∪ (rank‘(𝐴 × 𝐵))) ↔ (∪
(rank‘(𝐴 ×
𝐵)) = ∅ ∨
(∃𝑥 ∈ On ∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥 ∨ Lim ∪
(rank‘(𝐴 ×
𝐵))))) |
59 | 57, 58 | mpbi 219 |
. . . . . . . . . . 11
⊢ (∪ (rank‘(𝐴 × 𝐵)) = ∅ ∨ (∃𝑥 ∈ On ∪
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 ∨ Lim ∪ (rank‘(𝐴 × 𝐵)))) |
60 | 59 | ori 389 |
. . . . . . . . . 10
⊢ (¬
∪ (rank‘(𝐴 × 𝐵)) = ∅ → (∃𝑥 ∈ On ∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥 ∨ Lim ∪
(rank‘(𝐴 ×
𝐵)))) |
61 | 52, 60 | sylbi 206 |
. . . . . . . . 9
⊢ ((𝐴 × 𝐵) ≠ ∅ → (∃𝑥 ∈ On ∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥 ∨ Lim ∪
(rank‘(𝐴 ×
𝐵)))) |
62 | 61 | ord 391 |
. . . . . . . 8
⊢ ((𝐴 × 𝐵) ≠ ∅ → (¬ ∃𝑥 ∈ On ∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥 → Lim ∪
(rank‘(𝐴 ×
𝐵)))) |
63 | 62 | con1d 138 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ≠ ∅ → (¬ Lim ∪ (rank‘(𝐴 × 𝐵)) → ∃𝑥 ∈ On ∪
(rank‘(𝐴 ×
𝐵)) = suc 𝑥)) |
64 | 46, 63 | syld 46 |
. . . . . 6
⊢ ((𝐴 × 𝐵) ≠ ∅ → ((rank‘(𝐴 ∪ 𝐵)) = suc 𝐶 → ∃𝑥 ∈ On ∪
(rank‘(𝐴 ×
𝐵)) = suc 𝑥)) |
65 | 64 | impcom 445 |
. . . . 5
⊢
(((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → ∃𝑥 ∈ On ∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥) |
66 | | onsucuni2 6926 |
. . . . . . 7
⊢ ((∪ (rank‘(𝐴 × 𝐵)) ∈ On ∧ ∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥) → suc ∪
∪ (rank‘(𝐴 × 𝐵)) = ∪
(rank‘(𝐴 ×
𝐵))) |
67 | 54, 66 | mpan 702 |
. . . . . 6
⊢ (∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥 → suc ∪
∪ (rank‘(𝐴 × 𝐵)) = ∪
(rank‘(𝐴 ×
𝐵))) |
68 | 67 | rexlimivw 3011 |
. . . . 5
⊢
(∃𝑥 ∈ On
∪ (rank‘(𝐴 × 𝐵)) = suc 𝑥 → suc ∪
∪ (rank‘(𝐴 × 𝐵)) = ∪
(rank‘(𝐴 ×
𝐵))) |
69 | 65, 68 | syl 17 |
. . . 4
⊢
(((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → suc ∪ ∪ (rank‘(𝐴 × 𝐵)) = ∪
(rank‘(𝐴 ×
𝐵))) |
70 | 10, 69 | eqtrd 2644 |
. . 3
⊢
(((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → suc
(rank‘(𝐴 ∪ 𝐵)) = ∪ (rank‘(𝐴 × 𝐵))) |
71 | | suc11reg 8399 |
. . 3
⊢ (suc suc
(rank‘(𝐴 ∪ 𝐵)) = suc ∪ (rank‘(𝐴 × 𝐵)) ↔ suc (rank‘(𝐴 ∪ 𝐵)) = ∪
(rank‘(𝐴 ×
𝐵))) |
72 | 70, 71 | sylibr 223 |
. 2
⊢
(((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → suc suc
(rank‘(𝐴 ∪ 𝐵)) = suc ∪ (rank‘(𝐴 × 𝐵))) |
73 | 37 | imp 444 |
. . 3
⊢
(((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → ∃𝑥 ∈ On (rank‘(𝐴 × 𝐵)) = suc 𝑥) |
74 | | onsucuni2 6926 |
. . . . 5
⊢
(((rank‘(𝐴
× 𝐵)) ∈ On ∧
(rank‘(𝐴 ×
𝐵)) = suc 𝑥) → suc ∪ (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))) |
75 | 27, 74 | mpan 702 |
. . . 4
⊢
((rank‘(𝐴
× 𝐵)) = suc 𝑥 → suc ∪ (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))) |
76 | 75 | rexlimivw 3011 |
. . 3
⊢
(∃𝑥 ∈ On
(rank‘(𝐴 ×
𝐵)) = suc 𝑥 → suc ∪ (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))) |
77 | 73, 76 | syl 17 |
. 2
⊢
(((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → suc ∪ (rank‘(𝐴 × 𝐵)) = (rank‘(𝐴 × 𝐵))) |
78 | 72, 77 | eqtr2d 2645 |
1
⊢
(((rank‘(𝐴
∪ 𝐵)) = suc 𝐶 ∧ (𝐴 × 𝐵) ≠ ∅) → (rank‘(𝐴 × 𝐵)) = suc suc (rank‘(𝐴 ∪ 𝐵))) |