Step | Hyp | Ref
| Expression |
1 | | undjudom 10111 |
. . . 4
β’ ((π΄ β Fin β§ π΅ β Fin) β (π΄ βͺ π΅) βΌ (π΄ β π΅)) |
2 | | ficardadju 10143 |
. . . 4
β’ ((π΄ β Fin β§ π΅ β Fin) β (π΄ β π΅) β ((cardβπ΄) +o (cardβπ΅))) |
3 | | domentr 8959 |
. . . 4
β’ (((π΄ βͺ π΅) βΌ (π΄ β π΅) β§ (π΄ β π΅) β ((cardβπ΄) +o (cardβπ΅))) β (π΄ βͺ π΅) βΌ ((cardβπ΄) +o (cardβπ΅))) |
4 | 1, 2, 3 | syl2anc 585 |
. . 3
β’ ((π΄ β Fin β§ π΅ β Fin) β (π΄ βͺ π΅) βΌ ((cardβπ΄) +o (cardβπ΅))) |
5 | | unfi 9122 |
. . . . 5
β’ ((π΄ β Fin β§ π΅ β Fin) β (π΄ βͺ π΅) β Fin) |
6 | | finnum 9892 |
. . . . 5
β’ ((π΄ βͺ π΅) β Fin β (π΄ βͺ π΅) β dom card) |
7 | 5, 6 | syl 17 |
. . . 4
β’ ((π΄ β Fin β§ π΅ β Fin) β (π΄ βͺ π΅) β dom card) |
8 | | ficardom 9905 |
. . . . . 6
β’ (π΄ β Fin β
(cardβπ΄) β
Ο) |
9 | | ficardom 9905 |
. . . . . 6
β’ (π΅ β Fin β
(cardβπ΅) β
Ο) |
10 | | nnacl 8562 |
. . . . . 6
β’
(((cardβπ΄)
β Ο β§ (cardβπ΅) β Ο) β ((cardβπ΄) +o
(cardβπ΅)) β
Ο) |
11 | 8, 9, 10 | syl2an 597 |
. . . . 5
β’ ((π΄ β Fin β§ π΅ β Fin) β
((cardβπ΄)
+o (cardβπ΅)) β Ο) |
12 | | nnon 7812 |
. . . . 5
β’
(((cardβπ΄)
+o (cardβπ΅)) β Ο β ((cardβπ΄) +o
(cardβπ΅)) β
On) |
13 | | onenon 9893 |
. . . . 5
β’
(((cardβπ΄)
+o (cardβπ΅)) β On β ((cardβπ΄) +o
(cardβπ΅)) β dom
card) |
14 | 11, 12, 13 | 3syl 18 |
. . . 4
β’ ((π΄ β Fin β§ π΅ β Fin) β
((cardβπ΄)
+o (cardβπ΅)) β dom card) |
15 | | carddom2 9921 |
. . . 4
β’ (((π΄ βͺ π΅) β dom card β§ ((cardβπ΄) +o
(cardβπ΅)) β dom
card) β ((cardβ(π΄ βͺ π΅)) β (cardβ((cardβπ΄) +o
(cardβπ΅))) β
(π΄ βͺ π΅) βΌ ((cardβπ΄) +o (cardβπ΅)))) |
16 | 7, 14, 15 | syl2anc 585 |
. . 3
β’ ((π΄ β Fin β§ π΅ β Fin) β
((cardβ(π΄ βͺ π΅)) β
(cardβ((cardβπ΄)
+o (cardβπ΅))) β (π΄ βͺ π΅) βΌ ((cardβπ΄) +o (cardβπ΅)))) |
17 | 4, 16 | mpbird 257 |
. 2
β’ ((π΄ β Fin β§ π΅ β Fin) β
(cardβ(π΄ βͺ π΅)) β
(cardβ((cardβπ΄)
+o (cardβπ΅)))) |
18 | | cardnn 9907 |
. . 3
β’
(((cardβπ΄)
+o (cardβπ΅)) β Ο β
(cardβ((cardβπ΄)
+o (cardβπ΅))) = ((cardβπ΄) +o (cardβπ΅))) |
19 | 11, 18 | syl 17 |
. 2
β’ ((π΄ β Fin β§ π΅ β Fin) β
(cardβ((cardβπ΄)
+o (cardβπ΅))) = ((cardβπ΄) +o (cardβπ΅))) |
20 | 17, 19 | sseqtrd 3988 |
1
β’ ((π΄ β Fin β§ π΅ β Fin) β
(cardβ(π΄ βͺ π΅)) β ((cardβπ΄) +o
(cardβπ΅))) |