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 ⊢φ→C∈Fin
ixpfi2.2 ⊢φ∧x∈A→B∈Fin
ixpfi2.3 ⊢φ∧x∈A∖C→B⊆D
Assertion ixpfi2 ⊢φ→⨉x∈AB∈Fin

Proof

Step Hyp Ref Expression
1 ixpfi2.1 ⊢φ→C∈Fin
2 ixpfi2.2 ⊢φ∧x∈A→B∈Fin
3 ixpfi2.3 ⊢φ∧x∈A∖C→B⊆D
4 inss2 ⊢A∩C⊆C
5 ssfi ⊢C∈Fin∧A∩C⊆C→A∩C∈Fin
6 1 4 5 sylancl ⊢φ→A∩C∈Fin
7 inss1 ⊢A∩C⊆A
8 2 ralrimiva ⊢φ→∀x∈AB∈Fin
9 ssralv ⊢A∩C⊆A→∀x∈AB∈Fin→∀x∈A∩CB∈Fin
10 7 8 9 mpsyl ⊢φ→∀x∈A∩CB∈Fin
11 ixpfi ⊢A∩C∈Fin∧∀x∈A∩CB∈Fin→⨉x∈A∩CB∈Fin
12 6 10 11 syl2anc ⊢φ→⨉x∈A∩CB∈Fin
13 resixp ⊢A∩C⊆A∧f∈⨉x∈AB→f↾A∩C∈⨉x∈A∩CB
14 7 13 mpan ⊢f∈⨉x∈AB→f↾A∩C∈⨉x∈A∩CB
15 14 a1i ⊢φ→f∈⨉x∈AB→f↾A∩C∈⨉x∈A∩CB
16 simprl ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→f∈⨉x∈AB
17 vex ⊢f∈V
18 17 elixp ⊢f∈⨉x∈AB↔fFnA∧∀x∈Af⁡x∈B
19 16 18 sylib ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→fFnA∧∀x∈Af⁡x∈B
20 19 simprd ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→∀x∈Af⁡x∈B
21 simprr ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→g∈⨉x∈AB
22 vex ⊢g∈V
23 22 elixp ⊢g∈⨉x∈AB↔gFnA∧∀x∈Ag⁡x∈B
24 21 23 sylib ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→gFnA∧∀x∈Ag⁡x∈B
25 24 simprd ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→∀x∈Ag⁡x∈B
26 r19.26 ⊢∀x∈Af⁡x∈B∧g⁡x∈B↔∀x∈Af⁡x∈B∧∀x∈Ag⁡x∈B
27 difss ⊢A∖C⊆A
28 ssralv ⊢A∖C⊆A→∀x∈Af⁡x∈B∧g⁡x∈B→∀x∈A∖Cf⁡x∈B∧g⁡x∈B
29 27 28 ax-mp ⊢∀x∈Af⁡x∈B∧g⁡x∈B→∀x∈A∖Cf⁡x∈B∧g⁡x∈B
30 3 sseld ⊢φ∧x∈A∖C→f⁡x∈B→f⁡x∈D
31 elsni ⊢f⁡x∈D→f⁡x=D
32 30 31 syl6 ⊢φ∧x∈A∖C→f⁡x∈B→f⁡x=D
33 3 sseld ⊢φ∧x∈A∖C→g⁡x∈B→g⁡x∈D
34 elsni ⊢g⁡x∈D→g⁡x=D
35 33 34 syl6 ⊢φ∧x∈A∖C→g⁡x∈B→g⁡x=D
36 32 35 anim12d ⊢φ∧x∈A∖C→f⁡x∈B∧g⁡x∈B→f⁡x=D∧g⁡x=D
37 eqtr3 ⊢f⁡x=D∧g⁡x=D→f⁡x=g⁡x
38 36 37 syl6 ⊢φ∧x∈A∖C→f⁡x∈B∧g⁡x∈B→f⁡x=g⁡x
39 38 ralimdva ⊢φ→∀x∈A∖Cf⁡x∈B∧g⁡x∈B→∀x∈A∖Cf⁡x=g⁡x
40 39 adantr ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→∀x∈A∖Cf⁡x∈B∧g⁡x∈B→∀x∈A∖Cf⁡x=g⁡x
41 29 40 syl5 ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→∀x∈Af⁡x∈B∧g⁡x∈B→∀x∈A∖Cf⁡x=g⁡x
42 26 41 biimtrrid ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→∀x∈Af⁡x∈B∧∀x∈Ag⁡x∈B→∀x∈A∖Cf⁡x=g⁡x
43 20 25 42 mp2and ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→∀x∈A∖Cf⁡x=g⁡x
44 43 biantrud ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→∀x∈A∩Cf⁡x=g⁡x↔∀x∈A∩Cf⁡x=g⁡x∧∀x∈A∖Cf⁡x=g⁡x
45 fvres ⊢x∈A∩C→f↾A∩C⁡x=f⁡x
46 fvres ⊢x∈A∩C→g↾A∩C⁡x=g⁡x
47 45 46 eqeq12d ⊢x∈A∩C→f↾A∩C⁡x=g↾A∩C⁡x↔f⁡x=g⁡x
48 47 ralbiia ⊢∀x∈A∩Cf↾A∩C⁡x=g↾A∩C⁡x↔∀x∈A∩Cf⁡x=g⁡x
49 inundif ⊢A∩C∪A∖C=A
50 49 raleqi ⊢∀x∈A∩C∪A∖Cf⁡x=g⁡x↔∀x∈Af⁡x=g⁡x
51 ralunb ⊢∀x∈A∩C∪A∖Cf⁡x=g⁡x↔∀x∈A∩Cf⁡x=g⁡x∧∀x∈A∖Cf⁡x=g⁡x
52 50 51 bitr3i ⊢∀x∈Af⁡x=g⁡x↔∀x∈A∩Cf⁡x=g⁡x∧∀x∈A∖Cf⁡x=g⁡x
53 44 48 52 3bitr4g ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→∀x∈A∩Cf↾A∩C⁡x=g↾A∩C⁡x↔∀x∈Af⁡x=g⁡x
54 19 simpld ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→fFnA
55 fnssres ⊢fFnA∧A∩C⊆A→f↾A∩CFnA∩C
56 54 7 55 sylancl ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→f↾A∩CFnA∩C
57 24 simpld ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→gFnA
58 fnssres ⊢gFnA∧A∩C⊆A→g↾A∩CFnA∩C
59 57 7 58 sylancl ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→g↾A∩CFnA∩C
60 eqfnfv ⊢f↾A∩CFnA∩C∧g↾A∩CFnA∩C→f↾A∩C=g↾A∩C↔∀x∈A∩Cf↾A∩C⁡x=g↾A∩C⁡x
61 56 59 60 syl2anc ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→f↾A∩C=g↾A∩C↔∀x∈A∩Cf↾A∩C⁡x=g↾A∩C⁡x
62 eqfnfv ⊢fFnA∧gFnA→f=g↔∀x∈Af⁡x=g⁡x
63 54 57 62 syl2anc ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→f=g↔∀x∈Af⁡x=g⁡x
64 53 61 63 3bitr4d ⊢φ∧f∈⨉x∈AB∧g∈⨉x∈AB→f↾A∩C=g↾A∩C↔f=g
65 64 ex ⊢φ→f∈⨉x∈AB∧g∈⨉x∈AB→f↾A∩C=g↾A∩C↔f=g
66 15 65 dom2lem ⊢φ→f∈⨉x∈AB⟼f↾A∩C:⨉x∈AB⟶1-1⨉x∈A∩CB
67 f1fi ⊢⨉x∈A∩CB∈Fin∧f∈⨉x∈AB⟼f↾A∩C:⨉x∈AB⟶1-1⨉x∈A∩CB→⨉x∈AB∈Fin
68 12 66 67 syl2anc ⊢φ→⨉x∈AB∈Fin