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 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 × 𝐵 ) ∈ Fin )

Proof

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