Proof of Theorem ficardadju
| Step | Hyp | Ref
| Expression |
| 1 | | ficardom 10001 |
. . . 4
⊢ (𝐴 ∈ Fin →
(card‘𝐴) ∈
ω) |
| 2 | | ficardom 10001 |
. . . 4
⊢ (𝐵 ∈ Fin →
(card‘𝐵) ∈
ω) |
| 3 | | nnadju 10238 |
. . . . 5
⊢
(((card‘𝐴)
∈ ω ∧ (card‘𝐵) ∈ ω) →
(card‘((card‘𝐴)
⊔ (card‘𝐵))) =
((card‘𝐴)
+o (card‘𝐵))) |
| 4 | | df-dju 9941 |
. . . . . . 7
⊢
((card‘𝐴)
⊔ (card‘𝐵)) =
(({∅} × (card‘𝐴)) ∪ ({1o} ×
(card‘𝐵))) |
| 5 | | snfi 9083 |
. . . . . . . . 9
⊢ {∅}
∈ Fin |
| 6 | | nnfi 9207 |
. . . . . . . . 9
⊢
((card‘𝐴)
∈ ω → (card‘𝐴) ∈ Fin) |
| 7 | | xpfi 9358 |
. . . . . . . . 9
⊢
(({∅} ∈ Fin ∧ (card‘𝐴) ∈ Fin) → ({∅} ×
(card‘𝐴)) ∈
Fin) |
| 8 | 5, 6, 7 | sylancr 587 |
. . . . . . . 8
⊢
((card‘𝐴)
∈ ω → ({∅} × (card‘𝐴)) ∈ Fin) |
| 9 | | snfi 9083 |
. . . . . . . . 9
⊢
{1o} ∈ Fin |
| 10 | | nnfi 9207 |
. . . . . . . . 9
⊢
((card‘𝐵)
∈ ω → (card‘𝐵) ∈ Fin) |
| 11 | | xpfi 9358 |
. . . . . . . . 9
⊢
(({1o} ∈ Fin ∧ (card‘𝐵) ∈ Fin) → ({1o}
× (card‘𝐵))
∈ Fin) |
| 12 | 9, 10, 11 | sylancr 587 |
. . . . . . . 8
⊢
((card‘𝐵)
∈ ω → ({1o} × (card‘𝐵)) ∈ Fin) |
| 13 | | unfi 9211 |
. . . . . . . 8
⊢
((({∅} × (card‘𝐴)) ∈ Fin ∧ ({1o} ×
(card‘𝐵)) ∈ Fin)
→ (({∅} × (card‘𝐴)) ∪ ({1o} ×
(card‘𝐵))) ∈
Fin) |
| 14 | 8, 12, 13 | syl2an 596 |
. . . . . . 7
⊢
(((card‘𝐴)
∈ ω ∧ (card‘𝐵) ∈ ω) → (({∅} ×
(card‘𝐴)) ∪
({1o} × (card‘𝐵))) ∈ Fin) |
| 15 | 4, 14 | eqeltrid 2845 |
. . . . . 6
⊢
(((card‘𝐴)
∈ ω ∧ (card‘𝐵) ∈ ω) → ((card‘𝐴) ⊔ (card‘𝐵)) ∈ Fin) |
| 16 | | ficardid 10002 |
. . . . . 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 5167 |
. . . 4
⊢
(((card‘𝐴)
∈ ω ∧ (card‘𝐵) ∈ ω) → ((card‘𝐴) +o
(card‘𝐵)) ≈
((card‘𝐴) ⊔
(card‘𝐵))) |
| 19 | 1, 2, 18 | syl2an 596 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((card‘𝐴)
+o (card‘𝐵)) ≈ ((card‘𝐴) ⊔ (card‘𝐵))) |
| 20 | | ficardid 10002 |
. . . 4
⊢ (𝐴 ∈ Fin →
(card‘𝐴) ≈
𝐴) |
| 21 | | ficardid 10002 |
. . . 4
⊢ (𝐵 ∈ Fin →
(card‘𝐵) ≈
𝐵) |
| 22 | | djuen 10210 |
. . . 4
⊢
(((card‘𝐴)
≈ 𝐴 ∧
(card‘𝐵) ≈
𝐵) →
((card‘𝐴) ⊔
(card‘𝐵)) ≈
(𝐴 ⊔ 𝐵)) |
| 23 | 20, 21, 22 | syl2an 596 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((card‘𝐴) ⊔
(card‘𝐵)) ≈
(𝐴 ⊔ 𝐵)) |
| 24 | | entr 9046 |
. . 3
⊢
((((card‘𝐴)
+o (card‘𝐵)) ≈ ((card‘𝐴) ⊔ (card‘𝐵)) ∧ ((card‘𝐴) ⊔ (card‘𝐵)) ≈ (𝐴 ⊔ 𝐵)) → ((card‘𝐴) +o (card‘𝐵)) ≈ (𝐴 ⊔ 𝐵)) |
| 25 | 19, 23, 24 | syl2anc 584 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((card‘𝐴)
+o (card‘𝐵)) ≈ (𝐴 ⊔ 𝐵)) |
| 26 | 25 | ensymd 9045 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ⊔ 𝐵) ≈ ((card‘𝐴) +o (card‘𝐵))) |