ptcmpfi

Description: A topological product of finitely many compact spaces is compact. This weak version of Tychonoff's theorem does not require the axiom of choice. (Contributed by Mario Carneiro, 8-Feb-2015)

		Ref	Expression
	Assertion	ptcmpfi	$⊢ (A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} (F) \in Comp$

Proof

Step	Hyp	Ref	Expression
1		ffn	$⊢ F : A ⟶ Comp \to F Fn A$
2		fnresdm	$⊢ F Fn A \to {F ↾}_{A} = F$
3	1 2	syl	$⊢ F : A ⟶ Comp \to {F ↾}_{A} = F$
4	3	adantl	$⊢ (A \in Fin \land F : A ⟶ Comp) \to {F ↾}_{A} = F$
5	4	fveq2d	$⊢ (A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{A}) = \prod_{𝑡} (F)$
6		ssid	$⊢ A \subseteq A$
7		sseq1	$⊢ x = \emptyset \to (x \subseteq A \leftrightarrow \emptyset \subseteq A)$
8		reseq2	$⊢ x = \emptyset \to {F ↾}_{x} = {F ↾}_{\emptyset}$
9		res0	$⊢ {F ↾}_{\emptyset} = \emptyset$
10	8 9	eqtrdi	$⊢ x = \emptyset \to {F ↾}_{x} = \emptyset$
11	10	fveq2d	$⊢ x = \emptyset \to \prod_{𝑡} ({F ↾}_{x}) = \prod_{𝑡} (\emptyset)$
12	11	eleq1d	$⊢ x = \emptyset \to (\prod_{𝑡} ({F ↾}_{x}) \in Comp \leftrightarrow \prod_{𝑡} (\emptyset) \in Comp)$
13	12	imbi2d	$⊢ x = \emptyset \to (((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{x}) \in Comp) \leftrightarrow ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} (\emptyset) \in Comp))$
14	7 13	imbi12d	$⊢ x = \emptyset \to ((x \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{x}) \in Comp)) \leftrightarrow (\emptyset \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} (\emptyset) \in Comp)))$
15		sseq1	$⊢ x = y \to (x \subseteq A \leftrightarrow y \subseteq A)$
16		reseq2	$⊢ x = y \to {F ↾}_{x} = {F ↾}_{y}$
17	16	fveq2d	$⊢ x = y \to \prod_{𝑡} ({F ↾}_{x}) = \prod_{𝑡} ({F ↾}_{y})$
18	17	eleq1d	$⊢ x = y \to (\prod_{𝑡} ({F ↾}_{x}) \in Comp \leftrightarrow \prod_{𝑡} ({F ↾}_{y}) \in Comp)$
19	18	imbi2d	$⊢ x = y \to (((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{x}) \in Comp) \leftrightarrow ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{y}) \in Comp))$
20	15 19	imbi12d	$⊢ x = y \to ((x \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{x}) \in Comp)) \leftrightarrow (y \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{y}) \in Comp)))$
21		sseq1	$⊢ x = y \cup \{z\} \to (x \subseteq A \leftrightarrow y \cup \{z\} \subseteq A)$
22		reseq2	$⊢ x = y \cup \{z\} \to {F ↾}_{x} = {F ↾}_{(y \cup \{z\})}$
23	22	fveq2d	$⊢ x = y \cup \{z\} \to \prod_{𝑡} ({F ↾}_{x}) = \prod_{𝑡} ({F ↾}_{(y \cup \{z\})})$
24	23	eleq1d	$⊢ x = y \cup \{z\} \to (\prod_{𝑡} ({F ↾}_{x}) \in Comp \leftrightarrow \prod_{𝑡} ({F ↾}_{(y \cup \{z\})}) \in Comp)$
25	24	imbi2d	$⊢ x = y \cup \{z\} \to (((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{x}) \in Comp) \leftrightarrow ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{(y \cup \{z\})}) \in Comp))$
26	21 25	imbi12d	$⊢ x = y \cup \{z\} \to ((x \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{x}) \in Comp)) \leftrightarrow (y \cup \{z\} \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{(y \cup \{z\})}) \in Comp)))$
27		sseq1	$⊢ x = A \to (x \subseteq A \leftrightarrow A \subseteq A)$
28		reseq2	$⊢ x = A \to {F ↾}_{x} = {F ↾}_{A}$
29	28	fveq2d	$⊢ x = A \to \prod_{𝑡} ({F ↾}_{x}) = \prod_{𝑡} ({F ↾}_{A})$
30	29	eleq1d	$⊢ x = A \to (\prod_{𝑡} ({F ↾}_{x}) \in Comp \leftrightarrow \prod_{𝑡} ({F ↾}_{A}) \in Comp)$
31	30	imbi2d	$⊢ x = A \to (((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{x}) \in Comp) \leftrightarrow ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{A}) \in Comp))$
32	27 31	imbi12d	$⊢ x = A \to ((x \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{x}) \in Comp)) \leftrightarrow (A \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{A}) \in Comp)))$
33		0ex	$⊢ \emptyset \in V$
34		f0	$⊢ \emptyset : \emptyset ⟶ Top$
35		pttop	$⊢ (\emptyset \in V \land \emptyset : \emptyset ⟶ Top) \to \prod_{𝑡} (\emptyset) \in Top$
36	33 34 35	mp2an	$⊢ \prod_{𝑡} (\emptyset) \in Top$
37		eqid	$⊢ \prod_{𝑡} (\emptyset) = \prod_{𝑡} (\emptyset)$
38	37	ptuni	$⊢ (\emptyset \in V \land \emptyset : \emptyset ⟶ Top) \to \underset{x \in \emptyset}{⨉} ⋃ \emptyset (x) = ⋃ \prod_{𝑡} (\emptyset)$
39	33 34 38	mp2an	$⊢ \underset{x \in \emptyset}{⨉} ⋃ \emptyset (x) = ⋃ \prod_{𝑡} (\emptyset)$
40		ixp0x	$⊢ \underset{x \in \emptyset}{⨉} ⋃ \emptyset (x) = \{\emptyset\}$
41		snfi	$⊢ \{\emptyset\} \in Fin$
42	40 41	eqeltri	$⊢ \underset{x \in \emptyset}{⨉} ⋃ \emptyset (x) \in Fin$
43	39 42	eqeltrri	$⊢ ⋃ \prod_{𝑡} (\emptyset) \in Fin$
44		pwfi	$⊢ ⋃ \prod_{𝑡} (\emptyset) \in Fin \leftrightarrow 𝒫 ⋃ \prod_{𝑡} (\emptyset) \in Fin$
45	43 44	mpbi	$⊢ 𝒫 ⋃ \prod_{𝑡} (\emptyset) \in Fin$
46		pwuni	$⊢ \prod_{𝑡} (\emptyset) \subseteq 𝒫 ⋃ \prod_{𝑡} (\emptyset)$
47		ssfi	$⊢ (𝒫 ⋃ \prod_{𝑡} (\emptyset) \in Fin \land \prod_{𝑡} (\emptyset) \subseteq 𝒫 ⋃ \prod_{𝑡} (\emptyset)) \to \prod_{𝑡} (\emptyset) \in Fin$
48	45 46 47	mp2an	$⊢ \prod_{𝑡} (\emptyset) \in Fin$
49	36 48	elini	$⊢ \prod_{𝑡} (\emptyset) \in (Top \cap Fin)$
50		fincmp	$⊢ \prod_{𝑡} (\emptyset) \in (Top \cap Fin) \to \prod_{𝑡} (\emptyset) \in Comp$
51	49 50	ax-mp	$⊢ \prod_{𝑡} (\emptyset) \in Comp$
52	51	2a1i	$⊢ \emptyset \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} (\emptyset) \in Comp)$
53		ssun1	$⊢ y \subseteq y \cup \{z\}$
54		id	$⊢ y \cup \{z\} \subseteq A \to y \cup \{z\} \subseteq A$
55	53 54	sstrid	$⊢ y \cup \{z\} \subseteq A \to y \subseteq A$
56	55	imim1i	$⊢ (y \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{y}) \in Comp)) \to (y \cup \{z\} \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{y}) \in Comp))$
57		eqid	$⊢ ⋃ \prod_{𝑡} ({F ↾}_{y}) = ⋃ \prod_{𝑡} ({F ↾}_{y})$
58		eqid	$⊢ ⋃ \prod_{𝑡} ({F ↾}_{\{z\}}) = ⋃ \prod_{𝑡} ({F ↾}_{\{z\}})$
59		eqid	$⊢ \prod_{𝑡} ({F ↾}_{(y \cup \{z\})}) = \prod_{𝑡} ({F ↾}_{(y \cup \{z\})})$
60		resabs1	$⊢ y \subseteq y \cup \{z\} \to {({F ↾}_{(y \cup \{z\})}) ↾}_{y} = {F ↾}_{y}$
61	53 60	ax-mp	$⊢ {({F ↾}_{(y \cup \{z\})}) ↾}_{y} = {F ↾}_{y}$
62	61	eqcomi	$⊢ {F ↾}_{y} = {({F ↾}_{(y \cup \{z\})}) ↾}_{y}$
63	62	fveq2i	$⊢ \prod_{𝑡} ({F ↾}_{y}) = \prod_{𝑡} ({({F ↾}_{(y \cup \{z\})}) ↾}_{y})$
64		ssun2	$⊢ \{z\} \subseteq y \cup \{z\}$
65		resabs1	$⊢ \{z\} \subseteq y \cup \{z\} \to {({F ↾}_{(y \cup \{z\})}) ↾}_{\{z\}} = {F ↾}_{\{z\}}$
66	64 65	ax-mp	$⊢ {({F ↾}_{(y \cup \{z\})}) ↾}_{\{z\}} = {F ↾}_{\{z\}}$
67	66	eqcomi	$⊢ {F ↾}_{\{z\}} = {({F ↾}_{(y \cup \{z\})}) ↾}_{\{z\}}$
68	67	fveq2i	$⊢ \prod_{𝑡} ({F ↾}_{\{z\}}) = \prod_{𝑡} ({({F ↾}_{(y \cup \{z\})}) ↾}_{\{z\}})$
69		eqid	$⊢ (u \in ⋃ \prod_{𝑡} ({F ↾}_{y}), v \in ⋃ \prod_{𝑡} ({F ↾}_{\{z\}}) ⟼ u \cup v) = (u \in ⋃ \prod_{𝑡} ({F ↾}_{y}), v \in ⋃ \prod_{𝑡} ({F ↾}_{\{z\}}) ⟼ u \cup v)$
70		vex	$⊢ y \in V$
71		vsnex	$⊢ \{z\} \in V$
72	70 71	unex	$⊢ y \cup \{z\} \in V$
73	72	a1i	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to y \cup \{z\} \in V$
74		simplr	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to F : A ⟶ Comp$
75		cmptop	$⊢ x \in Comp \to x \in Top$
76	75	ssriv	$⊢ Comp \subseteq Top$
77		fss	$⊢ (F : A ⟶ Comp \land Comp \subseteq Top) \to F : A ⟶ Top$
78	74 76 77	sylancl	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to F : A ⟶ Top$
79		simprr	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to y \cup \{z\} \subseteq A$
80	78 79	fssresd	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to ({F ↾}_{(y \cup \{z\})}) : y \cup \{z\} ⟶ Top$
81		eqidd	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to y \cup \{z\} = y \cup \{z\}$
82		simprl	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to \neg z \in y$
83		disjsn	$⊢ y \cap \{z\} = \emptyset \leftrightarrow \neg z \in y$
84	82 83	sylibr	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to y \cap \{z\} = \emptyset$
85	57 58 59 63 68 69 73 80 81 84	ptunhmeo	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to (u \in ⋃ \prod_{𝑡} ({F ↾}_{y}), v \in ⋃ \prod_{𝑡} ({F ↾}_{\{z\}}) ⟼ u \cup v) \in ((\prod_{𝑡} ({F ↾}_{y}) \times_{t} \prod_{𝑡} ({F ↾}_{\{z\}})) Homeo \prod_{𝑡} ({F ↾}_{(y \cup \{z\})}))$
86		hmphi	$⊢ (u \in ⋃ \prod_{𝑡} ({F ↾}_{y}), v \in ⋃ \prod_{𝑡} ({F ↾}_{\{z\}}) ⟼ u \cup v) \in ((\prod_{𝑡} ({F ↾}_{y}) \times_{t} \prod_{𝑡} ({F ↾}_{\{z\}})) Homeo \prod_{𝑡} ({F ↾}_{(y \cup \{z\})})) \to (\prod_{𝑡} ({F ↾}_{y}) \times_{t} \prod_{𝑡} ({F ↾}_{\{z\}})) ≃ \prod_{𝑡} ({F ↾}_{(y \cup \{z\})})$
87	85 86	syl	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to (\prod_{𝑡} ({F ↾}_{y}) \times_{t} \prod_{𝑡} ({F ↾}_{\{z\}})) ≃ \prod_{𝑡} ({F ↾}_{(y \cup \{z\})})$
88	1	ad2antlr	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to F Fn A$
89	64 79	sstrid	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to \{z\} \subseteq A$
90		vex	$⊢ z \in V$
91	90	snss	$⊢ z \in A \leftrightarrow \{z\} \subseteq A$
92	89 91	sylibr	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to z \in A$
93		fnressn	$⊢ (F Fn A \land z \in A) \to {F ↾}_{\{z\}} = \{⟨z, F (z)⟩\}$
94	88 92 93	syl2anc	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to {F ↾}_{\{z\}} = \{⟨z, F (z)⟩\}$
95	94	fveq2d	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to \prod_{𝑡} ({F ↾}_{\{z\}}) = \prod_{𝑡} (\{⟨z, F (z)⟩\})$
96		eqid	$⊢ \prod_{𝑡} (\{⟨z, F (z)⟩\}) = \prod_{𝑡} (\{⟨z, F (z)⟩\})$
97	90	a1i	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to z \in V$
98	74 92	ffvelcdmd	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to F (z) \in Comp$
99	76 98	sselid	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to F (z) \in Top$
100		toptopon2	$⊢ F (z) \in Top \leftrightarrow F (z) \in TopOn (⋃ F (z))$
101	99 100	sylib	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to F (z) \in TopOn (⋃ F (z))$
102	96 97 101	pt1hmeo	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to (x \in ⋃ F (z) ⟼ \{⟨z, x⟩\}) \in (F (z) Homeo \prod_{𝑡} (\{⟨z, F (z)⟩\}))$
103		hmphi	$⊢ (x \in ⋃ F (z) ⟼ \{⟨z, x⟩\}) \in (F (z) Homeo \prod_{𝑡} (\{⟨z, F (z)⟩\})) \to F (z) ≃ \prod_{𝑡} (\{⟨z, F (z)⟩\})$
104	102 103	syl	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to F (z) ≃ \prod_{𝑡} (\{⟨z, F (z)⟩\})$
105		cmphmph	$⊢ F (z) ≃ \prod_{𝑡} (\{⟨z, F (z)⟩\}) \to (F (z) \in Comp \to \prod_{𝑡} (\{⟨z, F (z)⟩\}) \in Comp)$
106	104 98 105	sylc	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to \prod_{𝑡} (\{⟨z, F (z)⟩\}) \in Comp$
107	95 106	eqeltrd	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to \prod_{𝑡} ({F ↾}_{\{z\}}) \in Comp$
108		txcmp	$⊢ (\prod_{𝑡} ({F ↾}_{y}) \in Comp \land \prod_{𝑡} ({F ↾}_{\{z\}}) \in Comp) \to \prod_{𝑡} ({F ↾}_{y}) \times_{t} \prod_{𝑡} ({F ↾}_{\{z\}}) \in Comp$
109	108	expcom	$⊢ \prod_{𝑡} ({F ↾}_{\{z\}}) \in Comp \to (\prod_{𝑡} ({F ↾}_{y}) \in Comp \to \prod_{𝑡} ({F ↾}_{y}) \times_{t} \prod_{𝑡} ({F ↾}_{\{z\}}) \in Comp)$
110	107 109	syl	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to (\prod_{𝑡} ({F ↾}_{y}) \in Comp \to \prod_{𝑡} ({F ↾}_{y}) \times_{t} \prod_{𝑡} ({F ↾}_{\{z\}}) \in Comp)$
111		cmphmph	$⊢ (\prod_{𝑡} ({F ↾}_{y}) \times_{t} \prod_{𝑡} ({F ↾}_{\{z\}})) ≃ \prod_{𝑡} ({F ↾}_{(y \cup \{z\})}) \to (\prod_{𝑡} ({F ↾}_{y}) \times_{t} \prod_{𝑡} ({F ↾}_{\{z\}}) \in Comp \to \prod_{𝑡} ({F ↾}_{(y \cup \{z\})}) \in Comp)$
112	87 110 111	sylsyld	$⊢ ((A \in Fin \land F : A ⟶ Comp) \land (\neg z \in y \land y \cup \{z\} \subseteq A)) \to (\prod_{𝑡} ({F ↾}_{y}) \in Comp \to \prod_{𝑡} ({F ↾}_{(y \cup \{z\})}) \in Comp)$
113	112	expcom	$⊢ (\neg z \in y \land y \cup \{z\} \subseteq A) \to ((A \in Fin \land F : A ⟶ Comp) \to (\prod_{𝑡} ({F ↾}_{y}) \in Comp \to \prod_{𝑡} ({F ↾}_{(y \cup \{z\})}) \in Comp))$
114	113	a2d	$⊢ (\neg z \in y \land y \cup \{z\} \subseteq A) \to (((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{y}) \in Comp) \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{(y \cup \{z\})}) \in Comp))$
115	114	ex	$⊢ \neg z \in y \to (y \cup \{z\} \subseteq A \to (((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{y}) \in Comp) \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{(y \cup \{z\})}) \in Comp)))$
116	115	a2d	$⊢ \neg z \in y \to ((y \cup \{z\} \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{y}) \in Comp)) \to (y \cup \{z\} \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{(y \cup \{z\})}) \in Comp)))$
117	56 116	syl5	$⊢ \neg z \in y \to ((y \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{y}) \in Comp)) \to (y \cup \{z\} \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{(y \cup \{z\})}) \in Comp)))$
118	117	adantl	$⊢ (y \in Fin \land \neg z \in y) \to ((y \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{y}) \in Comp)) \to (y \cup \{z\} \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{(y \cup \{z\})}) \in Comp)))$
119	14 20 26 32 52 118	findcard2s	$⊢ A \in Fin \to (A \subseteq A \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{A}) \in Comp))$
120	6 119	mpi	$⊢ A \in Fin \to ((A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{A}) \in Comp)$
121	120	anabsi5	$⊢ (A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} ({F ↾}_{A}) \in Comp$
122	5 121	eqeltrrd	$⊢ (A \in Fin \land F : A ⟶ Comp) \to \prod_{𝑡} (F) \in Comp$

Metamath Proof Explorer

Theorem ptcmpfi

Proof