Metamath Proof Explorer

Theorem ixpfi2

Description: A Cartesian product of finite sets such that all but finitely many are singletons is finite. (Note that B ( x ) and D ( x ) are both possibly dependent on x .) (Contributed by Mario Carneiro, 25-Jan-2015)

Ref Expression
Hypotheses ixpfi2.1 
|- ( ph -> C e. Fin )
ixpfi2.2 
|- ( ( ph /\ x e. A ) -> B e. Fin )
ixpfi2.3 
|- ( ( ph /\ x e. ( A \ C ) ) -> B C_ { D } )
Assertion ixpfi2 
|- ( ph -> X_ x e. A B e. Fin )

Proof

Step Hyp Ref Expression
1 ixpfi2.1 
 |-  ( ph -> C e. Fin )
2 ixpfi2.2 
 |-  ( ( ph /\ x e. A ) -> B e. Fin )
3 ixpfi2.3 
 |-  ( ( ph /\ x e. ( A \ C ) ) -> B C_ { D } )
4 inss2 
 |-  ( A i^i C ) C_ C
5 ssfi 
 |-  ( ( C e. Fin /\ ( A i^i C ) C_ C ) -> ( A i^i C ) e. Fin )
6 1 4 5 sylancl 
 |-  ( ph -> ( A i^i C ) e. Fin )
7 inss1 
 |-  ( A i^i C ) C_ A
8 2 ralrimiva 
 |-  ( ph -> A. x e. A B e. Fin )
9 ssralv 
 |-  ( ( A i^i C ) C_ A -> ( A. x e. A B e. Fin -> A. x e. ( A i^i C ) B e. Fin ) )
10 7 8 9 mpsyl 
 |-  ( ph -> A. x e. ( A i^i C ) B e. Fin )
11 ixpfi 
 |-  ( ( ( A i^i C ) e. Fin /\ A. x e. ( A i^i C ) B e. Fin ) -> X_ x e. ( A i^i C ) B e. Fin )
12 6 10 11 syl2anc 
 |-  ( ph -> X_ x e. ( A i^i C ) B e. Fin )
13 resixp 
 |-  ( ( ( A i^i C ) C_ A /\ f e. X_ x e. A B ) -> ( f |` ( A i^i C ) ) e. X_ x e. ( A i^i C ) B )
14 7 13 mpan 
 |-  ( f e. X_ x e. A B -> ( f |` ( A i^i C ) ) e. X_ x e. ( A i^i C ) B )
15 14 a1i 
 |-  ( ph -> ( f e. X_ x e. A B -> ( f |` ( A i^i C ) ) e. X_ x e. ( A i^i C ) B ) )
16 simprl 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> f e. X_ x e. A B )
17 vex 
 |-  f e. _V
18 17 elixp 
 |-  ( f e. X_ x e. A B <-> ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )
19 16 18 sylib 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )
20 19 simprd 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> A. x e. A ( f ` x ) e. B )
21 simprr 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> g e. X_ x e. A B )
22 vex 
 |-  g e. _V
23 22 elixp 
 |-  ( g e. X_ x e. A B <-> ( g Fn A /\ A. x e. A ( g ` x ) e. B ) )
24 21 23 sylib 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> ( g Fn A /\ A. x e. A ( g ` x ) e. B ) )
25 24 simprd 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> A. x e. A ( g ` x ) e. B )
26 r19.26 
 |-  ( A. x e. A ( ( f ` x ) e. B /\ ( g ` x ) e. B ) <-> ( A. x e. A ( f ` x ) e. B /\ A. x e. A ( g ` x ) e. B ) )
27 difss 
 |-  ( A \ C ) C_ A
28 ssralv 
 |-  ( ( A \ C ) C_ A -> ( A. x e. A ( ( f ` x ) e. B /\ ( g ` x ) e. B ) -> A. x e. ( A \ C ) ( ( f ` x ) e. B /\ ( g ` x ) e. B ) ) )
29 27 28 ax-mp 
 |-  ( A. x e. A ( ( f ` x ) e. B /\ ( g ` x ) e. B ) -> A. x e. ( A \ C ) ( ( f ` x ) e. B /\ ( g ` x ) e. B ) )
30 3 sseld 
 |-  ( ( ph /\ x e. ( A \ C ) ) -> ( ( f ` x ) e. B -> ( f ` x ) e. { D } ) )
31 elsni 
 |-  ( ( f ` x ) e. { D } -> ( f ` x ) = D )
32 30 31 syl6 
 |-  ( ( ph /\ x e. ( A \ C ) ) -> ( ( f ` x ) e. B -> ( f ` x ) = D ) )
33 3 sseld 
 |-  ( ( ph /\ x e. ( A \ C ) ) -> ( ( g ` x ) e. B -> ( g ` x ) e. { D } ) )
34 elsni 
 |-  ( ( g ` x ) e. { D } -> ( g ` x ) = D )
35 33 34 syl6 
 |-  ( ( ph /\ x e. ( A \ C ) ) -> ( ( g ` x ) e. B -> ( g ` x ) = D ) )
36 32 35 anim12d 
 |-  ( ( ph /\ x e. ( A \ C ) ) -> ( ( ( f ` x ) e. B /\ ( g ` x ) e. B ) -> ( ( f ` x ) = D /\ ( g ` x ) = D ) ) )
37 eqtr3 
 |-  ( ( ( f ` x ) = D /\ ( g ` x ) = D ) -> ( f ` x ) = ( g ` x ) )
38 36 37 syl6 
 |-  ( ( ph /\ x e. ( A \ C ) ) -> ( ( ( f ` x ) e. B /\ ( g ` x ) e. B ) -> ( f ` x ) = ( g ` x ) ) )
39 38 ralimdva 
 |-  ( ph -> ( A. x e. ( A \ C ) ( ( f ` x ) e. B /\ ( g ` x ) e. B ) -> A. x e. ( A \ C ) ( f ` x ) = ( g ` x ) ) )
40 39 adantr 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> ( A. x e. ( A \ C ) ( ( f ` x ) e. B /\ ( g ` x ) e. B ) -> A. x e. ( A \ C ) ( f ` x ) = ( g ` x ) ) )
41 29 40 syl5 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> ( A. x e. A ( ( f ` x ) e. B /\ ( g ` x ) e. B ) -> A. x e. ( A \ C ) ( f ` x ) = ( g ` x ) ) )
42 26 41 syl5bir 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> ( ( A. x e. A ( f ` x ) e. B /\ A. x e. A ( g ` x ) e. B ) -> A. x e. ( A \ C ) ( f ` x ) = ( g ` x ) ) )
43 20 25 42 mp2and 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> A. x e. ( A \ C ) ( f ` x ) = ( g ` x ) )
44 43 biantrud 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> ( A. x e. ( A i^i C ) ( f ` x ) = ( g ` x ) <-> ( A. x e. ( A i^i C ) ( f ` x ) = ( g ` x ) /\ A. x e. ( A \ C ) ( f ` x ) = ( g ` x ) ) ) )
45 fvres 
 |-  ( x e. ( A i^i C ) -> ( ( f |` ( A i^i C ) ) ` x ) = ( f ` x ) )
46 fvres 
 |-  ( x e. ( A i^i C ) -> ( ( g |` ( A i^i C ) ) ` x ) = ( g ` x ) )
47 45 46 eqeq12d 
 |-  ( x e. ( A i^i C ) -> ( ( ( f |` ( A i^i C ) ) ` x ) = ( ( g |` ( A i^i C ) ) ` x ) <-> ( f ` x ) = ( g ` x ) ) )
48 47 ralbiia 
 |-  ( A. x e. ( A i^i C ) ( ( f |` ( A i^i C ) ) ` x ) = ( ( g |` ( A i^i C ) ) ` x ) <-> A. x e. ( A i^i C ) ( f ` x ) = ( g ` x ) )
49 inundif 
 |-  ( ( A i^i C ) u. ( A \ C ) ) = A
50 49 raleqi 
 |-  ( A. x e. ( ( A i^i C ) u. ( A \ C ) ) ( f ` x ) = ( g ` x ) <-> A. x e. A ( f ` x ) = ( g ` x ) )
51 ralunb 
 |-  ( A. x e. ( ( A i^i C ) u. ( A \ C ) ) ( f ` x ) = ( g ` x ) <-> ( A. x e. ( A i^i C ) ( f ` x ) = ( g ` x ) /\ A. x e. ( A \ C ) ( f ` x ) = ( g ` x ) ) )
52 50 51 bitr3i 
 |-  ( A. x e. A ( f ` x ) = ( g ` x ) <-> ( A. x e. ( A i^i C ) ( f ` x ) = ( g ` x ) /\ A. x e. ( A \ C ) ( f ` x ) = ( g ` x ) ) )
53 44 48 52 3bitr4g 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> ( A. x e. ( A i^i C ) ( ( f |` ( A i^i C ) ) ` x ) = ( ( g |` ( A i^i C ) ) ` x ) <-> A. x e. A ( f ` x ) = ( g ` x ) ) )
54 19 simpld 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> f Fn A )
55 fnssres 
 |-  ( ( f Fn A /\ ( A i^i C ) C_ A ) -> ( f |` ( A i^i C ) ) Fn ( A i^i C ) )
56 54 7 55 sylancl 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> ( f |` ( A i^i C ) ) Fn ( A i^i C ) )
57 24 simpld 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> g Fn A )
58 fnssres 
 |-  ( ( g Fn A /\ ( A i^i C ) C_ A ) -> ( g |` ( A i^i C ) ) Fn ( A i^i C ) )
59 57 7 58 sylancl 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> ( g |` ( A i^i C ) ) Fn ( A i^i C ) )
60 eqfnfv 
 |-  ( ( ( f |` ( A i^i C ) ) Fn ( A i^i C ) /\ ( g |` ( A i^i C ) ) Fn ( A i^i C ) ) -> ( ( f |` ( A i^i C ) ) = ( g |` ( A i^i C ) ) <-> A. x e. ( A i^i C ) ( ( f |` ( A i^i C ) ) ` x ) = ( ( g |` ( A i^i C ) ) ` x ) ) )
61 56 59 60 syl2anc 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> ( ( f |` ( A i^i C ) ) = ( g |` ( A i^i C ) ) <-> A. x e. ( A i^i C ) ( ( f |` ( A i^i C ) ) ` x ) = ( ( g |` ( A i^i C ) ) ` x ) ) )
62 eqfnfv 
 |-  ( ( f Fn A /\ g Fn A ) -> ( f = g <-> A. x e. A ( f ` x ) = ( g ` x ) ) )
63 54 57 62 syl2anc 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> ( f = g <-> A. x e. A ( f ` x ) = ( g ` x ) ) )
64 53 61 63 3bitr4d 
 |-  ( ( ph /\ ( f e. X_ x e. A B /\ g e. X_ x e. A B ) ) -> ( ( f |` ( A i^i C ) ) = ( g |` ( A i^i C ) ) <-> f = g ) )
65 64 ex 
 |-  ( ph -> ( ( f e. X_ x e. A B /\ g e. X_ x e. A B ) -> ( ( f |` ( A i^i C ) ) = ( g |` ( A i^i C ) ) <-> f = g ) ) )
66 15 65 dom2lem 
 |-  ( ph -> ( f e. X_ x e. A B |-> ( f |` ( A i^i C ) ) ) : X_ x e. A B -1-1-> X_ x e. ( A i^i C ) B )
67 f1fi 
 |-  ( ( X_ x e. ( A i^i C ) B e. Fin /\ ( f e. X_ x e. A B |-> ( f |` ( A i^i C ) ) ) : X_ x e. A B -1-1-> X_ x e. ( A i^i C ) B ) -> X_ x e. A B e. Fin )
68 12 66 67 syl2anc 
 |-  ( ph -> X_ x e. A B e. Fin )