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 ( 𝜑𝐶 ∈ Fin )
ixpfi2.2 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ Fin )
ixpfi2.3 ( ( 𝜑𝑥 ∈ ( 𝐴𝐶 ) ) → 𝐵 ⊆ { 𝐷 } )
Assertion ixpfi2 ( 𝜑X 𝑥𝐴 𝐵 ∈ Fin )

Proof

Step Hyp Ref Expression
1 ixpfi2.1 ( 𝜑𝐶 ∈ Fin )
2 ixpfi2.2 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ Fin )
3 ixpfi2.3 ( ( 𝜑𝑥 ∈ ( 𝐴𝐶 ) ) → 𝐵 ⊆ { 𝐷 } )
4 inss2 ( 𝐴𝐶 ) ⊆ 𝐶
5 ssfi ( ( 𝐶 ∈ Fin ∧ ( 𝐴𝐶 ) ⊆ 𝐶 ) → ( 𝐴𝐶 ) ∈ Fin )
6 1 4 5 sylancl ( 𝜑 → ( 𝐴𝐶 ) ∈ Fin )
7 inss1 ( 𝐴𝐶 ) ⊆ 𝐴
8 2 ralrimiva ( 𝜑 → ∀ 𝑥𝐴 𝐵 ∈ Fin )
9 ssralv ( ( 𝐴𝐶 ) ⊆ 𝐴 → ( ∀ 𝑥𝐴 𝐵 ∈ Fin → ∀ 𝑥 ∈ ( 𝐴𝐶 ) 𝐵 ∈ Fin ) )
10 7 8 9 mpsyl ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴𝐶 ) 𝐵 ∈ Fin )
11 ixpfi ( ( ( 𝐴𝐶 ) ∈ Fin ∧ ∀ 𝑥 ∈ ( 𝐴𝐶 ) 𝐵 ∈ Fin ) → X 𝑥 ∈ ( 𝐴𝐶 ) 𝐵 ∈ Fin )
12 6 10 11 syl2anc ( 𝜑X 𝑥 ∈ ( 𝐴𝐶 ) 𝐵 ∈ Fin )
13 resixp ( ( ( 𝐴𝐶 ) ⊆ 𝐴𝑓X 𝑥𝐴 𝐵 ) → ( 𝑓 ↾ ( 𝐴𝐶 ) ) ∈ X 𝑥 ∈ ( 𝐴𝐶 ) 𝐵 )
14 7 13 mpan ( 𝑓X 𝑥𝐴 𝐵 → ( 𝑓 ↾ ( 𝐴𝐶 ) ) ∈ X 𝑥 ∈ ( 𝐴𝐶 ) 𝐵 )
15 14 a1i ( 𝜑 → ( 𝑓X 𝑥𝐴 𝐵 → ( 𝑓 ↾ ( 𝐴𝐶 ) ) ∈ X 𝑥 ∈ ( 𝐴𝐶 ) 𝐵 ) )
16 simprl ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → 𝑓X 𝑥𝐴 𝐵 )
17 vex 𝑓 ∈ V
18 17 elixp ( 𝑓X 𝑥𝐴 𝐵 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) )
19 16 18 sylib ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ) )
20 19 simprd ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 )
21 simprr ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → 𝑔X 𝑥𝐴 𝐵 )
22 vex 𝑔 ∈ V
23 22 elixp ( 𝑔X 𝑥𝐴 𝐵 ↔ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ 𝐵 ) )
24 21 23 sylib ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → ( 𝑔 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ 𝐵 ) )
25 24 simprd ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ 𝐵 )
26 r19.26 ( ∀ 𝑥𝐴 ( ( 𝑓𝑥 ) ∈ 𝐵 ∧ ( 𝑔𝑥 ) ∈ 𝐵 ) ↔ ( ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ 𝐵 ) )
27 difss ( 𝐴𝐶 ) ⊆ 𝐴
28 ssralv ( ( 𝐴𝐶 ) ⊆ 𝐴 → ( ∀ 𝑥𝐴 ( ( 𝑓𝑥 ) ∈ 𝐵 ∧ ( 𝑔𝑥 ) ∈ 𝐵 ) → ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( ( 𝑓𝑥 ) ∈ 𝐵 ∧ ( 𝑔𝑥 ) ∈ 𝐵 ) ) )
29 27 28 ax-mp ( ∀ 𝑥𝐴 ( ( 𝑓𝑥 ) ∈ 𝐵 ∧ ( 𝑔𝑥 ) ∈ 𝐵 ) → ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( ( 𝑓𝑥 ) ∈ 𝐵 ∧ ( 𝑔𝑥 ) ∈ 𝐵 ) )
30 3 sseld ( ( 𝜑𝑥 ∈ ( 𝐴𝐶 ) ) → ( ( 𝑓𝑥 ) ∈ 𝐵 → ( 𝑓𝑥 ) ∈ { 𝐷 } ) )
31 elsni ( ( 𝑓𝑥 ) ∈ { 𝐷 } → ( 𝑓𝑥 ) = 𝐷 )
32 30 31 syl6 ( ( 𝜑𝑥 ∈ ( 𝐴𝐶 ) ) → ( ( 𝑓𝑥 ) ∈ 𝐵 → ( 𝑓𝑥 ) = 𝐷 ) )
33 3 sseld ( ( 𝜑𝑥 ∈ ( 𝐴𝐶 ) ) → ( ( 𝑔𝑥 ) ∈ 𝐵 → ( 𝑔𝑥 ) ∈ { 𝐷 } ) )
34 elsni ( ( 𝑔𝑥 ) ∈ { 𝐷 } → ( 𝑔𝑥 ) = 𝐷 )
35 33 34 syl6 ( ( 𝜑𝑥 ∈ ( 𝐴𝐶 ) ) → ( ( 𝑔𝑥 ) ∈ 𝐵 → ( 𝑔𝑥 ) = 𝐷 ) )
36 32 35 anim12d ( ( 𝜑𝑥 ∈ ( 𝐴𝐶 ) ) → ( ( ( 𝑓𝑥 ) ∈ 𝐵 ∧ ( 𝑔𝑥 ) ∈ 𝐵 ) → ( ( 𝑓𝑥 ) = 𝐷 ∧ ( 𝑔𝑥 ) = 𝐷 ) ) )
37 eqtr3 ( ( ( 𝑓𝑥 ) = 𝐷 ∧ ( 𝑔𝑥 ) = 𝐷 ) → ( 𝑓𝑥 ) = ( 𝑔𝑥 ) )
38 36 37 syl6 ( ( 𝜑𝑥 ∈ ( 𝐴𝐶 ) ) → ( ( ( 𝑓𝑥 ) ∈ 𝐵 ∧ ( 𝑔𝑥 ) ∈ 𝐵 ) → ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ) )
39 38 ralimdva ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( ( 𝑓𝑥 ) ∈ 𝐵 ∧ ( 𝑔𝑥 ) ∈ 𝐵 ) → ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ) )
40 39 adantr ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → ( ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( ( 𝑓𝑥 ) ∈ 𝐵 ∧ ( 𝑔𝑥 ) ∈ 𝐵 ) → ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ) )
41 29 40 syl5 ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → ( ∀ 𝑥𝐴 ( ( 𝑓𝑥 ) ∈ 𝐵 ∧ ( 𝑔𝑥 ) ∈ 𝐵 ) → ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ) )
42 26 41 syl5bir ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → ( ( ∀ 𝑥𝐴 ( 𝑓𝑥 ) ∈ 𝐵 ∧ ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ 𝐵 ) → ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ) )
43 20 25 42 mp2and ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( 𝑓𝑥 ) = ( 𝑔𝑥 ) )
44 43 biantrud ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → ( ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ↔ ( ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ∧ ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ) ) )
45 fvres ( 𝑥 ∈ ( 𝐴𝐶 ) → ( ( 𝑓 ↾ ( 𝐴𝐶 ) ) ‘ 𝑥 ) = ( 𝑓𝑥 ) )
46 fvres ( 𝑥 ∈ ( 𝐴𝐶 ) → ( ( 𝑔 ↾ ( 𝐴𝐶 ) ) ‘ 𝑥 ) = ( 𝑔𝑥 ) )
47 45 46 eqeq12d ( 𝑥 ∈ ( 𝐴𝐶 ) → ( ( ( 𝑓 ↾ ( 𝐴𝐶 ) ) ‘ 𝑥 ) = ( ( 𝑔 ↾ ( 𝐴𝐶 ) ) ‘ 𝑥 ) ↔ ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ) )
48 47 ralbiia ( ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( ( 𝑓 ↾ ( 𝐴𝐶 ) ) ‘ 𝑥 ) = ( ( 𝑔 ↾ ( 𝐴𝐶 ) ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( 𝑓𝑥 ) = ( 𝑔𝑥 ) )
49 inundif ( ( 𝐴𝐶 ) ∪ ( 𝐴𝐶 ) ) = 𝐴
50 49 raleqi ( ∀ 𝑥 ∈ ( ( 𝐴𝐶 ) ∪ ( 𝐴𝐶 ) ) ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ↔ ∀ 𝑥𝐴 ( 𝑓𝑥 ) = ( 𝑔𝑥 ) )
51 ralunb ( ∀ 𝑥 ∈ ( ( 𝐴𝐶 ) ∪ ( 𝐴𝐶 ) ) ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ↔ ( ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ∧ ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ) )
52 50 51 bitr3i ( ∀ 𝑥𝐴 ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ↔ ( ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ∧ ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ) )
53 44 48 52 3bitr4g ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → ( ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( ( 𝑓 ↾ ( 𝐴𝐶 ) ) ‘ 𝑥 ) = ( ( 𝑔 ↾ ( 𝐴𝐶 ) ) ‘ 𝑥 ) ↔ ∀ 𝑥𝐴 ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ) )
54 19 simpld ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → 𝑓 Fn 𝐴 )
55 fnssres ( ( 𝑓 Fn 𝐴 ∧ ( 𝐴𝐶 ) ⊆ 𝐴 ) → ( 𝑓 ↾ ( 𝐴𝐶 ) ) Fn ( 𝐴𝐶 ) )
56 54 7 55 sylancl ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → ( 𝑓 ↾ ( 𝐴𝐶 ) ) Fn ( 𝐴𝐶 ) )
57 24 simpld ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → 𝑔 Fn 𝐴 )
58 fnssres ( ( 𝑔 Fn 𝐴 ∧ ( 𝐴𝐶 ) ⊆ 𝐴 ) → ( 𝑔 ↾ ( 𝐴𝐶 ) ) Fn ( 𝐴𝐶 ) )
59 57 7 58 sylancl ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → ( 𝑔 ↾ ( 𝐴𝐶 ) ) Fn ( 𝐴𝐶 ) )
60 eqfnfv ( ( ( 𝑓 ↾ ( 𝐴𝐶 ) ) Fn ( 𝐴𝐶 ) ∧ ( 𝑔 ↾ ( 𝐴𝐶 ) ) Fn ( 𝐴𝐶 ) ) → ( ( 𝑓 ↾ ( 𝐴𝐶 ) ) = ( 𝑔 ↾ ( 𝐴𝐶 ) ) ↔ ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( ( 𝑓 ↾ ( 𝐴𝐶 ) ) ‘ 𝑥 ) = ( ( 𝑔 ↾ ( 𝐴𝐶 ) ) ‘ 𝑥 ) ) )
61 56 59 60 syl2anc ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → ( ( 𝑓 ↾ ( 𝐴𝐶 ) ) = ( 𝑔 ↾ ( 𝐴𝐶 ) ) ↔ ∀ 𝑥 ∈ ( 𝐴𝐶 ) ( ( 𝑓 ↾ ( 𝐴𝐶 ) ) ‘ 𝑥 ) = ( ( 𝑔 ↾ ( 𝐴𝐶 ) ) ‘ 𝑥 ) ) )
62 eqfnfv ( ( 𝑓 Fn 𝐴𝑔 Fn 𝐴 ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑥𝐴 ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ) )
63 54 57 62 syl2anc ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑥𝐴 ( 𝑓𝑥 ) = ( 𝑔𝑥 ) ) )
64 53 61 63 3bitr4d ( ( 𝜑 ∧ ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) ) → ( ( 𝑓 ↾ ( 𝐴𝐶 ) ) = ( 𝑔 ↾ ( 𝐴𝐶 ) ) ↔ 𝑓 = 𝑔 ) )
65 64 ex ( 𝜑 → ( ( 𝑓X 𝑥𝐴 𝐵𝑔X 𝑥𝐴 𝐵 ) → ( ( 𝑓 ↾ ( 𝐴𝐶 ) ) = ( 𝑔 ↾ ( 𝐴𝐶 ) ) ↔ 𝑓 = 𝑔 ) ) )
66 15 65 dom2lem ( 𝜑 → ( 𝑓X 𝑥𝐴 𝐵 ↦ ( 𝑓 ↾ ( 𝐴𝐶 ) ) ) : X 𝑥𝐴 𝐵1-1X 𝑥 ∈ ( 𝐴𝐶 ) 𝐵 )
67 f1fi ( ( X 𝑥 ∈ ( 𝐴𝐶 ) 𝐵 ∈ Fin ∧ ( 𝑓X 𝑥𝐴 𝐵 ↦ ( 𝑓 ↾ ( 𝐴𝐶 ) ) ) : X 𝑥𝐴 𝐵1-1X 𝑥 ∈ ( 𝐴𝐶 ) 𝐵 ) → X 𝑥𝐴 𝐵 ∈ Fin )
68 12 66 67 syl2anc ( 𝜑X 𝑥𝐴 𝐵 ∈ Fin )