Step | Hyp | Ref
| Expression |
1 | | finnum 9892 |
. . . . . . 7
β’ (π΄ β Fin β π΄ β dom
card) |
2 | | finnum 9892 |
. . . . . . 7
β’ (π΅ β Fin β π΅ β dom
card) |
3 | | cardadju 10138 |
. . . . . . 7
β’ ((π΄ β dom card β§ π΅ β dom card) β (π΄ β π΅) β ((cardβπ΄) +o (cardβπ΅))) |
4 | 1, 2, 3 | syl2an 597 |
. . . . . 6
β’ ((π΄ β Fin β§ π΅ β Fin) β (π΄ β π΅) β ((cardβπ΄) +o (cardβπ΅))) |
5 | 4 | 3adant3 1133 |
. . . . 5
β’ ((π΄ β Fin β§ π΅ β Fin β§ (π΄ β© π΅) = β
) β (π΄ β π΅) β ((cardβπ΄) +o (cardβπ΅))) |
6 | 5 | ensymd 8951 |
. . . 4
β’ ((π΄ β Fin β§ π΅ β Fin β§ (π΄ β© π΅) = β
) β ((cardβπ΄) +o
(cardβπ΅)) β
(π΄ β π΅)) |
7 | | endjudisj 10112 |
. . . 4
β’ ((π΄ β Fin β§ π΅ β Fin β§ (π΄ β© π΅) = β
) β (π΄ β π΅) β (π΄ βͺ π΅)) |
8 | | entr 8952 |
. . . 4
β’
((((cardβπ΄)
+o (cardβπ΅)) β (π΄ β π΅) β§ (π΄ β π΅) β (π΄ βͺ π΅)) β ((cardβπ΄) +o (cardβπ΅)) β (π΄ βͺ π΅)) |
9 | 6, 7, 8 | syl2anc 585 |
. . 3
β’ ((π΄ β Fin β§ π΅ β Fin β§ (π΄ β© π΅) = β
) β ((cardβπ΄) +o
(cardβπ΅)) β
(π΄ βͺ π΅)) |
10 | | carden2b 9911 |
. . 3
β’
(((cardβπ΄)
+o (cardβπ΅)) β (π΄ βͺ π΅) β (cardβ((cardβπ΄) +o
(cardβπ΅))) =
(cardβ(π΄ βͺ π΅))) |
11 | 9, 10 | syl 17 |
. 2
β’ ((π΄ β Fin β§ π΅ β Fin β§ (π΄ β© π΅) = β
) β
(cardβ((cardβπ΄)
+o (cardβπ΅))) = (cardβ(π΄ βͺ π΅))) |
12 | | ficardom 9905 |
. . . 4
β’ (π΄ β Fin β
(cardβπ΄) β
Ο) |
13 | | ficardom 9905 |
. . . 4
β’ (π΅ β Fin β
(cardβπ΅) β
Ο) |
14 | | nnacl 8562 |
. . . . 5
β’
(((cardβπ΄)
β Ο β§ (cardβπ΅) β Ο) β ((cardβπ΄) +o
(cardβπ΅)) β
Ο) |
15 | | cardnn 9907 |
. . . . 5
β’
(((cardβπ΄)
+o (cardβπ΅)) β Ο β
(cardβ((cardβπ΄)
+o (cardβπ΅))) = ((cardβπ΄) +o (cardβπ΅))) |
16 | 14, 15 | syl 17 |
. . . 4
β’
(((cardβπ΄)
β Ο β§ (cardβπ΅) β Ο) β
(cardβ((cardβπ΄)
+o (cardβπ΅))) = ((cardβπ΄) +o (cardβπ΅))) |
17 | 12, 13, 16 | syl2an 597 |
. . 3
β’ ((π΄ β Fin β§ π΅ β Fin) β
(cardβ((cardβπ΄)
+o (cardβπ΅))) = ((cardβπ΄) +o (cardβπ΅))) |
18 | 17 | 3adant3 1133 |
. 2
β’ ((π΄ β Fin β§ π΅ β Fin β§ (π΄ β© π΅) = β
) β
(cardβ((cardβπ΄)
+o (cardβπ΅))) = ((cardβπ΄) +o (cardβπ΅))) |
19 | 11, 18 | eqtr3d 2775 |
1
β’ ((π΄ β Fin β§ π΅ β Fin β§ (π΄ β© π΅) = β
) β (cardβ(π΄ βͺ π΅)) = ((cardβπ΄) +o (cardβπ΅))) |