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 eqtr3id
 |-  ( 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 )