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 biimtrrid ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 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-1→ X 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) 𝐵 )
67 f1fi ⊢ ( ( X 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) 𝐵 ∈ Fin ∧ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ↦ ( 𝑓 ↾ ( 𝐴 ∩ 𝐶 ) ) ) : X 𝑥 ∈ 𝐴 𝐵 –1-1→ X 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) 𝐵 ) → X 𝑥 ∈ 𝐴 𝐵 ∈ Fin )
68 12 66 67 syl2anc ⊢ ( 𝜑 → X 𝑥 ∈ 𝐴 𝐵 ∈ Fin )