Theorem ptcmpfi 23822

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.)

Assertion

Ref	Expression
ptcmpfi	⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘𝐹) ∈ Comp)

Proof of Theorem ptcmpfi

Dummy variables 𝑣 𝑢 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ffn 6735	. . . . 5 ⊢ (𝐹:𝐴⟶Comp → 𝐹 Fn 𝐴)
2		fnresdm 6686	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
3	1, 2	syl 17	. . . 4 ⊢ (𝐹:𝐴⟶Comp → (𝐹 ↾ 𝐴) = 𝐹)
4	3	adantl 481	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (𝐹 ↾ 𝐴) = 𝐹)
5	4	fveq2d 6909	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) = (∏t‘𝐹))
6		ssid 4005	. . . 4 ⊢ 𝐴 ⊆ 𝐴
7		sseq1 4008	. . . . . 6 ⊢ (𝑥 = ∅ → (𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴))
8		reseq2 5991	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → (𝐹 ↾ 𝑥) = (𝐹 ↾ ∅))
9		res0 6000	. . . . . . . . . 10 ⊢ (𝐹 ↾ ∅) = ∅
10	8, 9	eqtrdi 2792	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝐹 ↾ 𝑥) = ∅)
11	10	fveq2d 6909	. . . . . . . 8 ⊢ (𝑥 = ∅ → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘∅))
12	11	eleq1d 2825	. . . . . . 7 ⊢ (𝑥 = ∅ → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔ (∏t‘∅) ∈ Comp))
13	12	imbi2d 340	. . . . . 6 ⊢ (𝑥 = ∅ → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘∅) ∈ Comp)))
14	7, 13	imbi12d 344	. . . . 5 ⊢ (𝑥 = ∅ → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ (∅ ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘∅) ∈ Comp))))
15		sseq1 4008	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴))
16		reseq2 5991	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐹 ↾ 𝑥) = (𝐹 ↾ 𝑦))
17	16	fveq2d 6909	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ 𝑦)))
18	17	eleq1d 2825	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔ (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp))
19	18	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝑦 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)))
20	15, 19	imbi12d 344	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ (𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp))))
21		sseq1 4008	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥 ⊆ 𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴))
22		reseq2 5991	. . . . . . . . 9 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹 ↾ 𝑥) = (𝐹 ↾ (𝑦 ∪ {𝑧})))
23	22	fveq2d 6909	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))))
24	23	eleq1d 2825	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))
25	24	imbi2d 340	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
26	21, 25	imbi12d 344	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
27		sseq1 4008	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
28		reseq2 5991	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝐹 ↾ 𝑥) = (𝐹 ↾ 𝐴))
29	28	fveq2d 6909	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ 𝐴)))
30	29	eleq1d 2825	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔ (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp))
31	30	imbi2d 340	. . . . . 6 ⊢ (𝑥 = 𝐴 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp)))
32	27, 31	imbi12d 344	. . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ (𝐴 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp))))
33		0ex 5306	. . . . . . . . 9 ⊢ ∅ ∈ V
34		f0 6788	. . . . . . . . 9 ⊢ ∅:∅⟶Top
35		pttop 23591	. . . . . . . . 9 ⊢ ((∅ ∈ V ∧ ∅:∅⟶Top) → (∏t‘∅) ∈ Top)
36	33, 34, 35	mp2an 692	. . . . . . . 8 ⊢ (∏t‘∅) ∈ Top
37		eqid 2736	. . . . . . . . . . . . 13 ⊢ (∏t‘∅) = (∏t‘∅)
38	37	ptuni 23603	. . . . . . . . . . . 12 ⊢ ((∅ ∈ V ∧ ∅:∅⟶Top) → X𝑥 ∈ ∅ ∪ (∅‘𝑥) = ∪ (∏t‘∅))
39	33, 34, 38	mp2an 692	. . . . . . . . . . 11 ⊢ X𝑥 ∈ ∅ ∪ (∅‘𝑥) = ∪ (∏t‘∅)
40		ixp0x 8967	. . . . . . . . . . . 12 ⊢ X𝑥 ∈ ∅ ∪ (∅‘𝑥) = {∅}
41		snfi 9084	. . . . . . . . . . . 12 ⊢ {∅} ∈ Fin
42	40, 41	eqeltri 2836	. . . . . . . . . . 11 ⊢ X𝑥 ∈ ∅ ∪ (∅‘𝑥) ∈ Fin
43	39, 42	eqeltrri 2837	. . . . . . . . . 10 ⊢ ∪ (∏t‘∅) ∈ Fin
44		pwfi 9358	. . . . . . . . . 10 ⊢ (∪ (∏t‘∅) ∈ Fin ↔ 𝒫 ∪ (∏t‘∅) ∈ Fin)
45	43, 44	mpbi 230	. . . . . . . . 9 ⊢ 𝒫 ∪ (∏t‘∅) ∈ Fin
46		pwuni 4944	. . . . . . . . 9 ⊢ (∏t‘∅) ⊆ 𝒫 ∪ (∏t‘∅)
47		ssfi 9214	. . . . . . . . 9 ⊢ ((𝒫 ∪ (∏t‘∅) ∈ Fin ∧ (∏t‘∅) ⊆ 𝒫 ∪ (∏t‘∅)) → (∏t‘∅) ∈ Fin)
48	45, 46, 47	mp2an 692	. . . . . . . 8 ⊢ (∏t‘∅) ∈ Fin
49	36, 48	elini 4198	. . . . . . 7 ⊢ (∏t‘∅) ∈ (Top ∩ Fin)
50		fincmp 23402	. . . . . . 7 ⊢ ((∏t‘∅) ∈ (Top ∩ Fin) → (∏t‘∅) ∈ Comp)
51	49, 50	ax-mp 5	. . . . . 6 ⊢ (∏t‘∅) ∈ Comp
52	51	2a1i 12	. . . . 5 ⊢ (∅ ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘∅) ∈ Comp))
53		ssun1 4177	. . . . . . . . 9 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
54		id 22	. . . . . . . . 9 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
55	53, 54	sstrid 3994	. . . . . . . 8 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → 𝑦 ⊆ 𝐴)
56	55	imim1i 63	. . . . . . 7 ⊢ ((𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)))
57		eqid 2736	. . . . . . . . . . . . . 14 ⊢ ∪ (∏t‘(𝐹 ↾ 𝑦)) = ∪ (∏t‘(𝐹 ↾ 𝑦))
58		eqid 2736	. . . . . . . . . . . . . 14 ⊢ ∪ (∏t‘(𝐹 ↾ {𝑧})) = ∪ (∏t‘(𝐹 ↾ {𝑧}))
59		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) = (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))
60		resabs1 6023	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦) = (𝐹 ↾ 𝑦))
61	53, 60	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦) = (𝐹 ↾ 𝑦)
62	61	eqcomi 2745	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ↾ 𝑦) = ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦)
63	62	fveq2i 6908	. . . . . . . . . . . . . 14 ⊢ (∏t‘(𝐹 ↾ 𝑦)) = (∏t‘((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦))
64		ssun2 4178	. . . . . . . . . . . . . . . . 17 ⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧})
65		resabs1 6023	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧} ⊆ (𝑦 ∪ {𝑧}) → ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}) = (𝐹 ↾ {𝑧}))
66	64, 65	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}) = (𝐹 ↾ {𝑧})
67	66	eqcomi 2745	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ↾ {𝑧}) = ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧})
68	67	fveq2i 6908	. . . . . . . . . . . . . 14 ⊢ (∏t‘(𝐹 ↾ {𝑧})) = (∏t‘((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}))
69		eqid 2736	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪ (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣)) = (𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪ (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣))
70		vex 3483	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
71		vsnex 5433	. . . . . . . . . . . . . . . 16 ⊢ {𝑧} ∈ V
72	70, 71	unex 7765	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∪ {𝑧}) ∈ V
73	72	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) ∈ V)
74		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹:𝐴⟶Comp)
75		cmptop 23404	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Comp → 𝑥 ∈ Top)
76	75	ssriv 3986	. . . . . . . . . . . . . . . 16 ⊢ Comp ⊆ Top
77		fss 6751	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴⟶Comp ∧ Comp ⊆ Top) → 𝐹:𝐴⟶Top)
78	74, 76, 77	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹:𝐴⟶Top)
79		simprr 772	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
80	78, 79	fssresd 6774	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹 ↾ (𝑦 ∪ {𝑧})):(𝑦 ∪ {𝑧})⟶Top)
81		eqidd 2737	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) = (𝑦 ∪ {𝑧}))
82		simprl 770	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ¬ 𝑧 ∈ 𝑦)
83		disjsn 4710	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦)
84	82, 83	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∩ {𝑧}) = ∅)
85	57, 58, 59, 63, 68, 69, 73, 80, 81, 84	ptunhmeo 23817	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪ (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣)) ∈ (((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧})))Homeo(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))))
86		hmphi 23786	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪ (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣)) ∈ (((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧})))Homeo(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))) → ((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ≃ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))))
87	85, 86	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ≃ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))))
88	1	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹 Fn 𝐴)
89	64, 79	sstrid 3994	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → {𝑧} ⊆ 𝐴)
90		vex 3483	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑧 ∈ V
91	90	snss 4784	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴)
92	89, 91	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ 𝐴)
93		fnressn 7177	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝐹 ↾ {𝑧}) = {⟨𝑧, (𝐹‘𝑧)⟩})
94	88, 92, 93	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹 ↾ {𝑧}) = {⟨𝑧, (𝐹‘𝑧)⟩})
95	94	fveq2d 6909	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘(𝐹 ↾ {𝑧})) = (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}))
96		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) = (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩})
97	90	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ V)
98	74, 92	ffvelcdmd 7104	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ Comp)
99	76, 98	sselid 3980	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ Top)
100		toptopon2 22925	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑧) ∈ Top ↔ (𝐹‘𝑧) ∈ (TopOn‘∪ (𝐹‘𝑧)))
101	99, 100	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ (TopOn‘∪ (𝐹‘𝑧)))
102	96, 97, 101	pt1hmeo 23815	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑥 ∈ ∪ (𝐹‘𝑧) ↦ {⟨𝑧, 𝑥⟩}) ∈ ((𝐹‘𝑧)Homeo(∏t‘{⟨𝑧, (𝐹‘𝑧)⟩})))
103		hmphi 23786	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ∪ (𝐹‘𝑧) ↦ {⟨𝑧, 𝑥⟩}) ∈ ((𝐹‘𝑧)Homeo(∏t‘{⟨𝑧, (𝐹‘𝑧)⟩})) → (𝐹‘𝑧) ≃ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}))
104	102, 103	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ≃ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}))
105		cmphmph 23797	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑧) ≃ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) → ((𝐹‘𝑧) ∈ Comp → (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) ∈ Comp))
106	104, 98, 105	sylc 65	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) ∈ Comp)
107	95, 106	eqeltrd 2840	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘(𝐹 ↾ {𝑧})) ∈ Comp)
108		txcmp 23652	. . . . . . . . . . . . . 14 ⊢ (((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp ∧ (∏t‘(𝐹 ↾ {𝑧})) ∈ Comp) → ((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp)
109	108	expcom 413	. . . . . . . . . . . . 13 ⊢ ((∏t‘(𝐹 ↾ {𝑧})) ∈ Comp → ((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp → ((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp))
110	107, 109	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp → ((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp))
111		cmphmph 23797	. . . . . . . . . . . 12 ⊢ (((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ≃ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) → (((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))
112	87, 110, 111	sylsyld 61	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))
113	112	expcom 413	. . . . . . . . . 10 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → ((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
114	113	a2d 29	. . . . . . . . 9 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
115	114	ex 412	. . . . . . . 8 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
116	115	a2d 29	. . . . . . 7 ⊢ (¬ 𝑧 ∈ 𝑦 → (((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
117	56, 116	syl5 34	. . . . . 6 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
118	117	adantl 481	. . . . 5 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
119	14, 20, 26, 32, 52, 118	findcard2s 9206	. . . 4 ⊢ (𝐴 ∈ Fin → (𝐴 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp)))
120	6, 119	mpi 20	. . 3 ⊢ (𝐴 ∈ Fin → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp))
121	120	anabsi5 669	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp)
122	5, 121	eqeltrrd 2841	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘𝐹) ∈ Comp)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  Vcvv 3479   ∪ cun 3948   ∩ cin 3949   ⊆ wss 3950  ∅c0 4332  𝒫 cpw 4599  {csn 4625  ⟨cop 4631  ∪ cuni 4906   class class class wbr 5142   ↦ cmpt 5224   ↾ cres 5686   Fn wfn 6555  ⟶wf 6556  ‘cfv 6560  (class class class)co 7432   ∈ cmpo 7434  Xcixp 8938  Fincfn 8986  ∏_tcpt 17484  Topctop 22900  TopOnctopon 22917  Compccmp 23395   ×_t ctx 23569  Homeochmeo 23762   ≃ chmph 23763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-iin 4993  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-1o 8507  df-2o 8508  df-map 8869  df-ixp 8939  df-en 8987  df-dom 8988  df-fin 8990  df-fi 9452  df-topgen 17489  df-pt 17490  df-top 22901  df-topon 22918  df-bases 22954  df-cn 23236  df-cnp 23237  df-cmp 23396  df-tx 23571  df-hmeo 23764  df-hmph 23765

This theorem is referenced by:  poimirlem30  37658