Proof of Theorem ficardadju
Step | Hyp | Ref
| Expression |
1 | | ficardom 9408 |
. . . 4
⊢ (𝐴 ∈ Fin →
(card‘𝐴) ∈
ω) |
2 | | ficardom 9408 |
. . . 4
⊢ (𝐵 ∈ Fin →
(card‘𝐵) ∈
ω) |
3 | | nnadju 9642 |
. . . . 5
⊢
(((card‘𝐴)
∈ ω ∧ (card‘𝐵) ∈ ω) →
(card‘((card‘𝐴)
⊔ (card‘𝐵))) =
((card‘𝐴)
+o (card‘𝐵))) |
4 | | df-dju 9348 |
. . . . . . 7
⊢
((card‘𝐴)
⊔ (card‘𝐵)) =
(({∅} × (card‘𝐴)) ∪ ({1o} ×
(card‘𝐵))) |
5 | | snfi 8607 |
. . . . . . . . 9
⊢ {∅}
∈ Fin |
6 | | nnfi 8726 |
. . . . . . . . 9
⊢
((card‘𝐴)
∈ ω → (card‘𝐴) ∈ Fin) |
7 | | xpfi 8807 |
. . . . . . . . 9
⊢
(({∅} ∈ Fin ∧ (card‘𝐴) ∈ Fin) → ({∅} ×
(card‘𝐴)) ∈
Fin) |
8 | 5, 6, 7 | sylancr 591 |
. . . . . . . 8
⊢
((card‘𝐴)
∈ ω → ({∅} × (card‘𝐴)) ∈ Fin) |
9 | | snfi 8607 |
. . . . . . . . 9
⊢
{1o} ∈ Fin |
10 | | nnfi 8726 |
. . . . . . . . 9
⊢
((card‘𝐵)
∈ ω → (card‘𝐵) ∈ Fin) |
11 | | xpfi 8807 |
. . . . . . . . 9
⊢
(({1o} ∈ Fin ∧ (card‘𝐵) ∈ Fin) → ({1o}
× (card‘𝐵))
∈ Fin) |
12 | 9, 10, 11 | sylancr 591 |
. . . . . . . 8
⊢
((card‘𝐵)
∈ ω → ({1o} × (card‘𝐵)) ∈ Fin) |
13 | | unfi 8803 |
. . . . . . . 8
⊢
((({∅} × (card‘𝐴)) ∈ Fin ∧ ({1o} ×
(card‘𝐵)) ∈ Fin)
→ (({∅} × (card‘𝐴)) ∪ ({1o} ×
(card‘𝐵))) ∈
Fin) |
14 | 8, 12, 13 | syl2an 599 |
. . . . . . 7
⊢
(((card‘𝐴)
∈ ω ∧ (card‘𝐵) ∈ ω) → (({∅} ×
(card‘𝐴)) ∪
({1o} × (card‘𝐵))) ∈ Fin) |
15 | 4, 14 | eqeltrid 2855 |
. . . . . 6
⊢
(((card‘𝐴)
∈ ω ∧ (card‘𝐵) ∈ ω) → ((card‘𝐴) ⊔ (card‘𝐵)) ∈ Fin) |
16 | | ficardid 9409 |
. . . . . 6
⊢
(((card‘𝐴)
⊔ (card‘𝐵))
∈ Fin → (card‘((card‘𝐴) ⊔ (card‘𝐵))) ≈ ((card‘𝐴) ⊔ (card‘𝐵))) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢
(((card‘𝐴)
∈ ω ∧ (card‘𝐵) ∈ ω) →
(card‘((card‘𝐴)
⊔ (card‘𝐵)))
≈ ((card‘𝐴)
⊔ (card‘𝐵))) |
18 | 3, 17 | eqbrtrrd 5049 |
. . . 4
⊢
(((card‘𝐴)
∈ ω ∧ (card‘𝐵) ∈ ω) → ((card‘𝐴) +o
(card‘𝐵)) ≈
((card‘𝐴) ⊔
(card‘𝐵))) |
19 | 1, 2, 18 | syl2an 599 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((card‘𝐴)
+o (card‘𝐵)) ≈ ((card‘𝐴) ⊔ (card‘𝐵))) |
20 | | ficardid 9409 |
. . . 4
⊢ (𝐴 ∈ Fin →
(card‘𝐴) ≈
𝐴) |
21 | | ficardid 9409 |
. . . 4
⊢ (𝐵 ∈ Fin →
(card‘𝐵) ≈
𝐵) |
22 | | djuen 9614 |
. . . 4
⊢
(((card‘𝐴)
≈ 𝐴 ∧
(card‘𝐵) ≈
𝐵) →
((card‘𝐴) ⊔
(card‘𝐵)) ≈
(𝐴 ⊔ 𝐵)) |
23 | 20, 21, 22 | syl2an 599 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((card‘𝐴) ⊔
(card‘𝐵)) ≈
(𝐴 ⊔ 𝐵)) |
24 | | entr 8572 |
. . 3
⊢
((((card‘𝐴)
+o (card‘𝐵)) ≈ ((card‘𝐴) ⊔ (card‘𝐵)) ∧ ((card‘𝐴) ⊔ (card‘𝐵)) ≈ (𝐴 ⊔ 𝐵)) → ((card‘𝐴) +o (card‘𝐵)) ≈ (𝐴 ⊔ 𝐵)) |
25 | 19, 23, 24 | syl2anc 588 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((card‘𝐴)
+o (card‘𝐵)) ≈ (𝐴 ⊔ 𝐵)) |
26 | 25 | ensymd 8571 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ⊔ 𝐵) ≈ ((card‘𝐴) +o (card‘𝐵))) |