Step | Hyp | Ref
| Expression |
1 | | fvex 6817 |
. . . . 5
⊢
(ℵ‘𝐴)
∈ V |
2 | | fvex 6817 |
. . . . 5
⊢
(ℵ‘𝐵)
∈ V |
3 | | djuex 9710 |
. . . . 5
⊢
(((ℵ‘𝐴)
∈ V ∧ (ℵ‘𝐵) ∈ V) → ((ℵ‘𝐴) ⊔ (ℵ‘𝐵)) ∈ V) |
4 | 1, 2, 3 | mp2an 690 |
. . . 4
⊢
((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
∈ V |
5 | | alephfnon 9867 |
. . . . . . . 8
⊢ ℵ
Fn On |
6 | 5 | fndmi 6568 |
. . . . . . 7
⊢ dom
ℵ = On |
7 | 6 | eleq2i 2828 |
. . . . . 6
⊢ (𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On) |
8 | 7 | notbii 320 |
. . . . 5
⊢ (¬
𝐴 ∈ dom ℵ ↔
¬ 𝐴 ∈
On) |
9 | 6 | eleq2i 2828 |
. . . . . 6
⊢ (𝐵 ∈ dom ℵ ↔ 𝐵 ∈ On) |
10 | 9 | notbii 320 |
. . . . 5
⊢ (¬
𝐵 ∈ dom ℵ ↔
¬ 𝐵 ∈
On) |
11 | | df-dju 9703 |
. . . . . . 7
⊢ (∅
⊔ ∅) = (({∅} × ∅) ∪ ({1o} ×
∅)) |
12 | | xpundir 5667 |
. . . . . . 7
⊢
(({∅} ∪ {1o}) × ∅) = (({∅}
× ∅) ∪ ({1o} × ∅)) |
13 | | xp0 6076 |
. . . . . . 7
⊢
(({∅} ∪ {1o}) × ∅) =
∅ |
14 | 11, 12, 13 | 3eqtr2i 2770 |
. . . . . 6
⊢ (∅
⊔ ∅) = ∅ |
15 | | ndmfv 6836 |
. . . . . . 7
⊢ (¬
𝐴 ∈ dom ℵ →
(ℵ‘𝐴) =
∅) |
16 | | ndmfv 6836 |
. . . . . . 7
⊢ (¬
𝐵 ∈ dom ℵ →
(ℵ‘𝐵) =
∅) |
17 | | djueq12 9706 |
. . . . . . 7
⊢
(((ℵ‘𝐴)
= ∅ ∧ (ℵ‘𝐵) = ∅) → ((ℵ‘𝐴) ⊔ (ℵ‘𝐵)) = (∅ ⊔
∅)) |
18 | 15, 16, 17 | syl2an 597 |
. . . . . 6
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
= (∅ ⊔ ∅)) |
19 | 15 | adantr 482 |
. . . . . . . 8
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ (ℵ‘𝐴) =
∅) |
20 | 16 | adantl 483 |
. . . . . . . 8
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ (ℵ‘𝐵) =
∅) |
21 | 19, 20 | uneq12d 4104 |
. . . . . . 7
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ ((ℵ‘𝐴)
∪ (ℵ‘𝐵)) =
(∅ ∪ ∅)) |
22 | | un0 4330 |
. . . . . . 7
⊢ (∅
∪ ∅) = ∅ |
23 | 21, 22 | eqtrdi 2792 |
. . . . . 6
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ ((ℵ‘𝐴)
∪ (ℵ‘𝐵)) =
∅) |
24 | 14, 18, 23 | 3eqtr4a 2802 |
. . . . 5
⊢ ((¬
𝐴 ∈ dom ℵ ∧
¬ 𝐵 ∈ dom ℵ)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
= ((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
25 | 8, 10, 24 | syl2anbr 600 |
. . . 4
⊢ ((¬
𝐴 ∈ On ∧ ¬
𝐵 ∈ On) →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) =
((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
26 | | eqeng 8807 |
. . . 4
⊢
(((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
∈ V → (((ℵ‘𝐴) ⊔ (ℵ‘𝐵)) = ((ℵ‘𝐴) ∪ (ℵ‘𝐵)) → ((ℵ‘𝐴) ⊔ (ℵ‘𝐵)) ≈ ((ℵ‘𝐴) ∪ (ℵ‘𝐵)))) |
27 | 4, 25, 26 | mpsyl 68 |
. . 3
⊢ ((¬
𝐴 ∈ On ∧ ¬
𝐵 ∈ On) →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) ≈
((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
28 | 27 | ex 414 |
. 2
⊢ (¬
𝐴 ∈ On → (¬
𝐵 ∈ On →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) ≈
((ℵ‘𝐴) ∪
(ℵ‘𝐵)))) |
29 | | alephgeom 9884 |
. . 3
⊢ (𝐴 ∈ On ↔ ω
⊆ (ℵ‘𝐴)) |
30 | | ssdomg 8821 |
. . . . 5
⊢
((ℵ‘𝐴)
∈ V → (ω ⊆ (ℵ‘𝐴) → ω ≼
(ℵ‘𝐴))) |
31 | 1, 30 | ax-mp 5 |
. . . 4
⊢ (ω
⊆ (ℵ‘𝐴)
→ ω ≼ (ℵ‘𝐴)) |
32 | | alephon 9871 |
. . . . . 6
⊢
(ℵ‘𝐴)
∈ On |
33 | | onenon 9751 |
. . . . . 6
⊢
((ℵ‘𝐴)
∈ On → (ℵ‘𝐴) ∈ dom card) |
34 | 32, 33 | ax-mp 5 |
. . . . 5
⊢
(ℵ‘𝐴)
∈ dom card |
35 | | alephon 9871 |
. . . . . 6
⊢
(ℵ‘𝐵)
∈ On |
36 | | onenon 9751 |
. . . . . 6
⊢
((ℵ‘𝐵)
∈ On → (ℵ‘𝐵) ∈ dom card) |
37 | 35, 36 | ax-mp 5 |
. . . . 5
⊢
(ℵ‘𝐵)
∈ dom card |
38 | | infdju 10010 |
. . . . 5
⊢
(((ℵ‘𝐴)
∈ dom card ∧ (ℵ‘𝐵) ∈ dom card ∧ ω ≼
(ℵ‘𝐴)) →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) ≈
((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
39 | 34, 37, 38 | mp3an12 1451 |
. . . 4
⊢ (ω
≼ (ℵ‘𝐴)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐴)
∪ (ℵ‘𝐵))) |
40 | 31, 39 | syl 17 |
. . 3
⊢ (ω
⊆ (ℵ‘𝐴)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐴)
∪ (ℵ‘𝐵))) |
41 | 29, 40 | sylbi 216 |
. 2
⊢ (𝐴 ∈ On →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) ≈
((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
42 | | alephgeom 9884 |
. . 3
⊢ (𝐵 ∈ On ↔ ω
⊆ (ℵ‘𝐵)) |
43 | | ssdomg 8821 |
. . . . 5
⊢
((ℵ‘𝐵)
∈ V → (ω ⊆ (ℵ‘𝐵) → ω ≼
(ℵ‘𝐵))) |
44 | 2, 43 | ax-mp 5 |
. . . 4
⊢ (ω
⊆ (ℵ‘𝐵)
→ ω ≼ (ℵ‘𝐵)) |
45 | | djucomen 9979 |
. . . . . . 7
⊢
(((ℵ‘𝐴)
∈ V ∧ (ℵ‘𝐵) ∈ V) → ((ℵ‘𝐴) ⊔ (ℵ‘𝐵)) ≈ ((ℵ‘𝐵) ⊔ (ℵ‘𝐴))) |
46 | 1, 2, 45 | mp2an 690 |
. . . . . 6
⊢
((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐵)
⊔ (ℵ‘𝐴)) |
47 | | infdju 10010 |
. . . . . . 7
⊢
(((ℵ‘𝐵)
∈ dom card ∧ (ℵ‘𝐴) ∈ dom card ∧ ω ≼
(ℵ‘𝐵)) →
((ℵ‘𝐵) ⊔
(ℵ‘𝐴)) ≈
((ℵ‘𝐵) ∪
(ℵ‘𝐴))) |
48 | 37, 34, 47 | mp3an12 1451 |
. . . . . 6
⊢ (ω
≼ (ℵ‘𝐵)
→ ((ℵ‘𝐵)
⊔ (ℵ‘𝐴))
≈ ((ℵ‘𝐵)
∪ (ℵ‘𝐴))) |
49 | | entr 8827 |
. . . . . 6
⊢
((((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐵)
⊔ (ℵ‘𝐴))
∧ ((ℵ‘𝐵)
⊔ (ℵ‘𝐴))
≈ ((ℵ‘𝐵)
∪ (ℵ‘𝐴)))
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐵)
∪ (ℵ‘𝐴))) |
50 | 46, 48, 49 | sylancr 588 |
. . . . 5
⊢ (ω
≼ (ℵ‘𝐵)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐵)
∪ (ℵ‘𝐴))) |
51 | | uncom 4093 |
. . . . 5
⊢
((ℵ‘𝐵)
∪ (ℵ‘𝐴)) =
((ℵ‘𝐴) ∪
(ℵ‘𝐵)) |
52 | 50, 51 | breqtrdi 5122 |
. . . 4
⊢ (ω
≼ (ℵ‘𝐵)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐴)
∪ (ℵ‘𝐵))) |
53 | 44, 52 | syl 17 |
. . 3
⊢ (ω
⊆ (ℵ‘𝐵)
→ ((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐴)
∪ (ℵ‘𝐵))) |
54 | 42, 53 | sylbi 216 |
. 2
⊢ (𝐵 ∈ On →
((ℵ‘𝐴) ⊔
(ℵ‘𝐵)) ≈
((ℵ‘𝐴) ∪
(ℵ‘𝐵))) |
55 | 28, 41, 54 | pm2.61ii 183 |
1
⊢
((ℵ‘𝐴)
⊔ (ℵ‘𝐵))
≈ ((ℵ‘𝐴)
∪ (ℵ‘𝐵)) |