Step | Hyp | Ref
| Expression |
1 | | xpeq1 4625 |
. . . 4
⊢ (𝑥 = ∅ → (𝑥 × 𝐵) = (∅ × 𝐵)) |
2 | 1 | fveq2d 5500 |
. . 3
⊢ (𝑥 = ∅ →
(♯‘(𝑥 ×
𝐵)) =
(♯‘(∅ × 𝐵))) |
3 | | fveq2 5496 |
. . . 4
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
(♯‘∅)) |
4 | 3 | oveq1d 5868 |
. . 3
⊢ (𝑥 = ∅ →
((♯‘𝑥) ·
(♯‘𝐵)) =
((♯‘∅) · (♯‘𝐵))) |
5 | 2, 4 | eqeq12d 2185 |
. 2
⊢ (𝑥 = ∅ →
((♯‘(𝑥 ×
𝐵)) = ((♯‘𝑥) · (♯‘𝐵)) ↔
(♯‘(∅ × 𝐵)) = ((♯‘∅) ·
(♯‘𝐵)))) |
6 | | xpeq1 4625 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑥 × 𝐵) = (𝑦 × 𝐵)) |
7 | 6 | fveq2d 5500 |
. . 3
⊢ (𝑥 = 𝑦 → (♯‘(𝑥 × 𝐵)) = (♯‘(𝑦 × 𝐵))) |
8 | | fveq2 5496 |
. . . 4
⊢ (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦)) |
9 | 8 | oveq1d 5868 |
. . 3
⊢ (𝑥 = 𝑦 → ((♯‘𝑥) · (♯‘𝐵)) = ((♯‘𝑦) · (♯‘𝐵))) |
10 | 7, 9 | eqeq12d 2185 |
. 2
⊢ (𝑥 = 𝑦 → ((♯‘(𝑥 × 𝐵)) = ((♯‘𝑥) · (♯‘𝐵)) ↔ (♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵)))) |
11 | | xpeq1 4625 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥 × 𝐵) = ((𝑦 ∪ {𝑧}) × 𝐵)) |
12 | 11 | fveq2d 5500 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘(𝑥 × 𝐵)) = (♯‘((𝑦 ∪ {𝑧}) × 𝐵))) |
13 | | fveq2 5496 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (♯‘𝑥) = (♯‘(𝑦 ∪ {𝑧}))) |
14 | 13 | oveq1d 5868 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘𝑥) · (♯‘𝐵)) = ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵))) |
15 | 12, 14 | eqeq12d 2185 |
. 2
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((♯‘(𝑥 × 𝐵)) = ((♯‘𝑥) · (♯‘𝐵)) ↔ (♯‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵)))) |
16 | | xpeq1 4625 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑥 × 𝐵) = (𝐴 × 𝐵)) |
17 | 16 | fveq2d 5500 |
. . 3
⊢ (𝑥 = 𝐴 → (♯‘(𝑥 × 𝐵)) = (♯‘(𝐴 × 𝐵))) |
18 | | fveq2 5496 |
. . . 4
⊢ (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴)) |
19 | 18 | oveq1d 5868 |
. . 3
⊢ (𝑥 = 𝐴 → ((♯‘𝑥) · (♯‘𝐵)) = ((♯‘𝐴) · (♯‘𝐵))) |
20 | 17, 19 | eqeq12d 2185 |
. 2
⊢ (𝑥 = 𝐴 → ((♯‘(𝑥 × 𝐵)) = ((♯‘𝑥) · (♯‘𝐵)) ↔ (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) · (♯‘𝐵)))) |
21 | | 0xp 4691 |
. . . . 5
⊢ (∅
× 𝐵) =
∅ |
22 | 21 | fveq2i 5499 |
. . . 4
⊢
(♯‘(∅ × 𝐵)) =
(♯‘∅) |
23 | | hash0 10731 |
. . . 4
⊢
(♯‘∅) = 0 |
24 | 22, 23 | eqtri 2191 |
. . 3
⊢
(♯‘(∅ × 𝐵)) = 0 |
25 | 23 | oveq1i 5863 |
. . . 4
⊢
((♯‘∅) · (♯‘𝐵)) = (0 · (♯‘𝐵)) |
26 | | hashcl 10715 |
. . . . . . 7
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℕ0) |
27 | 26 | nn0cnd 9190 |
. . . . . 6
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℂ) |
28 | 27 | mul02d 8311 |
. . . . 5
⊢ (𝐵 ∈ Fin → (0 ·
(♯‘𝐵)) =
0) |
29 | 28 | adantl 275 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (0 ·
(♯‘𝐵)) =
0) |
30 | 25, 29 | eqtrid 2215 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘∅) · (♯‘𝐵)) = 0) |
31 | 24, 30 | eqtr4id 2222 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(∅ × 𝐵)) = ((♯‘∅) ·
(♯‘𝐵))) |
32 | | oveq1 5860 |
. . . . 5
⊢
((♯‘(𝑦
× 𝐵)) =
((♯‘𝑦) ·
(♯‘𝐵)) →
((♯‘(𝑦 ×
𝐵)) + (♯‘𝐵)) = (((♯‘𝑦) · (♯‘𝐵)) + (♯‘𝐵))) |
33 | 32 | adantl 275 |
. . . 4
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ (♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵))) → ((♯‘(𝑦 × 𝐵)) + (♯‘𝐵)) = (((♯‘𝑦) · (♯‘𝐵)) + (♯‘𝐵))) |
34 | | xpundir 4668 |
. . . . . . 7
⊢ ((𝑦 ∪ {𝑧}) × 𝐵) = ((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵)) |
35 | 34 | fveq2i 5499 |
. . . . . 6
⊢
(♯‘((𝑦
∪ {𝑧}) × 𝐵)) = (♯‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) |
36 | | simplr 525 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑦 ∈ Fin) |
37 | | simpllr 529 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝐵 ∈ Fin) |
38 | | xpfi 6907 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝑦 × 𝐵) ∈ Fin) |
39 | 36, 37, 38 | syl2anc 409 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝑦 × 𝐵) ∈ Fin) |
40 | | vex 2733 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
41 | | snfig 6792 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ V → {𝑧} ∈ Fin) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . . . 10
⊢ {𝑧} ∈ Fin |
43 | | xpfi 6907 |
. . . . . . . . . 10
⊢ (({𝑧} ∈ Fin ∧ 𝐵 ∈ Fin) → ({𝑧} × 𝐵) ∈ Fin) |
44 | 42, 43 | mpan 422 |
. . . . . . . . 9
⊢ (𝐵 ∈ Fin → ({𝑧} × 𝐵) ∈ Fin) |
45 | 44 | ad3antlr 490 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ({𝑧} × 𝐵) ∈ Fin) |
46 | | simprr 527 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ (𝐴 ∖ 𝑦)) |
47 | 46 | eldifbd 3133 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ¬ 𝑧 ∈ 𝑦) |
48 | | inxp 4745 |
. . . . . . . . . 10
⊢ ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ((𝑦 ∩ {𝑧}) × (𝐵 ∩ 𝐵)) |
49 | | disjsn 3645 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦) |
50 | 49 | biimpri 132 |
. . . . . . . . . . . 12
⊢ (¬
𝑧 ∈ 𝑦 → (𝑦 ∩ {𝑧}) = ∅) |
51 | 50 | xpeq1d 4634 |
. . . . . . . . . . 11
⊢ (¬
𝑧 ∈ 𝑦 → ((𝑦 ∩ {𝑧}) × (𝐵 ∩ 𝐵)) = (∅ × (𝐵 ∩ 𝐵))) |
52 | | 0xp 4691 |
. . . . . . . . . . 11
⊢ (∅
× (𝐵 ∩ 𝐵)) = ∅ |
53 | 51, 52 | eqtrdi 2219 |
. . . . . . . . . 10
⊢ (¬
𝑧 ∈ 𝑦 → ((𝑦 ∩ {𝑧}) × (𝐵 ∩ 𝐵)) = ∅) |
54 | 48, 53 | eqtrid 2215 |
. . . . . . . . 9
⊢ (¬
𝑧 ∈ 𝑦 → ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ∅) |
55 | 47, 54 | syl 14 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ∅) |
56 | | hashun 10740 |
. . . . . . . 8
⊢ (((𝑦 × 𝐵) ∈ Fin ∧ ({𝑧} × 𝐵) ∈ Fin ∧ ((𝑦 × 𝐵) ∩ ({𝑧} × 𝐵)) = ∅) → (♯‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((♯‘(𝑦 × 𝐵)) + (♯‘({𝑧} × 𝐵)))) |
57 | 39, 45, 55, 56 | syl3anc 1233 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (♯‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((♯‘(𝑦 × 𝐵)) + (♯‘({𝑧} × 𝐵)))) |
58 | 40 | snex 4171 |
. . . . . . . . . . . 12
⊢ {𝑧} ∈ V |
59 | 58 | a1i 9 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → {𝑧} ∈ V) |
60 | | xpcomeng 6806 |
. . . . . . . . . . 11
⊢ (({𝑧} ∈ V ∧ 𝐵 ∈ Fin) → ({𝑧} × 𝐵) ≈ (𝐵 × {𝑧})) |
61 | 59, 37, 60 | syl2anc 409 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ({𝑧} × 𝐵) ≈ (𝐵 × {𝑧})) |
62 | 40 | a1i 9 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → 𝑧 ∈ V) |
63 | | xpsneng 6800 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ Fin ∧ 𝑧 ∈ V) → (𝐵 × {𝑧}) ≈ 𝐵) |
64 | 37, 62, 63 | syl2anc 409 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (𝐵 × {𝑧}) ≈ 𝐵) |
65 | | entr 6762 |
. . . . . . . . . 10
⊢ ((({𝑧} × 𝐵) ≈ (𝐵 × {𝑧}) ∧ (𝐵 × {𝑧}) ≈ 𝐵) → ({𝑧} × 𝐵) ≈ 𝐵) |
66 | 61, 64, 65 | syl2anc 409 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ({𝑧} × 𝐵) ≈ 𝐵) |
67 | | hashen 10718 |
. . . . . . . . . 10
⊢ ((({𝑧} × 𝐵) ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘({𝑧} × 𝐵)) = (♯‘𝐵) ↔ ({𝑧} × 𝐵) ≈ 𝐵)) |
68 | 45, 37, 67 | syl2anc 409 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((♯‘({𝑧} × 𝐵)) = (♯‘𝐵) ↔ ({𝑧} × 𝐵) ≈ 𝐵)) |
69 | 66, 68 | mpbird 166 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (♯‘({𝑧} × 𝐵)) = (♯‘𝐵)) |
70 | 69 | oveq2d 5869 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((♯‘(𝑦 × 𝐵)) + (♯‘({𝑧} × 𝐵))) = ((♯‘(𝑦 × 𝐵)) + (♯‘𝐵))) |
71 | 57, 70 | eqtrd 2203 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (♯‘((𝑦 × 𝐵) ∪ ({𝑧} × 𝐵))) = ((♯‘(𝑦 × 𝐵)) + (♯‘𝐵))) |
72 | 35, 71 | eqtrid 2215 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (♯‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((♯‘(𝑦 × 𝐵)) + (♯‘𝐵))) |
73 | 72 | adantr 274 |
. . . 4
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ (♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵))) → (♯‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((♯‘(𝑦 × 𝐵)) + (♯‘𝐵))) |
74 | | hashunsng 10742 |
. . . . . . . . 9
⊢ (𝑧 ∈ V → ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1))) |
75 | 40, 74 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (♯‘(𝑦 ∪ {𝑧})) = ((♯‘𝑦) + 1)) |
76 | 75 | oveq1d 5868 |
. . . . . . 7
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵)) = (((♯‘𝑦) + 1) · (♯‘𝐵))) |
77 | 36, 47, 76 | syl2anc 409 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵)) = (((♯‘𝑦) + 1) · (♯‘𝐵))) |
78 | | hashcl 10715 |
. . . . . . . . 9
⊢ (𝑦 ∈ Fin →
(♯‘𝑦) ∈
ℕ0) |
79 | 78 | nn0cnd 9190 |
. . . . . . . 8
⊢ (𝑦 ∈ Fin →
(♯‘𝑦) ∈
ℂ) |
80 | 36, 79 | syl 14 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (♯‘𝑦) ∈ ℂ) |
81 | 37, 27 | syl 14 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (♯‘𝐵) ∈ ℂ) |
82 | 80, 81 | adddirp1d 7946 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → (((♯‘𝑦) + 1) ·
(♯‘𝐵)) =
(((♯‘𝑦)
· (♯‘𝐵))
+ (♯‘𝐵))) |
83 | 77, 82 | eqtrd 2203 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵)) = (((♯‘𝑦) · (♯‘𝐵)) + (♯‘𝐵))) |
84 | 83 | adantr 274 |
. . . 4
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ (♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵))) → ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵)) = (((♯‘𝑦) · (♯‘𝐵)) + (♯‘𝐵))) |
85 | 33, 73, 84 | 3eqtr4d 2213 |
. . 3
⊢
(((((𝐴 ∈ Fin
∧ 𝐵 ∈ Fin) ∧
𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) ∧ (♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵))) → (♯‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵))) |
86 | 85 | ex 114 |
. 2
⊢ ((((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) ∧ 𝑦 ∈ Fin) ∧ (𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ (𝐴 ∖ 𝑦))) → ((♯‘(𝑦 × 𝐵)) = ((♯‘𝑦) · (♯‘𝐵)) → (♯‘((𝑦 ∪ {𝑧}) × 𝐵)) = ((♯‘(𝑦 ∪ {𝑧})) · (♯‘𝐵)))) |
87 | | simpl 108 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → 𝐴 ∈ Fin) |
88 | 5, 10, 15, 20, 31, 86, 87 | findcard2sd 6870 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
(♯‘(𝐴 ×
𝐵)) = ((♯‘𝐴) · (♯‘𝐵))) |