Theorem ptcmpfi 23939

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 6706	. . . . 5 ⊢ (𝐹:𝐴⟶Comp → 𝐹 Fn 𝐴)
2		fnresdm 6655	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)
3	1, 2	syl 18	. . . 4 ⊢ (𝐹:𝐴⟶Comp → (𝐹 ↾ 𝐴) = 𝐹)
4	3	adantl 486	. . 3 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (𝐹 ↾ 𝐴) = 𝐹)
5	4	fveq2d 6886	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) = (∏t‘𝐹))
6		ssid 3967	. . . 4 ⊢ 𝐴 ⊆ 𝐴
7		sseq1 3970	. . . . . 6 ⊢ (𝑥 = ∅ → (𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴))
8		reseq2 5974	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → (𝐹 ↾ 𝑥) = (𝐹 ↾ ∅))
9		res0 5983	. . . . . . . . . 10 ⊢ (𝐹 ↾ ∅) = ∅
10	8, 9	eqtrdi 2820	. . . . . . . . 9 ⊢ (𝑥 = ∅ → (𝐹 ↾ 𝑥) = ∅)
11	10	fveq2d 6886	. . . . . . . 8 ⊢ (𝑥 = ∅ → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘∅))
12	11	eleq1d 2854	. . . . . . 7 ⊢ (𝑥 = ∅ → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔ (∏t‘∅) ∈ Comp))
13	12	imbi2d 343	. . . . . 6 ⊢ (𝑥 = ∅ → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘∅) ∈ Comp)))
14	7, 13	imbi12d 347	. . . . 5 ⊢ (𝑥 = ∅ → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ (∅ ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘∅) ∈ Comp))))
15		sseq1 3970	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴))
16		reseq2 5974	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝐹 ↾ 𝑥) = (𝐹 ↾ 𝑦))
17	16	fveq2d 6886	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ 𝑦)))
18	17	eleq1d 2854	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔ (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp))
19	18	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 𝑦 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)))
20	15, 19	imbi12d 347	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ (𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp))))
21		sseq1 3970	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥 ⊆ 𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴))
22		reseq2 5974	. . . . . . . . 9 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹 ↾ 𝑥) = (𝐹 ↾ (𝑦 ∪ {𝑧})))
23	22	fveq2d 6886	. . . . . . . 8 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))))
24	23	eleq1d 2854	. . . . . . 7 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))
25	24	imbi2d 343	. . . . . 6 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
26	21, 25	imbi12d 347	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
27		sseq1 3970	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
28		reseq2 5974	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝐹 ↾ 𝑥) = (𝐹 ↾ 𝐴))
29	28	fveq2d 6886	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (∏t‘(𝐹 ↾ 𝑥)) = (∏t‘(𝐹 ↾ 𝐴)))
30	29	eleq1d 2854	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ((∏t‘(𝐹 ↾ 𝑥)) ∈ Comp ↔ (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp))
31	30	imbi2d 343	. . . . . 6 ⊢ (𝑥 = 𝐴 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp)))
32	27, 31	imbi12d 347	. . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑥 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑥)) ∈ Comp)) ↔ (𝐴 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp))))
33		0ex 5272	. . . . . . . . 9 ⊢ ∅ ∈ V
34		f0 6760	. . . . . . . . 9 ⊢ ∅:∅⟶Top
35		pttop 23708	. . . . . . . . 9 ⊢ ((∅ ∈ V ∧ ∅:∅⟶Top) → (∏t‘∅) ∈ Top)
36	33, 34, 35	mp2an 704	. . . . . . . 8 ⊢ (∏t‘∅) ∈ Top
37		eqid 2769	. . . . . . . . . . . . 13 ⊢ (∏t‘∅) = (∏t‘∅)
38	37	ptuni 23720	. . . . . . . . . . . 12 ⊢ ((∅ ∈ V ∧ ∅:∅⟶Top) → X𝑥 ∈ ∅ ∪ (∅‘𝑥) = ∪ (∏t‘∅))
39	33, 34, 38	mp2an 704	. . . . . . . . . . 11 ⊢ X𝑥 ∈ ∅ ∪ (∅‘𝑥) = ∪ (∏t‘∅)
40		ixp0x 8924	. . . . . . . . . . . 12 ⊢ X𝑥 ∈ ∅ ∪ (∅‘𝑥) = {∅}
41		snfi 9040	. . . . . . . . . . . 12 ⊢ {∅} ∈ Fin
42	40, 41	eqeltri 2865	. . . . . . . . . . 11 ⊢ X𝑥 ∈ ∅ ∪ (∅‘𝑥) ∈ Fin
43	39, 42	eqeltrri 2866	. . . . . . . . . 10 ⊢ ∪ (∏t‘∅) ∈ Fin
44		pwfi 9278	. . . . . . . . . 10 ⊢ (∪ (∏t‘∅) ∈ Fin ↔ 𝒫 ∪ (∏t‘∅) ∈ Fin)
45	43, 44	mpbi 233	. . . . . . . . 9 ⊢ 𝒫 ∪ (∏t‘∅) ∈ Fin
46		pwuni 4915	. . . . . . . . 9 ⊢ (∏t‘∅) ⊆ 𝒫 ∪ (∏t‘∅)
47		ssfi 9157	. . . . . . . . 9 ⊢ ((𝒫 ∪ (∏t‘∅) ∈ Fin ∧ (∏t‘∅) ⊆ 𝒫 ∪ (∏t‘∅)) → (∏t‘∅) ∈ Fin)
48	45, 46, 47	mp2an 704	. . . . . . . 8 ⊢ (∏t‘∅) ∈ Fin
49	36, 48	elini 4160	. . . . . . 7 ⊢ (∏t‘∅) ∈ (Top ∩ Fin)
50		fincmp 23519	. . . . . . 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 4139	. . . . . . . . 9 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
54		id 23	. . . . . . . . 9 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
55	53, 54	sstrid 3956	. . . . . . . 8 ⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → 𝑦 ⊆ 𝐴)
56	55	imim1i 64	. . . . . . 7 ⊢ ((𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)))
57		eqid 2769	. . . . . . . . . . . . . 14 ⊢ ∪ (∏t‘(𝐹 ↾ 𝑦)) = ∪ (∏t‘(𝐹 ↾ 𝑦))
58		eqid 2769	. . . . . . . . . . . . . 14 ⊢ ∪ (∏t‘(𝐹 ↾ {𝑧})) = ∪ (∏t‘(𝐹 ↾ {𝑧}))
59		eqid 2769	. . . . . . . . . . . . . 14 ⊢ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) = (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))
60		resabs1 6006	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦) = (𝐹 ↾ 𝑦))
61	53, 60	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦) = (𝐹 ↾ 𝑦)
62	61	eqcomi 2778	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ↾ 𝑦) = ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦)
63	62	fveq2i 6885	. . . . . . . . . . . . . 14 ⊢ (∏t‘(𝐹 ↾ 𝑦)) = (∏t‘((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦))
64		ssun2 4140	. . . . . . . . . . . . . . . . 17 ⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧})
65		resabs1 6006	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧} ⊆ (𝑦 ∪ {𝑧}) → ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}) = (𝐹 ↾ {𝑧}))
66	64, 65	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}) = (𝐹 ↾ {𝑧})
67	66	eqcomi 2778	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ↾ {𝑧}) = ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧})
68	67	fveq2i 6885	. . . . . . . . . . . . . 14 ⊢ (∏t‘(𝐹 ↾ {𝑧})) = (∏t‘((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}))
69		eqid 2769	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪ (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣)) = (𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪ (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣))
70		vex 3467	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
71		vsnex 5407	. . . . . . . . . . . . . . . 16 ⊢ {𝑧} ∈ V
72	70, 71	unex 7743	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∪ {𝑧}) ∈ V
73	72	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) ∈ V)
74		simplr 780	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹:𝐴⟶Comp)
75		cmptop 23521	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ Comp → 𝑥 ∈ Top)
76	75	ssriv 3949	. . . . . . . . . . . . . . . 16 ⊢ Comp ⊆ Top
77		fss 6723	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴⟶Comp ∧ Comp ⊆ Top) → 𝐹:𝐴⟶Top)
78	74, 76, 77	sylancl 597	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹:𝐴⟶Top)
79		simprr 784	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
80	78, 79	fssresd 6746	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹 ↾ (𝑦 ∪ {𝑧})):(𝑦 ∪ {𝑧})⟶Top)
81		eqidd 2770	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) = (𝑦 ∪ {𝑧}))
82		simprl 782	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ¬ 𝑧 ∈ 𝑦)
83		disjsn 4682	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦)
84	82, 83	sylibr 237	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∩ {𝑧}) = ∅)
85	57, 58, 59, 63, 68, 69, 73, 80, 81, 84	ptunhmeo 23934	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪ (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣)) ∈ (((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧})))Homeo(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))))
86		hmphi 23903	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ ∪ (∏t‘(𝐹 ↾ 𝑦)), 𝑣 ∈ ∪ (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢 ∪ 𝑣)) ∈ (((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧})))Homeo(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))) → ((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ≃ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))))
87	85, 86	syl 18	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ≃ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))))
88	1	ad2antlr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹 Fn 𝐴)
89	64, 79	sstrid 3956	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → {𝑧} ⊆ 𝐴)
90		vex 3467	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑧 ∈ V
91	90	snss 4755	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝐴 ↔ {𝑧} ⊆ 𝐴)
92	89, 91	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ 𝐴)
93		fnressn 7156	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑧 ∈ 𝐴) → (𝐹 ↾ {𝑧}) = {⟨𝑧, (𝐹‘𝑧)⟩})
94	88, 92, 93	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹 ↾ {𝑧}) = {⟨𝑧, (𝐹‘𝑧)⟩})
95	94	fveq2d 6886	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘(𝐹 ↾ {𝑧})) = (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}))
96		eqid 2769	. . . . . . . . . . . . . . . . 17 ⊢ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) = (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩})
97	90	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ V)
98	74, 92	ffvelcdmd 7081	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ Comp)
99	76, 98	sselid 3943	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ Top)
100		toptopon2 23044	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑧) ∈ Top ↔ (𝐹‘𝑧) ∈ (TopOn‘∪ (𝐹‘𝑧)))
101	99, 100	sylib 221	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ∈ (TopOn‘∪ (𝐹‘𝑧)))
102	96, 97, 101	pt1hmeo 23932	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑥 ∈ ∪ (𝐹‘𝑧) ↦ {⟨𝑧, 𝑥⟩}) ∈ ((𝐹‘𝑧)Homeo(∏t‘{⟨𝑧, (𝐹‘𝑧)⟩})))
103		hmphi 23903	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ∪ (𝐹‘𝑧) ↦ {⟨𝑧, 𝑥⟩}) ∈ ((𝐹‘𝑧)Homeo(∏t‘{⟨𝑧, (𝐹‘𝑧)⟩})) → (𝐹‘𝑧) ≃ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}))
104	102, 103	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹‘𝑧) ≃ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}))
105		cmphmph 23914	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑧) ≃ (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) → ((𝐹‘𝑧) ∈ Comp → (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) ∈ Comp))
106	104, 98, 105	sylc 66	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘{⟨𝑧, (𝐹‘𝑧)⟩}) ∈ Comp)
107	95, 106	eqeltrd 2869	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘(𝐹 ↾ {𝑧})) ∈ Comp)
108		txcmp 23769	. . . . . . . . . . . . . 14 ⊢ (((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp ∧ (∏t‘(𝐹 ↾ {𝑧})) ∈ Comp) → ((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp)
109	108	expcom 418	. . . . . . . . . . . . 13 ⊢ ((∏t‘(𝐹 ↾ {𝑧})) ∈ Comp → ((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp → ((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp))
110	107, 109	syl 18	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp → ((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp))
111		cmphmph 23914	. . . . . . . . . . . 12 ⊢ (((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ≃ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) → (((∏t‘(𝐹 ↾ 𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))
112	87, 110, 111	sylsyld 62	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))
113	112	expcom 418	. . . . . . . . . 10 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → ((∏t‘(𝐹 ↾ 𝑦)) ∈ Comp → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
114	113	a2d 30	. . . . . . . . 9 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
115	114	ex 417	. . . . . . . 8 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
116	115	a2d 30	. . . . . . 7 ⊢ (¬ 𝑧 ∈ 𝑦 → (((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
117	56, 116	syl5 35	. . . . . 6 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
118	117	adantl 486	. . . . 5 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑦 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
119	14, 20, 26, 32, 52, 118	findcard2s 9150	. . . 4 ⊢ (𝐴 ∈ Fin → (𝐴 ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp)))
120	6, 119	mpi 21	. . 3 ⊢ (𝐴 ∈ Fin → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp))
121	120	anabsi5 681	. 2 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Comp)
122	5, 121	eqeltrrd 2870	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘𝐹) ∈ Comp)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  Vcvv 3463   ∪ cun 3911   ∩ cin 3912   ⊆ wss 3913  ∅c0 4294  𝒫 cpw 4567  {csn 4594  ⟨cop 4600  ∪ cuni 4876   class class class wbr 5113   ↦ cmpt 5196   ↾ cres 5664   Fn wfn 6532  ⟶wf 6533  ‘cfv 6537  (class class class)co 7411   ∈ cmpo 7413  Xcixp 8895  Fincfn 8943  ∏_tcpt 17491  Topctop 23019  TopOnctopon 23036  Compccmp 23512   ×_t ctx 23686  Homeochmeo 23879   ≃ chmph 23880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-int 4917  df-iun 4962  df-iin 4963  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7863  df-1st 7986  df-2nd 7987  df-1o 8453  df-2o 8454  df-map 8826  df-ixp 8896  df-en 8944  df-dom 8945  df-fin 8947  df-fi 9371  df-topgen 17496  df-pt 17497  df-top 23020  df-topon 23037  df-bases 23072  df-cn 23353  df-cnp 23354  df-cmp 23513  df-tx 23688  df-hmeo 23881  df-hmph 23882

This theorem is referenced by:  poimirlem30  38223