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 syl6eqel 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