Metamath Proof Explorer

Theorem xpfi

Description: The Cartesian product of two finite sets is finite. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Mar-2015)

Ref Expression
Assertion xpfi ⊢ A ∈ Fin ∧ B ∈ Fin → A × B ∈ Fin

Proof

Step Hyp Ref Expression
1 xpeq1 ⊢ x = ∅ → x × B = ∅ × B
2 1 eleq1d ⊢ x = ∅ → x × B ∈ Fin ↔ ∅ × B ∈ Fin
3 2 imbi2d ⊢ x = ∅ → B ∈ Fin → x × B ∈ Fin ↔ B ∈ Fin → ∅ × B ∈ Fin
4 xpeq1 ⊢ x = y ∖ z → x × B = y ∖ z × B
5 4 eleq1d ⊢ x = y ∖ z → x × B ∈ Fin ↔ y ∖ z × B ∈ Fin
6 5 imbi2d ⊢ x = y ∖ z → B ∈ Fin → x × B ∈ Fin ↔ B ∈ Fin → y ∖ z × B ∈ Fin
7 xpeq1 ⊢ x = y → x × B = y × B
8 7 eleq1d ⊢ x = y → x × B ∈ Fin ↔ y × B ∈ Fin
9 8 imbi2d ⊢ x = y → B ∈ Fin → x × B ∈ Fin ↔ B ∈ Fin → y × B ∈ Fin
10 xpeq1 ⊢ x = A → x × B = A × B
11 10 eleq1d ⊢ x = A → x × B ∈ Fin ↔ A × B ∈ Fin
12 11 imbi2d ⊢ x = A → B ∈ Fin → x × B ∈ Fin ↔ B ∈ Fin → A × B ∈ Fin
13 0xp ⊢ ∅ × B = ∅
14 0fin ⊢ ∅ ∈ Fin
15 13 14 eqeltri ⊢ ∅ × B ∈ Fin
16 15 a1i ⊢ B ∈ Fin → ∅ × B ∈ Fin
17 neq0 ⊢ ¬ y = ∅ ↔ ∃ w w ∈ y
18 sneq ⊢ z = w → z = w
19 18 difeq2d ⊢ z = w → y ∖ z = y ∖ w
20 19 xpeq1d ⊢ z = w → y ∖ z × B = y ∖ w × B
21 20 eleq1d ⊢ z = w → y ∖ z × B ∈ Fin ↔ y ∖ w × B ∈ Fin
22 21 imbi2d ⊢ z = w → B ∈ Fin → y ∖ z × B ∈ Fin ↔ B ∈ Fin → y ∖ w × B ∈ Fin
23 22 rspcv ⊢ w ∈ y → ∀ z ∈ y B ∈ Fin → y ∖ z × B ∈ Fin → B ∈ Fin → y ∖ w × B ∈ Fin
24 23 adantl ⊢ y ∈ Fin ∧ B ∈ Fin ∧ w ∈ y → ∀ z ∈ y B ∈ Fin → y ∖ z × B ∈ Fin → B ∈ Fin → y ∖ w × B ∈ Fin
25 pm2.27 ⊢ B ∈ Fin → B ∈ Fin → y ∖ w × B ∈ Fin → y ∖ w × B ∈ Fin
26 25 ad2antlr ⊢ y ∈ Fin ∧ B ∈ Fin ∧ w ∈ y → B ∈ Fin → y ∖ w × B ∈ Fin → y ∖ w × B ∈ Fin
27 snex ⊢ w ∈ V
28 xpexg ⊢ w ∈ V ∧ B ∈ Fin → w × B ∈ V
29 27 28 mpan ⊢ B ∈ Fin → w × B ∈ V
30 id ⊢ B ∈ Fin → B ∈ Fin
31 vex ⊢ w ∈ V
32 2ndconst ⊢ w ∈ V → 2 nd ↾ w × B : w × B ⟶ 1-1 onto B
33 31 32 mp1i ⊢ B ∈ Fin → 2 nd ↾ w × B : w × B ⟶ 1-1 onto B
34 f1oen2g ⊢ w × B ∈ V ∧ B ∈ Fin ∧ 2 nd ↾ w × B : w × B ⟶ 1-1 onto B → w × B ≈ B
35 29 30 33 34 syl3anc ⊢ B ∈ Fin → w × B ≈ B
36 enfii ⊢ B ∈ Fin ∧ w × B ≈ B → w × B ∈ Fin
37 35 36 mpdan ⊢ B ∈ Fin → w × B ∈ Fin
38 37 ad2antlr ⊢ y ∈ Fin ∧ B ∈ Fin ∧ w ∈ y → w × B ∈ Fin
39 unfi ⊢ y ∖ w × B ∈ Fin ∧ w × B ∈ Fin → y ∖ w × B ∪ w × B ∈ Fin
40 xpundir ⊢ y ∖ w ∪ w × B = y ∖ w × B ∪ w × B
41 difsnid ⊢ w ∈ y → y ∖ w ∪ w = y
42 41 xpeq1d ⊢ w ∈ y → y ∖ w ∪ w × B = y × B
43 40 42 syl5eqr ⊢ w ∈ y → y ∖ w × B ∪ w × B = y × B
44 43 eleq1d ⊢ w ∈ y → y ∖ w × B ∪ w × B ∈ Fin ↔ y × B ∈ Fin
45 44 biimpd ⊢ w ∈ y → y ∖ w × B ∪ w × B ∈ Fin → y × B ∈ Fin
46 45 adantl ⊢ y ∈ Fin ∧ B ∈ Fin ∧ w ∈ y → y ∖ w × B ∪ w × B ∈ Fin → y × B ∈ Fin
47 39 46 syl5 ⊢ y ∈ Fin ∧ B ∈ Fin ∧ w ∈ y → y ∖ w × B ∈ Fin ∧ w × B ∈ Fin → y × B ∈ Fin
48 38 47 mpan2d ⊢ y ∈ Fin ∧ B ∈ Fin ∧ w ∈ y → y ∖ w × B ∈ Fin → y × B ∈ Fin
49 24 26 48 3syld ⊢ y ∈ Fin ∧ B ∈ Fin ∧ w ∈ y → ∀ z ∈ y B ∈ Fin → y ∖ z × B ∈ Fin → y × B ∈ Fin
50 49 ex ⊢ y ∈ Fin ∧ B ∈ Fin → w ∈ y → ∀ z ∈ y B ∈ Fin → y ∖ z × B ∈ Fin → y × B ∈ Fin
51 50 exlimdv ⊢ y ∈ Fin ∧ B ∈ Fin → ∃ w w ∈ y → ∀ z ∈ y B ∈ Fin → y ∖ z × B ∈ Fin → y × B ∈ Fin
52 17 51 syl5bi ⊢ y ∈ Fin ∧ B ∈ Fin → ¬ y = ∅ → ∀ z ∈ y B ∈ Fin → y ∖ z × B ∈ Fin → y × B ∈ Fin
53 xpeq1 ⊢ y = ∅ → y × B = ∅ × B
54 53 15 eqeltrdi ⊢ y = ∅ → y × B ∈ Fin
55 54 a1d ⊢ y = ∅ → ∀ z ∈ y B ∈ Fin → y ∖ z × B ∈ Fin → y × B ∈ Fin
56 52 55 pm2.61d2 ⊢ y ∈ Fin ∧ B ∈ Fin → ∀ z ∈ y B ∈ Fin → y ∖ z × B ∈ Fin → y × B ∈ Fin
57 56 ex ⊢ y ∈ Fin → B ∈ Fin → ∀ z ∈ y B ∈ Fin → y ∖ z × B ∈ Fin → y × B ∈ Fin
58 57 com23 ⊢ y ∈ Fin → ∀ z ∈ y B ∈ Fin → y ∖ z × B ∈ Fin → B ∈ Fin → y × B ∈ Fin
59 3 6 9 12 16 58 findcard ⊢ A ∈ Fin → B ∈ Fin → A × B ∈ Fin
60 59 imp ⊢ A ∈ Fin ∧ B ∈ Fin → A × B ∈ Fin