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

Theorem ptcmpfi 21664
 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 6083 . . . . 5 (𝐹:𝐴⟶Comp → 𝐹 Fn 𝐴)
2 fnresdm 6038 . . . . 5 (𝐹 Fn 𝐴 → (𝐹𝐴) = 𝐹)
31, 2syl 17 . . . 4 (𝐹:𝐴⟶Comp → (𝐹𝐴) = 𝐹)
43adantl 481 . . 3 ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (𝐹𝐴) = 𝐹)
54fveq2d 6233 . 2 ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝐴)) = (∏t𝐹))
6 ssid 3657 . . . 4 𝐴𝐴
7 sseq1 3659 . . . . . 6 (𝑥 = ∅ → (𝑥𝐴 ↔ ∅ ⊆ 𝐴))
8 reseq2 5423 . . . . . . . . . 10 (𝑥 = ∅ → (𝐹𝑥) = (𝐹 ↾ ∅))
9 res0 5432 . . . . . . . . . 10 (𝐹 ↾ ∅) = ∅
108, 9syl6eq 2701 . . . . . . . . 9 (𝑥 = ∅ → (𝐹𝑥) = ∅)
1110fveq2d 6233 . . . . . . . 8 (𝑥 = ∅ → (∏t‘(𝐹𝑥)) = (∏t‘∅))
1211eleq1d 2715 . . . . . . 7 (𝑥 = ∅ → ((∏t‘(𝐹𝑥)) ∈ Comp ↔ (∏t‘∅) ∈ Comp))
1312imbi2d 329 . . . . . 6 (𝑥 = ∅ → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘∅) ∈ Comp)))
147, 13imbi12d 333 . . . . 5 (𝑥 = ∅ → ((𝑥𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑥)) ∈ Comp)) ↔ (∅ ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘∅) ∈ Comp))))
15 sseq1 3659 . . . . . 6 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
16 reseq2 5423 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
1716fveq2d 6233 . . . . . . . 8 (𝑥 = 𝑦 → (∏t‘(𝐹𝑥)) = (∏t‘(𝐹𝑦)))
1817eleq1d 2715 . . . . . . 7 (𝑥 = 𝑦 → ((∏t‘(𝐹𝑥)) ∈ Comp ↔ (∏t‘(𝐹𝑦)) ∈ Comp))
1918imbi2d 329 . . . . . 6 (𝑥 = 𝑦 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp)))
2015, 19imbi12d 333 . . . . 5 (𝑥 = 𝑦 → ((𝑥𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑥)) ∈ Comp)) ↔ (𝑦𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp))))
21 sseq1 3659 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑥𝐴 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐴))
22 reseq2 5423 . . . . . . . . 9 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹𝑥) = (𝐹 ↾ (𝑦 ∪ {𝑧})))
2322fveq2d 6233 . . . . . . . 8 (𝑥 = (𝑦 ∪ {𝑧}) → (∏t‘(𝐹𝑥)) = (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))))
2423eleq1d 2715 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → ((∏t‘(𝐹𝑥)) ∈ Comp ↔ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))
2524imbi2d 329 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
2621, 25imbi12d 333 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑥𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑥)) ∈ Comp)) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
27 sseq1 3659 . . . . . 6 (𝑥 = 𝐴 → (𝑥𝐴𝐴𝐴))
28 reseq2 5423 . . . . . . . . 9 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
2928fveq2d 6233 . . . . . . . 8 (𝑥 = 𝐴 → (∏t‘(𝐹𝑥)) = (∏t‘(𝐹𝐴)))
3029eleq1d 2715 . . . . . . 7 (𝑥 = 𝐴 → ((∏t‘(𝐹𝑥)) ∈ Comp ↔ (∏t‘(𝐹𝐴)) ∈ Comp))
3130imbi2d 329 . . . . . 6 (𝑥 = 𝐴 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑥)) ∈ Comp) ↔ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝐴)) ∈ Comp)))
3227, 31imbi12d 333 . . . . 5 (𝑥 = 𝐴 → ((𝑥𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑥)) ∈ Comp)) ↔ (𝐴𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝐴)) ∈ Comp))))
33 0ex 4823 . . . . . . . . 9 ∅ ∈ V
34 f0 6124 . . . . . . . . 9 ∅:∅⟶Top
35 pttop 21433 . . . . . . . . 9 ((∅ ∈ V ∧ ∅:∅⟶Top) → (∏t‘∅) ∈ Top)
3633, 34, 35mp2an 708 . . . . . . . 8 (∏t‘∅) ∈ Top
37 eqid 2651 . . . . . . . . . . . . 13 (∏t‘∅) = (∏t‘∅)
3837ptuni 21445 . . . . . . . . . . . 12 ((∅ ∈ V ∧ ∅:∅⟶Top) → X𝑥 ∈ ∅ (∅‘𝑥) = (∏t‘∅))
3933, 34, 38mp2an 708 . . . . . . . . . . 11 X𝑥 ∈ ∅ (∅‘𝑥) = (∏t‘∅)
40 ixp0x 7978 . . . . . . . . . . . 12 X𝑥 ∈ ∅ (∅‘𝑥) = {∅}
41 snfi 8079 . . . . . . . . . . . 12 {∅} ∈ Fin
4240, 41eqeltri 2726 . . . . . . . . . . 11 X𝑥 ∈ ∅ (∅‘𝑥) ∈ Fin
4339, 42eqeltrri 2727 . . . . . . . . . 10 (∏t‘∅) ∈ Fin
44 pwfi 8302 . . . . . . . . . 10 ( (∏t‘∅) ∈ Fin ↔ 𝒫 (∏t‘∅) ∈ Fin)
4543, 44mpbi 220 . . . . . . . . 9 𝒫 (∏t‘∅) ∈ Fin
46 pwuni 4506 . . . . . . . . 9 (∏t‘∅) ⊆ 𝒫 (∏t‘∅)
47 ssfi 8221 . . . . . . . . 9 ((𝒫 (∏t‘∅) ∈ Fin ∧ (∏t‘∅) ⊆ 𝒫 (∏t‘∅)) → (∏t‘∅) ∈ Fin)
4845, 46, 47mp2an 708 . . . . . . . 8 (∏t‘∅) ∈ Fin
49 elin 3829 . . . . . . . 8 ((∏t‘∅) ∈ (Top ∩ Fin) ↔ ((∏t‘∅) ∈ Top ∧ (∏t‘∅) ∈ Fin))
5036, 48, 49mpbir2an 975 . . . . . . 7 (∏t‘∅) ∈ (Top ∩ Fin)
51 fincmp 21244 . . . . . . 7 ((∏t‘∅) ∈ (Top ∩ Fin) → (∏t‘∅) ∈ Comp)
5250, 51ax-mp 5 . . . . . 6 (∏t‘∅) ∈ Comp
53522a1i 12 . . . . 5 (∅ ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘∅) ∈ Comp))
54 ssun1 3809 . . . . . . . . 9 𝑦 ⊆ (𝑦 ∪ {𝑧})
55 id 22 . . . . . . . . 9 ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
5654, 55syl5ss 3647 . . . . . . . 8 ((𝑦 ∪ {𝑧}) ⊆ 𝐴𝑦𝐴)
5756imim1i 63 . . . . . . 7 ((𝑦𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp)))
58 eqid 2651 . . . . . . . . . . . . . 14 (∏t‘(𝐹𝑦)) = (∏t‘(𝐹𝑦))
59 eqid 2651 . . . . . . . . . . . . . 14 (∏t‘(𝐹 ↾ {𝑧})) = (∏t‘(𝐹 ↾ {𝑧}))
60 eqid 2651 . . . . . . . . . . . . . 14 (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) = (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))
61 resabs1 5462 . . . . . . . . . . . . . . . . 17 (𝑦 ⊆ (𝑦 ∪ {𝑧}) → ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦) = (𝐹𝑦))
6254, 61ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦) = (𝐹𝑦)
6362eqcomi 2660 . . . . . . . . . . . . . . 15 (𝐹𝑦) = ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦)
6463fveq2i 6232 . . . . . . . . . . . . . 14 (∏t‘(𝐹𝑦)) = (∏t‘((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ 𝑦))
65 ssun2 3810 . . . . . . . . . . . . . . . . 17 {𝑧} ⊆ (𝑦 ∪ {𝑧})
66 resabs1 5462 . . . . . . . . . . . . . . . . 17 ({𝑧} ⊆ (𝑦 ∪ {𝑧}) → ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}) = (𝐹 ↾ {𝑧}))
6765, 66ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}) = (𝐹 ↾ {𝑧})
6867eqcomi 2660 . . . . . . . . . . . . . . 15 (𝐹 ↾ {𝑧}) = ((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧})
6968fveq2i 6232 . . . . . . . . . . . . . 14 (∏t‘(𝐹 ↾ {𝑧})) = (∏t‘((𝐹 ↾ (𝑦 ∪ {𝑧})) ↾ {𝑧}))
70 eqid 2651 . . . . . . . . . . . . . 14 (𝑢 (∏t‘(𝐹𝑦)), 𝑣 (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢𝑣)) = (𝑢 (∏t‘(𝐹𝑦)), 𝑣 (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢𝑣))
71 vex 3234 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
72 snex 4938 . . . . . . . . . . . . . . . 16 {𝑧} ∈ V
7371, 72unex 6998 . . . . . . . . . . . . . . 15 (𝑦 ∪ {𝑧}) ∈ V
7473a1i 11 . . . . . . . . . . . . . 14 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) ∈ V)
75 simplr 807 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹:𝐴⟶Comp)
76 cmptop 21246 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ Comp → 𝑥 ∈ Top)
7776ssriv 3640 . . . . . . . . . . . . . . . 16 Comp ⊆ Top
78 fss 6094 . . . . . . . . . . . . . . . 16 ((𝐹:𝐴⟶Comp ∧ Comp ⊆ Top) → 𝐹:𝐴⟶Top)
7975, 77, 78sylancl 695 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹:𝐴⟶Top)
80 simprr 811 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) ⊆ 𝐴)
8179, 80fssresd 6109 . . . . . . . . . . . . . 14 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹 ↾ (𝑦 ∪ {𝑧})):(𝑦 ∪ {𝑧})⟶Top)
82 eqidd 2652 . . . . . . . . . . . . . 14 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∪ {𝑧}) = (𝑦 ∪ {𝑧}))
83 simprl 809 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ¬ 𝑧𝑦)
84 disjsn 4278 . . . . . . . . . . . . . . 15 ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑦)
8583, 84sylibr 224 . . . . . . . . . . . . . 14 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑦 ∩ {𝑧}) = ∅)
8658, 59, 60, 64, 69, 70, 74, 81, 82, 85ptunhmeo 21659 . . . . . . . . . . . . 13 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑢 (∏t‘(𝐹𝑦)), 𝑣 (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢𝑣)) ∈ (((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧})))Homeo(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))))
87 hmphi 21628 . . . . . . . . . . . . 13 ((𝑢 (∏t‘(𝐹𝑦)), 𝑣 (∏t‘(𝐹 ↾ {𝑧})) ↦ (𝑢𝑣)) ∈ (((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧})))Homeo(∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧})))) → ((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ≃ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))))
8886, 87syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ≃ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))))
891ad2antlr 763 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝐹 Fn 𝐴)
9065, 80syl5ss 3647 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → {𝑧} ⊆ 𝐴)
91 vex 3234 . . . . . . . . . . . . . . . . . 18 𝑧 ∈ V
9291snss 4348 . . . . . . . . . . . . . . . . 17 (𝑧𝐴 ↔ {𝑧} ⊆ 𝐴)
9390, 92sylibr 224 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧𝐴)
94 fnressn 6465 . . . . . . . . . . . . . . . 16 ((𝐹 Fn 𝐴𝑧𝐴) → (𝐹 ↾ {𝑧}) = {⟨𝑧, (𝐹𝑧)⟩})
9589, 93, 94syl2anc 694 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹 ↾ {𝑧}) = {⟨𝑧, (𝐹𝑧)⟩})
9695fveq2d 6233 . . . . . . . . . . . . . 14 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘(𝐹 ↾ {𝑧})) = (∏t‘{⟨𝑧, (𝐹𝑧)⟩}))
97 eqid 2651 . . . . . . . . . . . . . . . . 17 (∏t‘{⟨𝑧, (𝐹𝑧)⟩}) = (∏t‘{⟨𝑧, (𝐹𝑧)⟩})
9891a1i 11 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → 𝑧 ∈ V)
9975, 93ffvelrnd 6400 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹𝑧) ∈ Comp)
10077, 99sseldi 3634 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹𝑧) ∈ Top)
101 eqid 2651 . . . . . . . . . . . . . . . . . . 19 (𝐹𝑧) = (𝐹𝑧)
102101toptopon 20770 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑧) ∈ Top ↔ (𝐹𝑧) ∈ (TopOn‘ (𝐹𝑧)))
103100, 102sylib 208 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹𝑧) ∈ (TopOn‘ (𝐹𝑧)))
10497, 98, 103pt1hmeo 21657 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝑥 (𝐹𝑧) ↦ {⟨𝑧, 𝑥⟩}) ∈ ((𝐹𝑧)Homeo(∏t‘{⟨𝑧, (𝐹𝑧)⟩})))
105 hmphi 21628 . . . . . . . . . . . . . . . 16 ((𝑥 (𝐹𝑧) ↦ {⟨𝑧, 𝑥⟩}) ∈ ((𝐹𝑧)Homeo(∏t‘{⟨𝑧, (𝐹𝑧)⟩})) → (𝐹𝑧) ≃ (∏t‘{⟨𝑧, (𝐹𝑧)⟩}))
106104, 105syl 17 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (𝐹𝑧) ≃ (∏t‘{⟨𝑧, (𝐹𝑧)⟩}))
107 cmphmph 21639 . . . . . . . . . . . . . . 15 ((𝐹𝑧) ≃ (∏t‘{⟨𝑧, (𝐹𝑧)⟩}) → ((𝐹𝑧) ∈ Comp → (∏t‘{⟨𝑧, (𝐹𝑧)⟩}) ∈ Comp))
108106, 99, 107sylc 65 . . . . . . . . . . . . . 14 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘{⟨𝑧, (𝐹𝑧)⟩}) ∈ Comp)
10996, 108eqeltrd 2730 . . . . . . . . . . . . 13 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → (∏t‘(𝐹 ↾ {𝑧})) ∈ Comp)
110 txcmp 21494 . . . . . . . . . . . . . 14 (((∏t‘(𝐹𝑦)) ∈ Comp ∧ (∏t‘(𝐹 ↾ {𝑧})) ∈ Comp) → ((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp)
111110expcom 450 . . . . . . . . . . . . 13 ((∏t‘(𝐹 ↾ {𝑧})) ∈ Comp → ((∏t‘(𝐹𝑦)) ∈ Comp → ((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp))
112109, 111syl 17 . . . . . . . . . . . 12 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ((∏t‘(𝐹𝑦)) ∈ Comp → ((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp))
113 cmphmph 21639 . . . . . . . . . . . 12 (((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ≃ (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) → (((∏t‘(𝐹𝑦)) ×t (∏t‘(𝐹 ↾ {𝑧}))) ∈ Comp → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))
11488, 112, 113sylsyld 61 . . . . . . . . . . 11 (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) ∧ (¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴)) → ((∏t‘(𝐹𝑦)) ∈ Comp → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))
115114expcom 450 . . . . . . . . . 10 ((¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → ((∏t‘(𝐹𝑦)) ∈ Comp → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
116115a2d 29 . . . . . . . . 9 ((¬ 𝑧𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐴) → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp)))
117116ex 449 . . . . . . . 8 𝑧𝑦 → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → (((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp) → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
118117a2d 29 . . . . . . 7 𝑧𝑦 → (((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
11957, 118syl5 34 . . . . . 6 𝑧𝑦 → ((𝑦𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
120119adantl 481 . . . . 5 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((𝑦𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝑦)) ∈ Comp)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹 ↾ (𝑦 ∪ {𝑧}))) ∈ Comp))))
12114, 20, 26, 32, 53, 120findcard2s 8242 . . . 4 (𝐴 ∈ Fin → (𝐴𝐴 → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝐴)) ∈ Comp)))
1226, 121mpi 20 . . 3 (𝐴 ∈ Fin → ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝐴)) ∈ Comp))
123122anabsi5 875 . 2 ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘(𝐹𝐴)) ∈ Comp)
1245, 123eqeltrrd 2731 1 ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t𝐹) ∈ Comp)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1523   ∈ wcel 2030  Vcvv 3231   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  𝒫 cpw 4191  {csn 4210  ⟨cop 4216  ∪ cuni 4468   class class class wbr 4685   ↦ cmpt 4762   ↾ cres 5145   Fn wfn 5921  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690   ↦ cmpt2 6692  Xcixp 7950  Fincfn 7997  ∏tcpt 16146  Topctop 20746  TopOnctopon 20763  Compccmp 21237   ×t ctx 21411  Homeochmeo 21604   ≃ chmph 21605 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fi 8358  df-topgen 16151  df-pt 16152  df-top 20747  df-topon 20764  df-bases 20798  df-cn 21079  df-cnp 21080  df-cmp 21238  df-tx 21413  df-hmeo 21606  df-hmph 21607 This theorem is referenced by:  poimirlem30  33569
 Copyright terms: Public domain W3C validator