Proof of Theorem alephadd
Step | Hyp | Ref
| Expression |
1 | | fvex 6506 |
. . . . 5
⊢
(ℵ‘𝐴)
∈ V |
2 | | fvex 6506 |
. . . . 5
⊢
(ℵ‘𝐵)
∈ V |
3 | | djuex 9125 |
. . . . 5
⊢
(((ℵ‘𝐴)
∈ V ∧ (ℵ‘𝐵) ∈ V) → ((ℵ‘𝐴) ⊔ (ℵ‘𝐵)) ∈ V) |
4 | 1, 2, 3 | mp2an 679 |
. . . 4
⊢
((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
∈ V |
5 | | alephfnon 9279 |
. . . . . . . 8
⊢ ℵ
Fn On |
6 | | fndm 6282 |
. . . . . . . 8
⊢ (ℵ
Fn On → dom ℵ = On) |
7 | 5, 6 | ax-mp 5 |
. . . . . . 7
⊢ dom
ℵ = On |
8 | 7 | eleq2i 2851 |
. . . . . 6
⊢ (𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On) |
9 | 8 | notbii 312 |
. . . . 5
⊢ (¬
𝐴 ∈ dom ℵ ↔
¬ 𝐴 ∈
On) |
10 | 7 | eleq2i 2851 |
. . . . . 6
⊢ (𝐵 ∈ dom ℵ ↔ 𝐵 ∈ On) |
11 | 10 | notbii 312 |
. . . . 5
⊢ (¬
𝐵 ∈ dom ℵ ↔
¬ 𝐵 ∈
On) |
12 | | df-dju 9118 |
. . . . . . 7
⊢ (∅
⊔ ∅) = (({∅} × ∅) ∪ ({1o} ×
∅)) |
13 | | xpundir 5465 |
. . . . . . 7
⊢
(({∅} ∪ {1o}) × ∅) = (({∅}
× ∅) ∪ ({1o} × ∅)) |
14 | | xp0 5849 |
. . . . . . 7
⊢
(({∅} ∪ {1o}) × ∅) =
∅ |
15 | 12, 13, 14 | 3eqtr2i 2802 |
. . . . . 6
⊢ (∅
⊔ ∅) = ∅ |
16 | | ndmfv 6523 |
. . . . . . 7
⊢ (¬
𝐴 ∈ dom ℵ →
(ℵ‘𝐴) =
∅) |
17 | | ndmfv 6523 |
. . . . . . 7
⊢ (¬
𝐵 ∈ dom ℵ →
(ℵ‘𝐵) =
∅) |
18 | | djueq12 9121 |
. . . . . . 7
⊢
(((ℵ‘𝐴)
= ∅ ∧ (ℵ‘𝐵) = ∅) → ((ℵ‘𝐴) ⊔ (ℵ‘𝐵)) = (∅ ⊔
∅)) |
19 | 16, 17, 18 | syl2an 586 |
. . . . . 6
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
= (∅ ⊔ ∅)) |
20 | 16 | adantr 473 |
. . . . . . . 8
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ (ℵ‘𝐴) =
∅) |
21 | 17 | adantl 474 |
. . . . . . . 8
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ (ℵ‘𝐵) =
∅) |
22 | 20, 21 | uneq12d 4023 |
. . . . . . 7
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ ((ℵ‘𝐴)
∪ (ℵ‘𝐵)) =
(∅ ∪ ∅)) |
23 | | un0 4224 |
. . . . . . 7
⊢ (∅
∪ ∅) = ∅ |
24 | 22, 23 | syl6eq 2824 |
. . . . . 6
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ ((ℵ‘𝐴)
∪ (ℵ‘𝐵)) =
∅) |
25 | 15, 19, 24 | 3eqtr4a 2834 |
. . . . 5
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
= ((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
26 | 9, 11, 25 | syl2anbr 589 |
. . . 4
⊢ ((¬
𝐴 ∈ On ∧ ¬
𝐵 ∈ On) →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) =
((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
27 | | eqeng 8334 |
. . . 4
⊢
(((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
∈ V → (((ℵ‘𝐴) ⊔ (ℵ‘𝐵)) = ((ℵ‘𝐴) ∪ (ℵ‘𝐵)) → ((ℵ‘𝐴) ⊔ (ℵ‘𝐵)) ≈ ((ℵ‘𝐴) ∪ (ℵ‘𝐵)))) |
28 | 4, 26, 27 | mpsyl 68 |
. . 3
⊢ ((¬
𝐴 ∈ On ∧ ¬
𝐵 ∈ On) →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) ≈
((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
29 | 28 | ex 405 |
. 2
⊢ (¬
𝐴 ∈ On → (¬
𝐵 ∈ On →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) ≈
((ℵ‘𝐴) ∪
(ℵ‘𝐵)))) |
30 | | alephgeom 9296 |
. . 3
⊢ (𝐴 ∈ On ↔ ω
⊆ (ℵ‘𝐴)) |
31 | | ssdomg 8346 |
. . . . 5
⊢
((ℵ‘𝐴)
∈ V → (ω ⊆ (ℵ‘𝐴) → ω ≼
(ℵ‘𝐴))) |
32 | 1, 31 | ax-mp 5 |
. . . 4
⊢ (ω
⊆ (ℵ‘𝐴)
→ ω ≼ (ℵ‘𝐴)) |
33 | | alephon 9283 |
. . . . . 6
⊢
(ℵ‘𝐴)
∈ On |
34 | | onenon 9166 |
. . . . . 6
⊢
((ℵ‘𝐴)
∈ On → (ℵ‘𝐴) ∈ dom card) |
35 | 33, 34 | ax-mp 5 |
. . . . 5
⊢
(ℵ‘𝐴)
∈ dom card |
36 | | alephon 9283 |
. . . . . 6
⊢
(ℵ‘𝐵)
∈ On |
37 | | onenon 9166 |
. . . . . 6
⊢
((ℵ‘𝐵)
∈ On → (ℵ‘𝐵) ∈ dom card) |
38 | 36, 37 | ax-mp 5 |
. . . . 5
⊢
(ℵ‘𝐵)
∈ dom card |
39 | | infdju 9422 |
. . . . 5
⊢
(((ℵ‘𝐴)
∈ dom card ∧ (ℵ‘𝐵) ∈ dom card ∧ ω ≼
(ℵ‘𝐴)) →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) ≈
((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
40 | 35, 38, 39 | mp3an12 1430 |
. . . 4
⊢ (ω
≼ (ℵ‘𝐴)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐴)
∪ (ℵ‘𝐵))) |
41 | 32, 40 | syl 17 |
. . 3
⊢ (ω
⊆ (ℵ‘𝐴)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐴)
∪ (ℵ‘𝐵))) |
42 | 30, 41 | sylbi 209 |
. 2
⊢ (𝐴 ∈ On →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) ≈
((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
43 | | alephgeom 9296 |
. . 3
⊢ (𝐵 ∈ On ↔ ω
⊆ (ℵ‘𝐵)) |
44 | | ssdomg 8346 |
. . . . 5
⊢
((ℵ‘𝐵)
∈ V → (ω ⊆ (ℵ‘𝐵) → ω ≼
(ℵ‘𝐵))) |
45 | 2, 44 | ax-mp 5 |
. . . 4
⊢ (ω
⊆ (ℵ‘𝐵)
→ ω ≼ (ℵ‘𝐵)) |
46 | | djucomen 9395 |
. . . . . . 7
⊢
(((ℵ‘𝐴)
∈ V ∧ (ℵ‘𝐵) ∈ V) → ((ℵ‘𝐴) ⊔ (ℵ‘𝐵)) ≈ ((ℵ‘𝐵) ⊔ (ℵ‘𝐴))) |
47 | 1, 2, 46 | mp2an 679 |
. . . . . 6
⊢
((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐵)
⊔ (ℵ‘𝐴)) |
48 | | infdju 9422 |
. . . . . . 7
⊢
(((ℵ‘𝐵)
∈ dom card ∧ (ℵ‘𝐴) ∈ dom card ∧ ω ≼
(ℵ‘𝐵)) →
((ℵ‘𝐵) ⊔
(ℵ‘𝐴)) ≈
((ℵ‘𝐵) ∪
(ℵ‘𝐴))) |
49 | 38, 35, 48 | mp3an12 1430 |
. . . . . 6
⊢ (ω
≼ (ℵ‘𝐵)
→ ((ℵ‘𝐵)
⊔ (ℵ‘𝐴))
≈ ((ℵ‘𝐵)
∪ (ℵ‘𝐴))) |
50 | | entr 8352 |
. . . . . 6
⊢
((((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐵)
⊔ (ℵ‘𝐴))
∧ ((ℵ‘𝐵)
⊔ (ℵ‘𝐴))
≈ ((ℵ‘𝐵)
∪ (ℵ‘𝐴)))
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐵)
∪ (ℵ‘𝐴))) |
51 | 47, 49, 50 | sylancr 578 |
. . . . 5
⊢ (ω
≼ (ℵ‘𝐵)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐵)
∪ (ℵ‘𝐴))) |
52 | | uncom 4012 |
. . . . 5
⊢
((ℵ‘𝐵)
∪ (ℵ‘𝐴)) =
((ℵ‘𝐴) ∪
(ℵ‘𝐵)) |
53 | 51, 52 | syl6breq 4964 |
. . . 4
⊢ (ω
≼ (ℵ‘𝐵)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐴)
∪ (ℵ‘𝐵))) |
54 | 45, 53 | syl 17 |
. . 3
⊢ (ω
⊆ (ℵ‘𝐵)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐴)
∪ (ℵ‘𝐵))) |
55 | 43, 54 | sylbi 209 |
. 2
⊢ (𝐵 ∈ On →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) ≈
((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
56 | 29, 42, 55 | pm2.61ii 178 |
1
⊢
((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐴)
∪ (ℵ‘𝐵)) |