Theorem ptcmpfi 23698

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 6652	. . . . 5 ⊢ (𝐹:𝐴⟶Comp → 𝐹 Fn 𝐴)
2		fnresdm 6601	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
3	1, 2	syl 17	. . . 4 ⊢ (𝐹:𝐴⟶Comp → (𝐹 ↾ 𝐴) = 𝐹)
4	3	adantl 481	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (𝐹 ↾ 𝐴) = 𝐹)
5	4	fveq2d 6826	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) = (∏t‘𝐹))
6		ssid 3958	. . . 4 ⊢ 𝐴 ⊆ 𝐴
7		sseq1 3961	. . . . . 6 ⊢ (𝑥 = ∅ → (𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴))
8		reseq2 5925	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → (𝐹 ↾ 𝑥) = (𝐹 ↾ ∅))
9		res0 5934	. . . . . . . . . 10 ⊢ (𝐹 ↾ ∅) = ∅
10	8, 9	eqtrdi 2780	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝐹 ↾ 𝑥) = ∅)
11	10	fveq2d 6826	. . . . . . . 8 ⊢ (𝑥 = ∅ → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘∅))
12	11	eleq1d 2813	. . . . . . 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 3961	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴))
16		reseq2 5925	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐹 ↾ 𝑥) = (𝐹 ↾ 𝑦))
17	16	fveq2d 6826	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ 𝑦)))
18	17	eleq1d 2813	. . . . . . 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 3961	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥 ⊆ 𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴))
22		reseq2 5925	. . . . . . . . 9 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹 ↾ 𝑥) = (𝐹 ↾ (𝑦 ∪ {𝑧})))
23	22	fveq2d 6826	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))))
24	23	eleq1d 2813	. . . . . . 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 3961	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
28		reseq2 5925	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝐹 ↾ 𝑥) = (𝐹 ↾ 𝐴))
29	28	fveq2d 6826	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ 𝐴)))
30	29	eleq1d 2813	. . . . . . 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 5246	. . . . . . . . 9 ⊢ ∅ ∈ V
34		f0 6705	. . . . . . . . 9 ⊢ ∅:∅⟶Top
35		pttop 23467	. . . . . . . . 9 ⊢ ((∅ ∈ V ∧ ∅:∅⟶Top) → (∏t‘∅) ∈ Top)
36	33, 34, 35	mp2an 692	. . . . . . . 8 ⊢ (∏t‘∅) ∈ Top
37		eqid 2729	. . . . . . . . . . . . 13 ⊢ (∏t‘∅) = (∏t‘∅)
38	37	ptuni 23479	. . . . . . . . . . . 12 ⊢ ((∅ ∈ V ∧ ∅:∅⟶Top) → X𝑥 ∈ ∅ ∪ (∅‘𝑥) = ∪ (∏t‘∅))
39	33, 34, 38	mp2an 692	. . . . . . . . . . 11 ⊢ X𝑥 ∈ ∅ ∪ (∅‘𝑥) = ∪ (∏t‘∅)
40		ixp0x 8853	. . . . . . . . . . . 12 ⊢ X𝑥 ∈ ∅ ∪ (∅‘𝑥) = {∅}
41		snfi 8968	. . . . . . . . . . . 12 ⊢ {∅} ∈ Fin
42	40, 41	eqeltri 2824	. . . . . . . . . . 11 ⊢ X𝑥 ∈ ∅ ∪ (∅‘𝑥) ∈ Fin
43	39, 42	eqeltrri 2825	. . . . . . . . . 10 ⊢ ∪ (∏t‘∅) ∈ Fin
44		pwfi 9208	. . . . . . . . . 10 ⊢ (∪ (∏t‘∅) ∈ Fin ↔ 𝒫 ∪ (∏t‘∅) ∈ Fin)
45	43, 44	mpbi 230	. . . . . . . . 9 ⊢ 𝒫 ∪ (∏t‘∅) ∈ Fin
46		pwuni 4895	. . . . . . . . 9 ⊢ (∏t‘∅) ⊆ 𝒫 ∪ (∏t‘∅)
47		ssfi 9087	. . . . . . . . 9 ⊢ ((𝒫 ∪ (∏t‘∅) ∈ Fin ∧ (∏t‘∅) ⊆ 𝒫 ∪ (∏t‘∅)) → (∏t‘∅) ∈ Fin)
48	45, 46, 47	mp2an 692	. . . . . . . 8 ⊢ (∏t‘∅) ∈ Fin
49	36, 48	elini 4150	. . . . . . 7 ⊢ (∏t‘∅) ∈ (Top ∩ Fin)
50		fincmp 23278	. . . . . . 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 4129	. . . . . . . . 9 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
54		id 22	. . . . . . . . 9 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
55	53, 54	sstrid 3947	. . . . . . . 8 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → 𝑦 ⊆ 𝐴)
56	55	imim1i 63	. . . . . . 7 ⊢ ((𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)))
57		eqid 2729	. . . . . . . . . . . . . 14 ⊢ ∪ (∏t‘(𝐹 ↾ 𝑦)) = ∪ (∏t‘(𝐹 ↾ 𝑦))
58		eqid 2729	. . . . . . . . . . . . . 14 ⊢ ∪ (∏t‘(𝐹 ↾ {𝑧})) = ∪ (∏t‘(𝐹 ↾ {𝑧}))
59		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) = (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))
60		resabs1 5957	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦) = (𝐹 ↾ 𝑦))
61	53, 60	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦) = (𝐹 ↾ 𝑦)
62	61	eqcomi 2738	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ↾ 𝑦) = ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦)
63	62	fveq2i 6825	. . . . . . . . . . . . . 14 ⊢ (∏t‘(𝐹 ↾ 𝑦)) = (∏t‘((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦))
64		ssun2 4130	. . . . . . . . . . . . . . . . 17 ⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧})
65		resabs1 5957	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧} ⊆ (𝑦 ∪ {𝑧}) → ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}) = (𝐹 ↾ {𝑧}))
66	64, 65	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}) = (𝐹 ↾ {𝑧})
67	66	eqcomi 2738	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ↾ {𝑧}) = ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧})
68	67	fveq2i 6825	. . . . . . . . . . . . . 14 ⊢ (∏t‘(𝐹 ↾ {𝑧})) = (∏t‘((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}))
69		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪ (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣)) = (𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪ (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣))
70		vex 3440	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
71		vsnex 5373	. . . . . . . . . . . . . . . 16 ⊢ {𝑧} ∈ V
72	70, 71	unex 7680	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∪ {𝑧}) ∈ V
73	72	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) ∈ V)
74		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹:𝐴⟶Comp)
75		cmptop 23280	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Comp → 𝑥 ∈ Top)
76	75	ssriv 3939	. . . . . . . . . . . . . . . 16 ⊢ Comp ⊆ Top
77		fss 6668	. . . . . . . . . . . . . . . 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 6691	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹 ↾ (𝑦 ∪ {𝑧})):(𝑦 ∪ {𝑧})⟶Top)
81		eqidd 2730	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) = (𝑦 ∪ {𝑧}))
82		simprl 770	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ¬ 𝑧 ∈ 𝑦)
83		disjsn 4663	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦)
84	82, 83	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∩ {𝑧}) = ∅)
85	57, 58, 59, 63, 68, 69, 73, 80, 81, 84	ptunhmeo 23693	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪ (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣)) ∈ (((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧})))Homeo(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))))
86		hmphi 23662	. . . . . . . . . . . . 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 3947	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → {𝑧} ⊆ 𝐴)
90		vex 3440	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑧 ∈ V
91	90	snss 4736	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴)
92	89, 91	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ 𝐴)
93		fnressn 7092	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝐹 ↾ {𝑧}) = {⟨𝑧, (𝐹‘𝑧)⟩})
94	88, 92, 93	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹 ↾ {𝑧}) = {⟨𝑧, (𝐹‘𝑧)⟩})
95	94	fveq2d 6826	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘(𝐹 ↾ {𝑧})) = (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}))
96		eqid 2729	. . . . . . . . . . . . . . . . 17 ⊢ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) = (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩})
97	90	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ V)
98	74, 92	ffvelcdmd 7019	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ Comp)
99	76, 98	sselid 3933	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ Top)
100		toptopon2 22803	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑧) ∈ Top ↔ (𝐹‘𝑧) ∈ (TopOn‘∪ (𝐹‘𝑧)))
101	99, 100	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ (TopOn‘∪ (𝐹‘𝑧)))
102	96, 97, 101	pt1hmeo 23691	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑥 ∈ ∪ (𝐹‘𝑧) ↦ {⟨𝑧, 𝑥⟩}) ∈ ((𝐹‘𝑧)Homeo(∏t‘{⟨𝑧, (𝐹‘𝑧)⟩})))
103		hmphi 23662	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ∪ (𝐹‘𝑧) ↦ {⟨𝑧, 𝑥⟩}) ∈ ((𝐹‘𝑧)Homeo(∏t‘{⟨𝑧, (𝐹‘𝑧)⟩})) → (𝐹‘𝑧) ≃ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}))
104	102, 103	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ≃ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}))
105		cmphmph 23673	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑧) ≃ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) → ((𝐹‘𝑧) ∈ Comp → (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) ∈ Comp))
106	104, 98, 105	sylc 65	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) ∈ Comp)
107	95, 106	eqeltrd 2828	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘(𝐹 ↾ {𝑧})) ∈ Comp)
108		txcmp 23528	. . . . . . . . . . . . . 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 23673	. . . . . . . . . . . 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 9079	. . . 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 2829	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘𝐹) ∈ Comp)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3436   ∪ cun 3901   ∩ cin 3902   ⊆ wss 3903  ∅c0 4284  𝒫 cpw 4551  {csn 4577  ⟨cop 4583  ∪ cuni 4858   class class class wbr 5092   ↦ cmpt 5173   ↾ cres 5621   Fn wfn 6477  ⟶wf 6478  ‘cfv 6482  (class class class)co 7349   ∈ cmpo 7351  Xcixp 8824  Fincfn 8872  ∏_tcpt 17342  Topctop 22778  TopOnctopon 22795  Compccmp 23271   ×_t ctx 23445  Homeochmeo 23638   ≃ chmph 23639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-int 4897  df-iun 4943  df-iin 4944  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-1o 8388  df-2o 8389  df-map 8755  df-ixp 8825  df-en 8873  df-dom 8874  df-fin 8876  df-fi 9301  df-topgen 17347  df-pt 17348  df-top 22779  df-topon 22796  df-bases 22831  df-cn 23112  df-cnp 23113  df-cmp 23272  df-tx 23447  df-hmeo 23640  df-hmph 23641

This theorem is referenced by:  poimirlem30  37640