Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ptcmpfi Structured version   Visualization version   GIF version

Theorem ptcmpfi 22528
 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.
StepHypRef Expression
1 ffn 6504 . . . . 5 (𝐹:𝐴⟶Comp → 𝐹 Fn 𝐴)
2 fnresdm 6455 . . . . 5 (𝐹 Fn 𝐴 → (𝐹𝐴) = 𝐹)
31, 2syl 17 . . . 4 (𝐹:𝐴⟶Comp → (𝐹𝐴) = 𝐹)
43adantl 485 . . 3 ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (𝐹𝐴) = 𝐹)
54fveq2d 6668 . 2 ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝐴)) = (∏t𝐹))
6 ssid 3917 . . . 4 𝐴𝐴
7 sseq1 3920 . . . . . 6 (𝑥 = ∅ → (𝑥𝐴 ↔ ∅ ⊆ 𝐴))
8 reseq2 5824 . . . . . . . . . 10 (𝑥 = ∅ → (𝐹𝑥) = (𝐹 ↾ ∅))
9 res0 5833 . . . . . . . . . 10 (𝐹 ↾ ∅) = ∅
108, 9eqtrdi 2810 . . . . . . . . 9 (𝑥 = ∅ → (𝐹𝑥) = ∅)
1110fveq2d 6668 . . . . . . . 8 (𝑥 = ∅ → (∏t‘(𝐹𝑥)) = (∏t‘∅))
1211eleq1d 2837 . . . . . . 7 (𝑥 = ∅ → ((∏t‘(𝐹𝑥)) ∈ Comp ↔ (∏t‘∅) ∈ Comp))
1312imbi2d 344 . . . . . 6 (𝑥 = ∅ → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘∅) ∈ Comp)))
147, 13imbi12d 348 . . . . 5 (𝑥 = ∅ → ((𝑥𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑥)) ∈ Comp)) ↔ (∅ ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘∅) ∈ Comp))))
15 sseq1 3920 . . . . . 6 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
16 reseq2 5824 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
1716fveq2d 6668 . . . . . . . 8 (𝑥 = 𝑦 → (∏t‘(𝐹𝑥)) = (∏t‘(𝐹𝑦)))
1817eleq1d 2837 . . . . . . 7 (𝑥 = 𝑦 → ((∏t‘(𝐹𝑥)) ∈ Comp ↔ (∏t‘(𝐹𝑦)) ∈ Comp))
1918imbi2d 344 . . . . . 6 (𝑥 = 𝑦 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp)))
2015, 19imbi12d 348 . . . . 5 (𝑥 = 𝑦 → ((𝑥𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑥)) ∈ Comp)) ↔ (𝑦𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp))))
21 sseq1 3920 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴))
22 reseq2 5824 . . . . . . . . 9 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹𝑥) = (𝐹 ↾ (𝑦 ∪ {𝑧})))
2322fveq2d 6668 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑧}) → (∏t‘(𝐹𝑥)) = (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))))
2423eleq1d 2837 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → ((∏t‘(𝐹𝑥)) ∈ Comp ↔ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))
2524imbi2d 344 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
2621, 25imbi12d 348 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑥𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑥)) ∈ Comp)) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
27 sseq1 3920 . . . . . 6 (𝑥 = 𝐴 → (𝑥𝐴𝐴𝐴))
28 reseq2 5824 . . . . . . . . 9 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
2928fveq2d 6668 . . . . . . . 8 (𝑥 = 𝐴 → (∏t‘(𝐹𝑥)) = (∏t‘(𝐹𝐴)))
3029eleq1d 2837 . . . . . . 7 (𝑥 = 𝐴 → ((∏t‘(𝐹𝑥)) ∈ Comp ↔ (∏t‘(𝐹𝐴)) ∈ Comp))
3130imbi2d 344 . . . . . 6 (𝑥 = 𝐴 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝐴)) ∈ Comp)))
3227, 31imbi12d 348 . . . . 5 (𝑥 = 𝐴 → ((𝑥𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑥)) ∈ Comp)) ↔ (𝐴𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝐴)) ∈ Comp))))
33 0ex 5182 . . . . . . . . 9 ∅ ∈ V
34 f0 6551 . . . . . . . . 9 ∅:∅⟶Top
35 pttop 22297 . . . . . . . . 9 ((∅ ∈ V ∧ ∅:∅⟶Top) → (∏t‘∅) ∈ Top)
3633, 34, 35mp2an 691 . . . . . . . 8 (∏t‘∅) ∈ Top
37 eqid 2759 . . . . . . . . . . . . 13 (∏t‘∅) = (∏t‘∅)
3837ptuni 22309 . . . . . . . . . . . 12 ((∅ ∈ V ∧ ∅:∅⟶Top) → X𝑥 ∈ ∅ (∅‘𝑥) = (∏t‘∅))
3933, 34, 38mp2an 691 . . . . . . . . . . 11 X𝑥 ∈ ∅ (∅‘𝑥) = (∏t‘∅)
40 ixp0x 8522 . . . . . . . . . . . 12 X𝑥 ∈ ∅ (∅‘𝑥) = {∅}
41 snfi 8628 . . . . . . . . . . . 12 {∅} ∈ Fin
4240, 41eqeltri 2849 . . . . . . . . . . 11 X𝑥 ∈ ∅ (∅‘𝑥) ∈ Fin
4339, 42eqeltrri 2850 . . . . . . . . . 10 (∏t‘∅) ∈ Fin
44 pwfi 8760 . . . . . . . . . 10 ( (∏t‘∅) ∈ Fin ↔ 𝒫 (∏t‘∅) ∈ Fin)
4543, 44mpbi 233 . . . . . . . . 9 𝒫 (∏t‘∅) ∈ Fin
46 pwuni 4841 . . . . . . . . 9 (∏t‘∅) ⊆ 𝒫 (∏t‘∅)
47 ssfi 8756 . . . . . . . . 9 ((𝒫 (∏t‘∅) ∈ Fin ∧ (∏t‘∅) ⊆ 𝒫 (∏t‘∅)) → (∏t‘∅) ∈ Fin)
4845, 46, 47mp2an 691 . . . . . . . 8 (∏t‘∅) ∈ Fin
4936, 48elini 4101 . . . . . . 7 (∏t‘∅) ∈ (Top ∩ Fin)
50 fincmp 22108 . . . . . . 7 ((∏t‘∅) ∈ (Top ∩ Fin) → (∏t‘∅) ∈ Comp)
5149, 50ax-mp 5 . . . . . 6 (∏t‘∅) ∈ Comp
52512a1i 12 . . . . 5 (∅ ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘∅) ∈ Comp))
53 ssun1 4080 . . . . . . . . 9 𝑦 ⊆ (𝑦 ∪ {𝑧})
54 id 22 . . . . . . . . 9 ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
5553, 54sstrid 3906 . . . . . . . 8 ((𝑦 ∪ {𝑧}) ⊆ 𝐴𝑦𝐴)
5655imim1i 63 . . . . . . 7 ((𝑦𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp)))
57 eqid 2759 . . . . . . . . . . . . . 14 (∏t‘(𝐹𝑦)) = (∏t‘(𝐹𝑦))
58 eqid 2759 . . . . . . . . . . . . . 14 (∏t‘(𝐹 ↾ {𝑧})) = (∏t‘(𝐹 ↾ {𝑧}))
59 eqid 2759 . . . . . . . . . . . . . 14 (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) = (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))
60 resabs1 5859 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ (𝑦 ∪ {𝑧}) → ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦) = (𝐹𝑦))
6153, 60ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦) = (𝐹𝑦)
6261eqcomi 2768 . . . . . . . . . . . . . . 15 (𝐹𝑦) = ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦)
6362fveq2i 6667 . . . . . . . . . . . . . 14 (∏t‘(𝐹𝑦)) = (∏t‘((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦))
64 ssun2 4081 . . . . . . . . . . . . . . . . 17 {𝑧} ⊆ (𝑦 ∪ {𝑧})
65 resabs1 5859 . . . . . . . . . . . . . . . . 17 ({𝑧} ⊆ (𝑦 ∪ {𝑧}) → ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}) = (𝐹 ↾ {𝑧}))
6664, 65ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}) = (𝐹 ↾ {𝑧})
6766eqcomi 2768 . . . . . . . . . . . . . . 15 (𝐹 ↾ {𝑧}) = ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧})
6867fveq2i 6667 . . . . . . . . . . . . . 14 (∏t‘(𝐹 ↾ {𝑧})) = (∏t‘((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}))
69 eqid 2759 . . . . . . . . . . . . . 14 (𝑢 (∏t‘(𝐹𝑦)), 𝑣 (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢𝑣)) = (𝑢 (∏t‘(𝐹𝑦)), 𝑣 (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢𝑣))
70 vex 3414 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
71 snex 5305 . . . . . . . . . . . . . . . 16 {𝑧} ∈ V
7270, 71unex 7474 . . . . . . . . . . . . . . 15 (𝑦 ∪ {𝑧}) ∈ V
7372a1i 11 . . . . . . . . . . . . . 14 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) ∈ V)
74 simplr 768 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹:𝐴⟶Comp)
75 cmptop 22110 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ Comp → 𝑥 ∈ Top)
7675ssriv 3899 . . . . . . . . . . . . . . . 16 Comp ⊆ Top
77 fss 6518 . . . . . . . . . . . . . . . 16 ((𝐹:𝐴⟶Comp ∧ Comp ⊆ Top) → 𝐹:𝐴⟶Top)
7874, 76, 77sylancl 589 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹:𝐴⟶Top)
79 simprr 772 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
8078, 79fssresd 6536 . . . . . . . . . . . . . 14 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹 ↾ (𝑦 ∪ {𝑧})):(𝑦 ∪ {𝑧})⟶Top)
81 eqidd 2760 . . . . . . . . . . . . . 14 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) = (𝑦 ∪ {𝑧}))
82 simprl 770 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ¬ 𝑧𝑦)
83 disjsn 4608 . . . . . . . . . . . . . . 15 ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑦)
8482, 83sylibr 237 . . . . . . . . . . . . . 14 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∩ {𝑧}) = ∅)
8557, 58, 59, 63, 68, 69, 73, 80, 81, 84ptunhmeo 22523 . . . . . . . . . . . . 13 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑢 (∏t‘(𝐹𝑦)), 𝑣 (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢𝑣)) ∈ (((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧})))Homeo(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))))
86 hmphi 22492 . . . . . . . . . . . . 13 ((𝑢 (∏t‘(𝐹𝑦)), 𝑣 (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢𝑣)) ∈ (((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧})))Homeo(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))) → ((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ≃ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))))
8785, 86syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ≃ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))))
881ad2antlr 726 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹 Fn 𝐴)
8964, 79sstrid 3906 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → {𝑧} ⊆ 𝐴)
90 vex 3414 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ V
9190snss 4680 . . . . . . . . . . . . . . . . 17 (𝑧𝐴 ↔ {𝑧} ⊆ 𝐴)
9289, 91sylibr 237 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧𝐴)
93 fnressn 6918 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝐴𝑧𝐴) → (𝐹 ↾ {𝑧}) = {⟨𝑧, (𝐹𝑧)⟩})
9488, 92, 93syl2anc 587 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹 ↾ {𝑧}) = {⟨𝑧, (𝐹𝑧)⟩})
9594fveq2d 6668 . . . . . . . . . . . . . 14 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘(𝐹 ↾ {𝑧})) = (∏t‘{⟨𝑧, (𝐹𝑧)⟩}))
96 eqid 2759 . . . . . . . . . . . . . . . . 17 (∏t‘{⟨𝑧, (𝐹𝑧)⟩}) = (∏t‘{⟨𝑧, (𝐹𝑧)⟩})
9790a1i 11 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ V)
9874, 92ffvelrnd 6850 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹𝑧) ∈ Comp)
9976, 98sseldi 3893 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹𝑧) ∈ Top)
100 toptopon2 21633 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑧) ∈ Top ↔ (𝐹𝑧) ∈ (TopOn‘ (𝐹𝑧)))
10199, 100sylib 221 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹𝑧) ∈ (TopOn‘ (𝐹𝑧)))
10296, 97, 101pt1hmeo 22521 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑥 (𝐹𝑧) ↦ {⟨𝑧, 𝑥⟩}) ∈ ((𝐹𝑧)Homeo(∏t‘{⟨𝑧, (𝐹𝑧)⟩})))
103 hmphi 22492 . . . . . . . . . . . . . . . 16 ((𝑥 (𝐹𝑧) ↦ {⟨𝑧, 𝑥⟩}) ∈ ((𝐹𝑧)Homeo(∏t‘{⟨𝑧, (𝐹𝑧)⟩})) → (𝐹𝑧) ≃ (∏t‘{⟨𝑧, (𝐹𝑧)⟩}))
104102, 103syl 17 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹𝑧) ≃ (∏t‘{⟨𝑧, (𝐹𝑧)⟩}))
105 cmphmph 22503 . . . . . . . . . . . . . . 15 ((𝐹𝑧) ≃ (∏t‘{⟨𝑧, (𝐹𝑧)⟩}) → ((𝐹𝑧) ∈ Comp → (∏t‘{⟨𝑧, (𝐹𝑧)⟩}) ∈ Comp))
106104, 98, 105sylc 65 . . . . . . . . . . . . . 14 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘{⟨𝑧, (𝐹𝑧)⟩}) ∈ Comp)
10795, 106eqeltrd 2853 . . . . . . . . . . . . 13 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘(𝐹 ↾ {𝑧})) ∈ Comp)
108 txcmp 22358 . . . . . . . . . . . . . 14 (((∏t‘(𝐹𝑦)) ∈ Comp ∧ (∏t‘(𝐹 ↾ {𝑧})) ∈ Comp) → ((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp)
109108expcom 417 . . . . . . . . . . . . 13 ((∏t‘(𝐹 ↾ {𝑧})) ∈ Comp → ((∏t‘(𝐹𝑦)) ∈ Comp → ((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp))
110107, 109syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ((∏t‘(𝐹𝑦)) ∈ Comp → ((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp))
111 cmphmph 22503 . . . . . . . . . . . 12 (((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ≃ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) → (((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))
11287, 110, 111sylsyld 61 . . . . . . . . . . 11 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ((∏t‘(𝐹𝑦)) ∈ Comp → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))
113112expcom 417 . . . . . . . . . 10 ((¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → ((∏t‘(𝐹𝑦)) ∈ Comp → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
114113a2d 29 . . . . . . . . 9 ((¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
115114ex 416 . . . . . . . 8 𝑧𝑦 → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
116115a2d 29 . . . . . . 7 𝑧𝑦 → (((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
11756, 116syl5 34 . . . . . 6 𝑧𝑦 → ((𝑦𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
118117adantl 485 . . . . 5 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((𝑦𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
11914, 20, 26, 32, 52, 118findcard2s 8750 . . . 4 (𝐴 ∈ Fin → (𝐴𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝐴)) ∈ Comp)))
1206, 119mpi 20 . . 3 (𝐴 ∈ Fin → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝐴)) ∈ Comp))
121120anabsi5 668 . 2 ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝐴)) ∈ Comp)
1225, 121eqeltrrd 2854 1 ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t𝐹) ∈ Comp)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1539   ∈ wcel 2112  Vcvv 3410   ∪ cun 3859   ∩ cin 3860   ⊆ wss 3861  ∅c0 4228  𝒫 cpw 4498  {csn 4526  ⟨cop 4532  ∪ cuni 4802   class class class wbr 5037   ↦ cmpt 5117   ↾ cres 5531   Fn wfn 6336  ⟶wf 6337  ‘cfv 6341  (class class class)co 7157   ∈ cmpo 7159  Xcixp 8493  Fincfn 8541  ∏tcpt 16785  Topctop 21608  TopOnctopon 21625  Compccmp 22101   ×t ctx 22275  Homeochmeo 22468   ≃ chmph 22469 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5161  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-pss 3880  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4803  df-int 4843  df-iun 4889  df-iin 4890  df-br 5038  df-opab 5100  df-mpt 5118  df-tr 5144  df-id 5435  df-eprel 5440  df-po 5448  df-so 5449  df-fr 5488  df-we 5490  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-ord 6178  df-on 6179  df-lim 6180  df-suc 6181  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-ov 7160  df-oprab 7161  df-mpo 7162  df-om 7587  df-1st 7700  df-2nd 7701  df-1o 8119  df-er 8306  df-map 8425  df-ixp 8494  df-en 8542  df-dom 8543  df-fin 8545  df-fi 8922  df-topgen 16790  df-pt 16791  df-top 21609  df-topon 21626  df-bases 21661  df-cn 21942  df-cnp 21943  df-cmp 22102  df-tx 22277  df-hmeo 22470  df-hmph 22471 This theorem is referenced by:  poimirlem30  35403
 Copyright terms: Public domain W3C validator