Theorem ptcmpfi 22964

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 6600	. . . . 5 ⊢ (𝐹:𝐴⟶Comp → 𝐹 Fn 𝐴)
2		fnresdm 6551	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
3	1, 2	syl 17	. . . 4 ⊢ (𝐹:𝐴⟶Comp → (𝐹 ↾ 𝐴) = 𝐹)
4	3	adantl 482	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (𝐹 ↾ 𝐴) = 𝐹)
5	4	fveq2d 6778	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) = (∏t‘𝐹))
6		ssid 3943	. . . 4 ⊢ 𝐴 ⊆ 𝐴
7		sseq1 3946	. . . . . 6 ⊢ (𝑥 = ∅ → (𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴))
8		reseq2 5886	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → (𝐹 ↾ 𝑥) = (𝐹 ↾ ∅))
9		res0 5895	. . . . . . . . . 10 ⊢ (𝐹 ↾ ∅) = ∅
10	8, 9	eqtrdi 2794	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝐹 ↾ 𝑥) = ∅)
11	10	fveq2d 6778	. . . . . . . 8 ⊢ (𝑥 = ∅ → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘∅))
12	11	eleq1d 2823	. . . . . . 7 ⊢ (𝑥 = ∅ → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔ (∏t‘∅) ∈ Comp))
13	12	imbi2d 341	. . . . . 6 ⊢ (𝑥 = ∅ → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘∅) ∈ Comp)))
14	7, 13	imbi12d 345	. . . . 5 ⊢ (𝑥 = ∅ → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ (∅ ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘∅) ∈ Comp))))
15		sseq1 3946	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴))
16		reseq2 5886	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐹 ↾ 𝑥) = (𝐹 ↾ 𝑦))
17	16	fveq2d 6778	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ 𝑦)))
18	17	eleq1d 2823	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔ (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp))
19	18	imbi2d 341	. . . . . 6 ⊢ (𝑥 = 𝑦 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)))
20	15, 19	imbi12d 345	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ (𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp))))
21		sseq1 3946	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥 ⊆ 𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴))
22		reseq2 5886	. . . . . . . . 9 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹 ↾ 𝑥) = (𝐹 ↾ (𝑦 ∪ {𝑧})))
23	22	fveq2d 6778	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))))
24	23	eleq1d 2823	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))
25	24	imbi2d 341	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
26	21, 25	imbi12d 345	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
27		sseq1 3946	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
28		reseq2 5886	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝐹 ↾ 𝑥) = (𝐹 ↾ 𝐴))
29	28	fveq2d 6778	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ 𝐴)))
30	29	eleq1d 2823	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔ (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp))
31	30	imbi2d 341	. . . . . 6 ⊢ (𝑥 = 𝐴 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp)))
32	27, 31	imbi12d 345	. . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ (𝐴 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp))))
33		0ex 5231	. . . . . . . . 9 ⊢ ∅ ∈ V
34		f0 6655	. . . . . . . . 9 ⊢ ∅:∅⟶Top
35		pttop 22733	. . . . . . . . 9 ⊢ ((∅ ∈ V ∧ ∅:∅⟶Top) → (∏t‘∅) ∈ Top)
36	33, 34, 35	mp2an 689	. . . . . . . 8 ⊢ (∏t‘∅) ∈ Top
37		eqid 2738	. . . . . . . . . . . . 13 ⊢ (∏t‘∅) = (∏t‘∅)
38	37	ptuni 22745	. . . . . . . . . . . 12 ⊢ ((∅ ∈ V ∧ ∅:∅⟶Top) → X𝑥 ∈ ∅ ∪ (∅‘𝑥) = ∪ (∏t‘∅))
39	33, 34, 38	mp2an 689	. . . . . . . . . . 11 ⊢ X𝑥 ∈ ∅ ∪ (∅‘𝑥) = ∪ (∏t‘∅)
40		ixp0x 8714	. . . . . . . . . . . 12 ⊢ X𝑥 ∈ ∅ ∪ (∅‘𝑥) = {∅}
41		snfi 8834	. . . . . . . . . . . 12 ⊢ {∅} ∈ Fin
42	40, 41	eqeltri 2835	. . . . . . . . . . 11 ⊢ X𝑥 ∈ ∅ ∪ (∅‘𝑥) ∈ Fin
43	39, 42	eqeltrri 2836	. . . . . . . . . 10 ⊢ ∪ (∏t‘∅) ∈ Fin
44		pwfi 8961	. . . . . . . . . 10 ⊢ (∪ (∏t‘∅) ∈ Fin ↔ 𝒫 ∪ (∏t‘∅) ∈ Fin)
45	43, 44	mpbi 229	. . . . . . . . 9 ⊢ 𝒫 ∪ (∏t‘∅) ∈ Fin
46		pwuni 4878	. . . . . . . . 9 ⊢ (∏t‘∅) ⊆ 𝒫 ∪ (∏t‘∅)
47		ssfi 8956	. . . . . . . . 9 ⊢ ((𝒫 ∪ (∏t‘∅) ∈ Fin ∧ (∏t‘∅) ⊆ 𝒫 ∪ (∏t‘∅)) → (∏t‘∅) ∈ Fin)
48	45, 46, 47	mp2an 689	. . . . . . . 8 ⊢ (∏t‘∅) ∈ Fin
49	36, 48	elini 4127	. . . . . . 7 ⊢ (∏t‘∅) ∈ (Top ∩ Fin)
50		fincmp 22544	. . . . . . 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 4106	. . . . . . . . 9 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
54		id 22	. . . . . . . . 9 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
55	53, 54	sstrid 3932	. . . . . . . 8 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → 𝑦 ⊆ 𝐴)
56	55	imim1i 63	. . . . . . 7 ⊢ ((𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)))
57		eqid 2738	. . . . . . . . . . . . . 14 ⊢ ∪ (∏t‘(𝐹 ↾ 𝑦)) = ∪ (∏t‘(𝐹 ↾ 𝑦))
58		eqid 2738	. . . . . . . . . . . . . 14 ⊢ ∪ (∏t‘(𝐹 ↾ {𝑧})) = ∪ (∏t‘(𝐹 ↾ {𝑧}))
59		eqid 2738	. . . . . . . . . . . . . 14 ⊢ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) = (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))
60		resabs1 5921	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦) = (𝐹 ↾ 𝑦))
61	53, 60	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦) = (𝐹 ↾ 𝑦)
62	61	eqcomi 2747	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ↾ 𝑦) = ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦)
63	62	fveq2i 6777	. . . . . . . . . . . . . 14 ⊢ (∏t‘(𝐹 ↾ 𝑦)) = (∏t‘((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦))
64		ssun2 4107	. . . . . . . . . . . . . . . . 17 ⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧})
65		resabs1 5921	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧} ⊆ (𝑦 ∪ {𝑧}) → ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}) = (𝐹 ↾ {𝑧}))
66	64, 65	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}) = (𝐹 ↾ {𝑧})
67	66	eqcomi 2747	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ↾ {𝑧}) = ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧})
68	67	fveq2i 6777	. . . . . . . . . . . . . 14 ⊢ (∏t‘(𝐹 ↾ {𝑧})) = (∏t‘((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}))
69		eqid 2738	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪ (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣)) = (𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪ (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣))
70		vex 3436	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
71		snex 5354	. . . . . . . . . . . . . . . 16 ⊢ {𝑧} ∈ V
72	70, 71	unex 7596	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∪ {𝑧}) ∈ V
73	72	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) ∈ V)
74		simplr 766	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹:𝐴⟶Comp)
75		cmptop 22546	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Comp → 𝑥 ∈ Top)
76	75	ssriv 3925	. . . . . . . . . . . . . . . 16 ⊢ Comp ⊆ Top
77		fss 6617	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴⟶Comp ∧ Comp ⊆ Top) → 𝐹:𝐴⟶Top)
78	74, 76, 77	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹:𝐴⟶Top)
79		simprr 770	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
80	78, 79	fssresd 6641	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹 ↾ (𝑦 ∪ {𝑧})):(𝑦 ∪ {𝑧})⟶Top)
81		eqidd 2739	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) = (𝑦 ∪ {𝑧}))
82		simprl 768	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ¬ 𝑧 ∈ 𝑦)
83		disjsn 4647	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦)
84	82, 83	sylibr 233	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∩ {𝑧}) = ∅)
85	57, 58, 59, 63, 68, 69, 73, 80, 81, 84	ptunhmeo 22959	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪ (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣)) ∈ (((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧})))Homeo(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))))
86		hmphi 22928	. . . . . . . . . . . . 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 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹 Fn 𝐴)
89	64, 79	sstrid 3932	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → {𝑧} ⊆ 𝐴)
90		vex 3436	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑧 ∈ V
91	90	snss 4719	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴)
92	89, 91	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ 𝐴)
93		fnressn 7030	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝐹 ↾ {𝑧}) = {⟨𝑧, (𝐹‘𝑧)⟩})
94	88, 92, 93	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹 ↾ {𝑧}) = {⟨𝑧, (𝐹‘𝑧)⟩})
95	94	fveq2d 6778	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘(𝐹 ↾ {𝑧})) = (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}))
96		eqid 2738	. . . . . . . . . . . . . . . . 17 ⊢ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) = (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩})
97	90	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ V)
98	74, 92	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ Comp)
99	76, 98	sselid 3919	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ Top)
100		toptopon2 22067	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑧) ∈ Top ↔ (𝐹‘𝑧) ∈ (TopOn‘∪ (𝐹‘𝑧)))
101	99, 100	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ (TopOn‘∪ (𝐹‘𝑧)))
102	96, 97, 101	pt1hmeo 22957	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑥 ∈ ∪ (𝐹‘𝑧) ↦ {⟨𝑧, 𝑥⟩}) ∈ ((𝐹‘𝑧)Homeo(∏t‘{⟨𝑧, (𝐹‘𝑧)⟩})))
103		hmphi 22928	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ∪ (𝐹‘𝑧) ↦ {⟨𝑧, 𝑥⟩}) ∈ ((𝐹‘𝑧)Homeo(∏t‘{⟨𝑧, (𝐹‘𝑧)⟩})) → (𝐹‘𝑧) ≃ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}))
104	102, 103	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ≃ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}))
105		cmphmph 22939	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑧) ≃ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) → ((𝐹‘𝑧) ∈ Comp → (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) ∈ Comp))
106	104, 98, 105	sylc 65	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) ∈ Comp)
107	95, 106	eqeltrd 2839	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘(𝐹 ↾ {𝑧})) ∈ Comp)
108		txcmp 22794	. . . . . . . . . . . . . 14 ⊢ (((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp ∧ (∏t‘(𝐹 ↾ {𝑧})) ∈ Comp) → ((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp)
109	108	expcom 414	. . . . . . . . . . . . 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 22939	. . . . . . . . . . . 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 414	. . . . . . . . . 10 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → ((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
114	113	a2d 29	. . . . . . . . 9 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
115	114	ex 413	. . . . . . . 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 482	. . . . 5 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
119	14, 20, 26, 32, 52, 118	findcard2s 8948	. . . 4 ⊢ (𝐴 ∈ Fin → (𝐴 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp)))
120	6, 119	mpi 20	. . 3 ⊢ (𝐴 ∈ Fin → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp))
121	120	anabsi5 666	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp)
122	5, 121	eqeltrrd 2840	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘𝐹) ∈ Comp)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  Vcvv 3432   ∪ cun 3885   ∩ cin 3886   ⊆ wss 3887  ∅c0 4256  𝒫 cpw 4533  {csn 4561  ⟨cop 4567  ∪ cuni 4839   class class class wbr 5074   ↦ cmpt 5157   ↾ cres 5591   Fn wfn 6428  ⟶wf 6429  ‘cfv 6433  (class class class)co 7275   ∈ cmpo 7277  Xcixp 8685  Fincfn 8733  ∏_tcpt 17149  Topctop 22042  TopOnctopon 22059  Compccmp 22537   ×_t ctx 22711  Homeochmeo 22904   ≃ chmph 22905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-1o 8297  df-er 8498  df-map 8617  df-ixp 8686  df-en 8734  df-dom 8735  df-fin 8737  df-fi 9170  df-topgen 17154  df-pt 17155  df-top 22043  df-topon 22060  df-bases 22096  df-cn 22378  df-cnp 22379  df-cmp 22538  df-tx 22713  df-hmeo 22906  df-hmph 22907

This theorem is referenced by:  poimirlem30  35807