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 e. Fin /\ B e. Fin ) -> ( A X. B ) e. Fin )

Proof

Step Hyp Ref Expression
1 xpeq1 
 |-  ( x = (/) -> ( x X. B ) = ( (/) X. B ) )
2 1 eleq1d 
 |-  ( x = (/) -> ( ( x X. B ) e. Fin <-> ( (/) X. B ) e. Fin ) )
3 2 imbi2d 
 |-  ( x = (/) -> ( ( B e. Fin -> ( x X. B ) e. Fin ) <-> ( B e. Fin -> ( (/) X. B ) e. Fin ) ) )
4 xpeq1 
 |-  ( x = ( y \ { z } ) -> ( x X. B ) = ( ( y \ { z } ) X. B ) )
5 4 eleq1d 
 |-  ( x = ( y \ { z } ) -> ( ( x X. B ) e. Fin <-> ( ( y \ { z } ) X. B ) e. Fin ) )
6 5 imbi2d 
 |-  ( x = ( y \ { z } ) -> ( ( B e. Fin -> ( x X. B ) e. Fin ) <-> ( B e. Fin -> ( ( y \ { z } ) X. B ) e. Fin ) ) )
7 xpeq1 
 |-  ( x = y -> ( x X. B ) = ( y X. B ) )
8 7 eleq1d 
 |-  ( x = y -> ( ( x X. B ) e. Fin <-> ( y X. B ) e. Fin ) )
9 8 imbi2d 
 |-  ( x = y -> ( ( B e. Fin -> ( x X. B ) e. Fin ) <-> ( B e. Fin -> ( y X. B ) e. Fin ) ) )
10 xpeq1 
 |-  ( x = A -> ( x X. B ) = ( A X. B ) )
11 10 eleq1d 
 |-  ( x = A -> ( ( x X. B ) e. Fin <-> ( A X. B ) e. Fin ) )
12 11 imbi2d 
 |-  ( x = A -> ( ( B e. Fin -> ( x X. B ) e. Fin ) <-> ( B e. Fin -> ( A X. B ) e. Fin ) ) )
13 0xp 
 |-  ( (/) X. B ) = (/)
14 0fin 
 |-  (/) e. Fin
15 13 14 eqeltri 
 |-  ( (/) X. B ) e. Fin
16 15 a1i 
 |-  ( B e. Fin -> ( (/) X. B ) e. Fin )
17 neq0 
 |-  ( -. y = (/) <-> E. w w e. y )
18 sneq 
 |-  ( z = w -> { z } = { w } )
19 18 difeq2d 
 |-  ( z = w -> ( y \ { z } ) = ( y \ { w } ) )
20 19 xpeq1d 
 |-  ( z = w -> ( ( y \ { z } ) X. B ) = ( ( y \ { w } ) X. B ) )
21 20 eleq1d 
 |-  ( z = w -> ( ( ( y \ { z } ) X. B ) e. Fin <-> ( ( y \ { w } ) X. B ) e. Fin ) )
22 21 imbi2d 
 |-  ( z = w -> ( ( B e. Fin -> ( ( y \ { z } ) X. B ) e. Fin ) <-> ( B e. Fin -> ( ( y \ { w } ) X. B ) e. Fin ) ) )
23 22 rspcv 
 |-  ( w e. y -> ( A. z e. y ( B e. Fin -> ( ( y \ { z } ) X. B ) e. Fin ) -> ( B e. Fin -> ( ( y \ { w } ) X. B ) e. Fin ) ) )
24 23 adantl 
 |-  ( ( ( y e. Fin /\ B e. Fin ) /\ w e. y ) -> ( A. z e. y ( B e. Fin -> ( ( y \ { z } ) X. B ) e. Fin ) -> ( B e. Fin -> ( ( y \ { w } ) X. B ) e. Fin ) ) )
25 pm2.27 
 |-  ( B e. Fin -> ( ( B e. Fin -> ( ( y \ { w } ) X. B ) e. Fin ) -> ( ( y \ { w } ) X. B ) e. Fin ) )
26 25 ad2antlr 
 |-  ( ( ( y e. Fin /\ B e. Fin ) /\ w e. y ) -> ( ( B e. Fin -> ( ( y \ { w } ) X. B ) e. Fin ) -> ( ( y \ { w } ) X. B ) e. Fin ) )
27 snex 
 |-  { w } e. _V
28 xpexg 
 |-  ( ( { w } e. _V /\ B e. Fin ) -> ( { w } X. B ) e. _V )
29 27 28 mpan 
 |-  ( B e. Fin -> ( { w } X. B ) e. _V )
30 id 
 |-  ( B e. Fin -> B e. Fin )
31 vex 
 |-  w e. _V
32 2ndconst 
 |-  ( w e. _V -> ( 2nd |` ( { w } X. B ) ) : ( { w } X. B ) -1-1-onto-> B )
33 31 32 mp1i 
 |-  ( B e. Fin -> ( 2nd |` ( { w } X. B ) ) : ( { w } X. B ) -1-1-onto-> B )
34 f1oen2g 
 |-  ( ( ( { w } X. B ) e. _V /\ B e. Fin /\ ( 2nd |` ( { w } X. B ) ) : ( { w } X. B ) -1-1-onto-> B ) -> ( { w } X. B ) ~~ B )
35 29 30 33 34 syl3anc 
 |-  ( B e. Fin -> ( { w } X. B ) ~~ B )
36 enfii 
 |-  ( ( B e. Fin /\ ( { w } X. B ) ~~ B ) -> ( { w } X. B ) e. Fin )
37 35 36 mpdan 
 |-  ( B e. Fin -> ( { w } X. B ) e. Fin )
38 37 ad2antlr 
 |-  ( ( ( y e. Fin /\ B e. Fin ) /\ w e. y ) -> ( { w } X. B ) e. Fin )
39 unfi 
 |-  ( ( ( ( y \ { w } ) X. B ) e. Fin /\ ( { w } X. B ) e. Fin ) -> ( ( ( y \ { w } ) X. B ) u. ( { w } X. B ) ) e. Fin )
40 xpundir 
 |-  ( ( ( y \ { w } ) u. { w } ) X. B ) = ( ( ( y \ { w } ) X. B ) u. ( { w } X. B ) )
41 difsnid 
 |-  ( w e. y -> ( ( y \ { w } ) u. { w } ) = y )
42 41 xpeq1d 
 |-  ( w e. y -> ( ( ( y \ { w } ) u. { w } ) X. B ) = ( y X. B ) )
43 40 42 syl5eqr 
 |-  ( w e. y -> ( ( ( y \ { w } ) X. B ) u. ( { w } X. B ) ) = ( y X. B ) )
44 43 eleq1d 
 |-  ( w e. y -> ( ( ( ( y \ { w } ) X. B ) u. ( { w } X. B ) ) e. Fin <-> ( y X. B ) e. Fin ) )
45 44 biimpd 
 |-  ( w e. y -> ( ( ( ( y \ { w } ) X. B ) u. ( { w } X. B ) ) e. Fin -> ( y X. B ) e. Fin ) )
46 45 adantl 
 |-  ( ( ( y e. Fin /\ B e. Fin ) /\ w e. y ) -> ( ( ( ( y \ { w } ) X. B ) u. ( { w } X. B ) ) e. Fin -> ( y X. B ) e. Fin ) )
47 39 46 syl5 
 |-  ( ( ( y e. Fin /\ B e. Fin ) /\ w e. y ) -> ( ( ( ( y \ { w } ) X. B ) e. Fin /\ ( { w } X. B ) e. Fin ) -> ( y X. B ) e. Fin ) )
48 38 47 mpan2d 
 |-  ( ( ( y e. Fin /\ B e. Fin ) /\ w e. y ) -> ( ( ( y \ { w } ) X. B ) e. Fin -> ( y X. B ) e. Fin ) )
49 24 26 48 3syld 
 |-  ( ( ( y e. Fin /\ B e. Fin ) /\ w e. y ) -> ( A. z e. y ( B e. Fin -> ( ( y \ { z } ) X. B ) e. Fin ) -> ( y X. B ) e. Fin ) )
50 49 ex 
 |-  ( ( y e. Fin /\ B e. Fin ) -> ( w e. y -> ( A. z e. y ( B e. Fin -> ( ( y \ { z } ) X. B ) e. Fin ) -> ( y X. B ) e. Fin ) ) )
51 50 exlimdv 
 |-  ( ( y e. Fin /\ B e. Fin ) -> ( E. w w e. y -> ( A. z e. y ( B e. Fin -> ( ( y \ { z } ) X. B ) e. Fin ) -> ( y X. B ) e. Fin ) ) )
52 17 51 syl5bi 
 |-  ( ( y e. Fin /\ B e. Fin ) -> ( -. y = (/) -> ( A. z e. y ( B e. Fin -> ( ( y \ { z } ) X. B ) e. Fin ) -> ( y X. B ) e. Fin ) ) )
53 xpeq1 
 |-  ( y = (/) -> ( y X. B ) = ( (/) X. B ) )
54 53 15 eqeltrdi 
 |-  ( y = (/) -> ( y X. B ) e. Fin )
55 54 a1d 
 |-  ( y = (/) -> ( A. z e. y ( B e. Fin -> ( ( y \ { z } ) X. B ) e. Fin ) -> ( y X. B ) e. Fin ) )
56 52 55 pm2.61d2 
 |-  ( ( y e. Fin /\ B e. Fin ) -> ( A. z e. y ( B e. Fin -> ( ( y \ { z } ) X. B ) e. Fin ) -> ( y X. B ) e. Fin ) )
57 56 ex 
 |-  ( y e. Fin -> ( B e. Fin -> ( A. z e. y ( B e. Fin -> ( ( y \ { z } ) X. B ) e. Fin ) -> ( y X. B ) e. Fin ) ) )
58 57 com23 
 |-  ( y e. Fin -> ( A. z e. y ( B e. Fin -> ( ( y \ { z } ) X. B ) e. Fin ) -> ( B e. Fin -> ( y X. B ) e. Fin ) ) )
59 3 6 9 12 16 58 findcard 
 |-  ( A e. Fin -> ( B e. Fin -> ( A X. B ) e. Fin ) )
60 59 imp 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A X. B ) e. Fin )