Proof of Theorem alephadd
Step | Hyp | Ref
| Expression |
1 | | fvex 6678 |
. . . . 5
⊢
(ℵ‘𝐴)
∈ V |
2 | | fvex 6678 |
. . . . 5
⊢
(ℵ‘𝐵)
∈ V |
3 | | djuex 9331 |
. . . . 5
⊢
(((ℵ‘𝐴)
∈ V ∧ (ℵ‘𝐵) ∈ V) → ((ℵ‘𝐴) ⊔ (ℵ‘𝐵)) ∈ V) |
4 | 1, 2, 3 | mp2an 690 |
. . . 4
⊢
((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
∈ V |
5 | | alephfnon 9485 |
. . . . . . . 8
⊢ ℵ
Fn On |
6 | | fndm 6450 |
. . . . . . . 8
⊢ (ℵ
Fn On → dom ℵ = On) |
7 | 5, 6 | ax-mp 5 |
. . . . . . 7
⊢ dom
ℵ = On |
8 | 7 | eleq2i 2904 |
. . . . . 6
⊢ (𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On) |
9 | 8 | notbii 322 |
. . . . 5
⊢ (¬
𝐴 ∈ dom ℵ ↔
¬ 𝐴 ∈
On) |
10 | 7 | eleq2i 2904 |
. . . . . 6
⊢ (𝐵 ∈ dom ℵ ↔ 𝐵 ∈ On) |
11 | 10 | notbii 322 |
. . . . 5
⊢ (¬
𝐵 ∈ dom ℵ ↔
¬ 𝐵 ∈
On) |
12 | | df-dju 9324 |
. . . . . . 7
⊢ (∅
⊔ ∅) = (({∅} × ∅) ∪ ({1o} ×
∅)) |
13 | | xpundir 5616 |
. . . . . . 7
⊢
(({∅} ∪ {1o}) × ∅) = (({∅}
× ∅) ∪ ({1o} × ∅)) |
14 | | xp0 6010 |
. . . . . . 7
⊢
(({∅} ∪ {1o}) × ∅) =
∅ |
15 | 12, 13, 14 | 3eqtr2i 2850 |
. . . . . 6
⊢ (∅
⊔ ∅) = ∅ |
16 | | ndmfv 6695 |
. . . . . . 7
⊢ (¬
𝐴 ∈ dom ℵ →
(ℵ‘𝐴) =
∅) |
17 | | ndmfv 6695 |
. . . . . . 7
⊢ (¬
𝐵 ∈ dom ℵ →
(ℵ‘𝐵) =
∅) |
18 | | djueq12 9327 |
. . . . . . 7
⊢
(((ℵ‘𝐴)
= ∅ ∧ (ℵ‘𝐵) = ∅) → ((ℵ‘𝐴) ⊔ (ℵ‘𝐵)) = (∅ ⊔
∅)) |
19 | 16, 17, 18 | syl2an 597 |
. . . . . 6
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
= (∅ ⊔ ∅)) |
20 | 16 | adantr 483 |
. . . . . . . 8
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ (ℵ‘𝐴) =
∅) |
21 | 17 | adantl 484 |
. . . . . . . 8
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ (ℵ‘𝐵) =
∅) |
22 | 20, 21 | uneq12d 4140 |
. . . . . . 7
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ ((ℵ‘𝐴)
∪ (ℵ‘𝐵)) =
(∅ ∪ ∅)) |
23 | | un0 4344 |
. . . . . . 7
⊢ (∅
∪ ∅) = ∅ |
24 | 22, 23 | syl6eq 2872 |
. . . . . 6
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ ((ℵ‘𝐴)
∪ (ℵ‘𝐵)) =
∅) |
25 | 15, 19, 24 | 3eqtr4a 2882 |
. . . . 5
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
= ((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
26 | 9, 11, 25 | syl2anbr 600 |
. . . 4
⊢ ((¬
𝐴 ∈ On ∧ ¬
𝐵 ∈ On) →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) =
((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
27 | | eqeng 8537 |
. . . 4
⊢
(((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
∈ V → (((ℵ‘𝐴) ⊔ (ℵ‘𝐵)) = ((ℵ‘𝐴) ∪ (ℵ‘𝐵)) → ((ℵ‘𝐴) ⊔ (ℵ‘𝐵)) ≈ ((ℵ‘𝐴) ∪ (ℵ‘𝐵)))) |
28 | 4, 26, 27 | mpsyl 68 |
. . 3
⊢ ((¬
𝐴 ∈ On ∧ ¬
𝐵 ∈ On) →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) ≈
((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
29 | 28 | ex 415 |
. 2
⊢ (¬
𝐴 ∈ On → (¬
𝐵 ∈ On →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) ≈
((ℵ‘𝐴) ∪
(ℵ‘𝐵)))) |
30 | | alephgeom 9502 |
. . 3
⊢ (𝐴 ∈ On ↔ ω
⊆ (ℵ‘𝐴)) |
31 | | ssdomg 8549 |
. . . . 5
⊢
((ℵ‘𝐴)
∈ V → (ω ⊆ (ℵ‘𝐴) → ω ≼
(ℵ‘𝐴))) |
32 | 1, 31 | ax-mp 5 |
. . . 4
⊢ (ω
⊆ (ℵ‘𝐴)
→ ω ≼ (ℵ‘𝐴)) |
33 | | alephon 9489 |
. . . . . 6
⊢
(ℵ‘𝐴)
∈ On |
34 | | onenon 9372 |
. . . . . 6
⊢
((ℵ‘𝐴)
∈ On → (ℵ‘𝐴) ∈ dom card) |
35 | 33, 34 | ax-mp 5 |
. . . . 5
⊢
(ℵ‘𝐴)
∈ dom card |
36 | | alephon 9489 |
. . . . . 6
⊢
(ℵ‘𝐵)
∈ On |
37 | | onenon 9372 |
. . . . . 6
⊢
((ℵ‘𝐵)
∈ On → (ℵ‘𝐵) ∈ dom card) |
38 | 36, 37 | ax-mp 5 |
. . . . 5
⊢
(ℵ‘𝐵)
∈ dom card |
39 | | infdju 9624 |
. . . . 5
⊢
(((ℵ‘𝐴)
∈ dom card ∧ (ℵ‘𝐵) ∈ dom card ∧ ω ≼
(ℵ‘𝐴)) →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) ≈
((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
40 | 35, 38, 39 | mp3an12 1447 |
. . . 4
⊢ (ω
≼ (ℵ‘𝐴)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐴)
∪ (ℵ‘𝐵))) |
41 | 32, 40 | syl 17 |
. . 3
⊢ (ω
⊆ (ℵ‘𝐴)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐴)
∪ (ℵ‘𝐵))) |
42 | 30, 41 | sylbi 219 |
. 2
⊢ (𝐴 ∈ On →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) ≈
((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
43 | | alephgeom 9502 |
. . 3
⊢ (𝐵 ∈ On ↔ ω
⊆ (ℵ‘𝐵)) |
44 | | ssdomg 8549 |
. . . . 5
⊢
((ℵ‘𝐵)
∈ V → (ω ⊆ (ℵ‘𝐵) → ω ≼
(ℵ‘𝐵))) |
45 | 2, 44 | ax-mp 5 |
. . . 4
⊢ (ω
⊆ (ℵ‘𝐵)
→ ω ≼ (ℵ‘𝐵)) |
46 | | djucomen 9597 |
. . . . . . 7
⊢
(((ℵ‘𝐴)
∈ V ∧ (ℵ‘𝐵) ∈ V) → ((ℵ‘𝐴) ⊔ (ℵ‘𝐵)) ≈ ((ℵ‘𝐵) ⊔ (ℵ‘𝐴))) |
47 | 1, 2, 46 | mp2an 690 |
. . . . . 6
⊢
((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐵)
⊔ (ℵ‘𝐴)) |
48 | | infdju 9624 |
. . . . . . 7
⊢
(((ℵ‘𝐵)
∈ dom card ∧ (ℵ‘𝐴) ∈ dom card ∧ ω ≼
(ℵ‘𝐵)) →
((ℵ‘𝐵) ⊔
(ℵ‘𝐴)) ≈
((ℵ‘𝐵) ∪
(ℵ‘𝐴))) |
49 | 38, 35, 48 | mp3an12 1447 |
. . . . . 6
⊢ (ω
≼ (ℵ‘𝐵)
→ ((ℵ‘𝐵)
⊔ (ℵ‘𝐴))
≈ ((ℵ‘𝐵)
∪ (ℵ‘𝐴))) |
50 | | entr 8555 |
. . . . . 6
⊢
((((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐵)
⊔ (ℵ‘𝐴))
∧ ((ℵ‘𝐵)
⊔ (ℵ‘𝐴))
≈ ((ℵ‘𝐵)
∪ (ℵ‘𝐴)))
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐵)
∪ (ℵ‘𝐴))) |
51 | 47, 49, 50 | sylancr 589 |
. . . . 5
⊢ (ω
≼ (ℵ‘𝐵)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐵)
∪ (ℵ‘𝐴))) |
52 | | uncom 4129 |
. . . . 5
⊢
((ℵ‘𝐵)
∪ (ℵ‘𝐴)) =
((ℵ‘𝐴) ∪
(ℵ‘𝐵)) |
53 | 51, 52 | breqtrdi 5100 |
. . . 4
⊢ (ω
≼ (ℵ‘𝐵)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐴)
∪ (ℵ‘𝐵))) |
54 | 45, 53 | syl 17 |
. . 3
⊢ (ω
⊆ (ℵ‘𝐵)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐴)
∪ (ℵ‘𝐵))) |
55 | 43, 54 | sylbi 219 |
. 2
⊢ (𝐵 ∈ On →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) ≈
((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
56 | 29, 42, 55 | pm2.61ii 185 |
1
⊢
((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐴)
∪ (ℵ‘𝐵)) |