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	$⊢ φ \to C \in Fin$
	ixpfi2.2	$⊢ (φ \land x \in A) \to B \in Fin$
	ixpfi2.3	$⊢ (φ \land x \in (A ∖ C)) \to B \subseteq \{D\}$
Assertion	ixpfi2	$⊢ φ \to \underset{x \in A}{⨉} B \in Fin$

Proof

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

Metamath Proof Explorer

Theorem ixpfi2

Proof