Theorem ptcmpfi 23874

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 6692	. . . . 5 ⊢ (𝐹:𝐴⟶Comp → 𝐹 Fn 𝐴)
2		fnresdm 6641	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
3	1, 2	syl 17	. . . 4 ⊢ (𝐹:𝐴⟶Comp → (𝐹 ↾ 𝐴) = 𝐹)
4	3	adantl 485	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (𝐹 ↾ 𝐴) = 𝐹)
5	4	fveq2d 6872	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) = (∏t‘𝐹))
6		ssid 3959	. . . 4 ⊢ 𝐴 ⊆ 𝐴
7		sseq1 3962	. . . . . 6 ⊢ (𝑥 = ∅ → (𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴))
8		reseq2 5961	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → (𝐹 ↾ 𝑥) = (𝐹 ↾ ∅))
9		res0 5970	. . . . . . . . . 10 ⊢ (𝐹 ↾ ∅) = ∅
10	8, 9	eqtrdi 2814	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝐹 ↾ 𝑥) = ∅)
11	10	fveq2d 6872	. . . . . . . 8 ⊢ (𝑥 = ∅ → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘∅))
12	11	eleq1d 2848	. . . . . . 7 ⊢ (𝑥 = ∅ → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔ (∏t‘∅) ∈ Comp))
13	12	imbi2d 342	. . . . . 6 ⊢ (𝑥 = ∅ → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘∅) ∈ Comp)))
14	7, 13	imbi12d 346	. . . . 5 ⊢ (𝑥 = ∅ → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ (∅ ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘∅) ∈ Comp))))
15		sseq1 3962	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴))
16		reseq2 5961	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐹 ↾ 𝑥) = (𝐹 ↾ 𝑦))
17	16	fveq2d 6872	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ 𝑦)))
18	17	eleq1d 2848	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔ (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp))
19	18	imbi2d 342	. . . . . 6 ⊢ (𝑥 = 𝑦 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)))
20	15, 19	imbi12d 346	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ (𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp))))
21		sseq1 3962	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥 ⊆ 𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴))
22		reseq2 5961	. . . . . . . . 9 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹 ↾ 𝑥) = (𝐹 ↾ (𝑦 ∪ {𝑧})))
23	22	fveq2d 6872	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))))
24	23	eleq1d 2848	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))
25	24	imbi2d 342	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
26	21, 25	imbi12d 346	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
27		sseq1 3962	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
28		reseq2 5961	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝐹 ↾ 𝑥) = (𝐹 ↾ 𝐴))
29	28	fveq2d 6872	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ 𝐴)))
30	29	eleq1d 2848	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔ (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp))
31	30	imbi2d 342	. . . . . 6 ⊢ (𝑥 = 𝐴 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp)))
32	27, 31	imbi12d 346	. . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ (𝐴 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp))))
33		0ex 5258	. . . . . . . . 9 ⊢ ∅ ∈ V
34		f0 6746	. . . . . . . . 9 ⊢ ∅:∅⟶Top
35		pttop 23643	. . . . . . . . 9 ⊢ ((∅ ∈ V ∧ ∅:∅⟶Top) → (∏t‘∅) ∈ Top)
36	33, 34, 35	mp2an 702	. . . . . . . 8 ⊢ (∏t‘∅) ∈ Top
37		eqid 2763	. . . . . . . . . . . . 13 ⊢ (∏t‘∅) = (∏t‘∅)
38	37	ptuni 23655	. . . . . . . . . . . 12 ⊢ ((∅ ∈ V ∧ ∅:∅⟶Top) → X𝑥 ∈ ∅ ∪ (∅‘𝑥) = ∪ (∏t‘∅))
39	33, 34, 38	mp2an 702	. . . . . . . . . . 11 ⊢ X𝑥 ∈ ∅ ∪ (∅‘𝑥) = ∪ (∏t‘∅)
40		ixp0x 8909	. . . . . . . . . . . 12 ⊢ X𝑥 ∈ ∅ ∪ (∅‘𝑥) = {∅}
41		snfi 9025	. . . . . . . . . . . 12 ⊢ {∅} ∈ Fin
42	40, 41	eqeltri 2859	. . . . . . . . . . 11 ⊢ X𝑥 ∈ ∅ ∪ (∅‘𝑥) ∈ Fin
43	39, 42	eqeltrri 2860	. . . . . . . . . 10 ⊢ ∪ (∏t‘∅) ∈ Fin
44		pwfi 9264	. . . . . . . . . 10 ⊢ (∪ (∏t‘∅) ∈ Fin ↔ 𝒫 ∪ (∏t‘∅) ∈ Fin)
45	43, 44	mpbi 232	. . . . . . . . 9 ⊢ 𝒫 ∪ (∏t‘∅) ∈ Fin
46		pwuni 4905	. . . . . . . . 9 ⊢ (∏t‘∅) ⊆ 𝒫 ∪ (∏t‘∅)
47		ssfi 9142	. . . . . . . . 9 ⊢ ((𝒫 ∪ (∏t‘∅) ∈ Fin ∧ (∏t‘∅) ⊆ 𝒫 ∪ (∏t‘∅)) → (∏t‘∅) ∈ Fin)
48	45, 46, 47	mp2an 702	. . . . . . . 8 ⊢ (∏t‘∅) ∈ Fin
49	36, 48	elini 4152	. . . . . . 7 ⊢ (∏t‘∅) ∈ (Top ∩ Fin)
50		fincmp 23454	. . . . . . 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 4131	. . . . . . . . 9 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
54		id 22	. . . . . . . . 9 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
55	53, 54	sstrid 3948	. . . . . . . 8 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → 𝑦 ⊆ 𝐴)
56	55	imim1i 63	. . . . . . 7 ⊢ ((𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)))
57		eqid 2763	. . . . . . . . . . . . . 14 ⊢ ∪ (∏t‘(𝐹 ↾ 𝑦)) = ∪ (∏t‘(𝐹 ↾ 𝑦))
58		eqid 2763	. . . . . . . . . . . . . 14 ⊢ ∪ (∏t‘(𝐹 ↾ {𝑧})) = ∪ (∏t‘(𝐹 ↾ {𝑧}))
59		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) = (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))
60		resabs1 5993	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦) = (𝐹 ↾ 𝑦))
61	53, 60	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦) = (𝐹 ↾ 𝑦)
62	61	eqcomi 2772	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ↾ 𝑦) = ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦)
63	62	fveq2i 6871	. . . . . . . . . . . . . 14 ⊢ (∏t‘(𝐹 ↾ 𝑦)) = (∏t‘((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦))
64		ssun2 4132	. . . . . . . . . . . . . . . . 17 ⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧})
65		resabs1 5993	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧} ⊆ (𝑦 ∪ {𝑧}) → ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}) = (𝐹 ↾ {𝑧}))
66	64, 65	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}) = (𝐹 ↾ {𝑧})
67	66	eqcomi 2772	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ↾ {𝑧}) = ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧})
68	67	fveq2i 6871	. . . . . . . . . . . . . 14 ⊢ (∏t‘(𝐹 ↾ {𝑧})) = (∏t‘((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}))
69		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪ (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣)) = (𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪ (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣))
70		vex 3459	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
71		vsnex 5393	. . . . . . . . . . . . . . . 16 ⊢ {𝑧} ∈ V
72	70, 71	unex 7728	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∪ {𝑧}) ∈ V
73	72	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) ∈ V)
74		simplr 778	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹:𝐴⟶Comp)
75		cmptop 23456	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Comp → 𝑥 ∈ Top)
76	75	ssriv 3941	. . . . . . . . . . . . . . . 16 ⊢ Comp ⊆ Top
77		fss 6709	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴⟶Comp ∧ Comp ⊆ Top) → 𝐹:𝐴⟶Top)
78	74, 76, 77	sylancl 595	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹:𝐴⟶Top)
79		simprr 782	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
80	78, 79	fssresd 6732	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹 ↾ (𝑦 ∪ {𝑧})):(𝑦 ∪ {𝑧})⟶Top)
81		eqidd 2764	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) = (𝑦 ∪ {𝑧}))
82		simprl 780	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ¬ 𝑧 ∈ 𝑦)
83		disjsn 4671	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦)
84	82, 83	sylibr 236	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∩ {𝑧}) = ∅)
85	57, 58, 59, 63, 68, 69, 73, 80, 81, 84	ptunhmeo 23869	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪ (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣)) ∈ (((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧})))Homeo(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))))
86		hmphi 23838	. . . . . . . . . . . . 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 737	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹 Fn 𝐴)
89	64, 79	sstrid 3948	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → {𝑧} ⊆ 𝐴)
90		vex 3459	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑧 ∈ V
91	90	snss 4744	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴)
92	89, 91	sylibr 236	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ 𝐴)
93		fnressn 7142	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝐹 ↾ {𝑧}) = {⟨𝑧, (𝐹‘𝑧)⟩})
94	88, 92, 93	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹 ↾ {𝑧}) = {⟨𝑧, (𝐹‘𝑧)⟩})
95	94	fveq2d 6872	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘(𝐹 ↾ {𝑧})) = (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}))
96		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) = (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩})
97	90	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ V)
98	74, 92	ffvelcdmd 7067	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ Comp)
99	76, 98	sselid 3935	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ Top)
100		toptopon2 22979	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑧) ∈ Top ↔ (𝐹‘𝑧) ∈ (TopOn‘∪ (𝐹‘𝑧)))
101	99, 100	sylib 220	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ (TopOn‘∪ (𝐹‘𝑧)))
102	96, 97, 101	pt1hmeo 23867	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑥 ∈ ∪ (𝐹‘𝑧) ↦ {⟨𝑧, 𝑥⟩}) ∈ ((𝐹‘𝑧)Homeo(∏t‘{⟨𝑧, (𝐹‘𝑧)⟩})))
103		hmphi 23838	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ∪ (𝐹‘𝑧) ↦ {⟨𝑧, 𝑥⟩}) ∈ ((𝐹‘𝑧)Homeo(∏t‘{⟨𝑧, (𝐹‘𝑧)⟩})) → (𝐹‘𝑧) ≃ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}))
104	102, 103	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ≃ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}))
105		cmphmph 23849	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑧) ≃ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) → ((𝐹‘𝑧) ∈ Comp → (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) ∈ Comp))
106	104, 98, 105	sylc 65	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) ∈ Comp)
107	95, 106	eqeltrd 2863	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘(𝐹 ↾ {𝑧})) ∈ Comp)
108		txcmp 23704	. . . . . . . . . . . . . 14 ⊢ (((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp ∧ (∏t‘(𝐹 ↾ {𝑧})) ∈ Comp) → ((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp)
109	108	expcom 417	. . . . . . . . . . . . 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 23849	. . . . . . . . . . . 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 417	. . . . . . . . . 10 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → ((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
114	113	a2d 29	. . . . . . . . 9 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
115	114	ex 416	. . . . . . . 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 485	. . . . 5 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
119	14, 20, 26, 32, 52, 118	findcard2s 9135	. . . 4 ⊢ (𝐴 ∈ Fin → (𝐴 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp)))
120	6, 119	mpi 20	. . 3 ⊢ (𝐴 ∈ Fin → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp))
121	120	anabsi5 679	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp)
122	5, 121	eqeltrrd 2864	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘𝐹) ∈ Comp)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1561   ∈ wcel 2143  Vcvv 3455   ∪ cun 3903   ∩ cin 3904   ⊆ wss 3905  ∅c0 4286  𝒫 cpw 4556  {csn 4583  ⟨cop 4589  ∪ cuni 4866   class class class wbr 5101   ↦ cmpt 5182   ↾ cres 5650   Fn wfn 6517  ⟶wf 6518  ‘cfv 6522  (class class class)co 7397   ∈ cmpo 7399  Xcixp 8880  Fincfn 8928  ∏_tcpt 17468  Topctop 22954  TopOnctopon 22971  Compccmp 23447   ×_t ctx 23621  Homeochmeo 23814   ≃ chmph 23815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5228  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7719

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-br 5102  df-opab 5164  df-mpt 5183  df-tr 5209  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-ord 6350  df-on 6351  df-lim 6352  df-suc 6353  df-iota 6478  df-fun 6524  df-fn 6525  df-f 6526  df-f1 6527  df-fo 6528  df-f1o 6529  df-fv 6530  df-ov 7400  df-oprab 7401  df-mpo 7402  df-om 7848  df-1st 7971  df-2nd 7972  df-1o 8438  df-2o 8439  df-map 8811  df-ixp 8881  df-en 8929  df-dom 8930  df-fin 8932  df-fi 9358  df-topgen 17473  df-pt 17474  df-top 22955  df-topon 22972  df-bases 23007  df-cn 23288  df-cnp 23289  df-cmp 23448  df-tx 23623  df-hmeo 23816  df-hmph 23817

This theorem is referenced by:  poimirlem30  38150