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 )