Metamath Proof Explorer

Theorem ptcmpfi

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)

Ref Expression
Assertion ptcmpfi ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ 𝐹 ) ∈ Comp )

Proof

Step Hyp Ref Expression
1 ffn ⊢ ( 𝐹 : 𝐴 ⟶ Comp → 𝐹 Fn 𝐴 )
2 fnresdm ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
3 1 2 syl ⊢ ( 𝐹 : 𝐴 ⟶ Comp → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
4 3 adantl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
5 4 fveq2d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝐴 ) ) = ( ∏t ‘ 𝐹 ) )
6 ssid ⊢ 𝐴 ⊆ 𝐴
7 sseq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴 ) )
8 reseq2 ⊢ ( 𝑥 = ∅ → ( 𝐹 ↾ 𝑥 ) = ( 𝐹 ↾ ∅ ) )
9 res0 ⊢ ( 𝐹 ↾ ∅ ) = ∅
10 8 9 eqtrdi ⊢ ( 𝑥 = ∅ → ( 𝐹 ↾ 𝑥 ) = ∅ )
11 10 fveq2d ⊢ ( 𝑥 = ∅ → ( ∏t ‘ ( 𝐹 ↾ 𝑥 ) ) = ( ∏t ‘ ∅ ) )
12 11 eleq1d ⊢ ( 𝑥 = ∅ → ( ( ∏t ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ Comp ↔ ( ∏t ‘ ∅ ) ∈ Comp ) )
13 12 imbi2d ⊢ ( 𝑥 = ∅ → ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ Comp ) ↔ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ∅ ) ∈ Comp ) ) )
14 7 13 imbi12d ⊢ ( 𝑥 = ∅ → ( ( 𝑥 ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ Comp ) ) ↔ ( ∅ ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ∅ ) ∈ Comp ) ) ) )
15 sseq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴 ) )
16 reseq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ↾ 𝑥 ) = ( 𝐹 ↾ 𝑦 ) )
17 16 fveq2d ⊢ ( 𝑥 = 𝑦 → ( ∏t ‘ ( 𝐹 ↾ 𝑥 ) ) = ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) )
18 17 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( ∏t ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ Comp ↔ ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ∈ Comp ) )
19 18 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ Comp ) ↔ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ∈ Comp ) ) )
20 15 19 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ Comp ) ) ↔ ( 𝑦 ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ∈ Comp ) ) ) )
21 sseq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑥 ⊆ 𝐴 ↔ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) )
22 reseq2 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐹 ↾ 𝑥 ) = ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) )
23 22 fveq2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∏t ‘ ( 𝐹 ↾ 𝑥 ) ) = ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) )
24 23 eleq1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ∏t ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ Comp ↔ ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ∈ Comp ) )
25 24 imbi2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ Comp ) ↔ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ∈ Comp ) ) )
26 21 25 imbi12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑥 ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ Comp ) ) ↔ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ∈ Comp ) ) ) )
27 sseq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
28 reseq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ↾ 𝑥 ) = ( 𝐹 ↾ 𝐴 ) )
29 28 fveq2d ⊢ ( 𝑥 = 𝐴 → ( ∏t ‘ ( 𝐹 ↾ 𝑥 ) ) = ( ∏t ‘ ( 𝐹 ↾ 𝐴 ) ) )
30 29 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( ∏t ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ Comp ↔ ( ∏t ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ Comp ) )
31 30 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ Comp ) ↔ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ Comp ) ) )
32 27 31 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝑥 ) ) ∈ Comp ) ) ↔ ( 𝐴 ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ Comp ) ) ) )
33 0ex ⊢ ∅ ∈ V
34 f0 ⊢ ∅ : ∅ ⟶ Top
35 pttop ⊢ ( ( ∅ ∈ V ∧ ∅ : ∅ ⟶ Top ) → ( ∏t ‘ ∅ ) ∈ Top )
36 33 34 35 mp2an ⊢ ( ∏t ‘ ∅ ) ∈ Top
37 eqid ⊢ ( ∏t ‘ ∅ ) = ( ∏t ‘ ∅ )
38 37 ptuni ⊢ ( ( ∅ ∈ V ∧ ∅ : ∅ ⟶ Top ) → X 𝑥 ∈ ∅ ∪ ( ∅ ‘ 𝑥 ) = ∪ ( ∏t ‘ ∅ ) )
39 33 34 38 mp2an ⊢ X 𝑥 ∈ ∅ ∪ ( ∅ ‘ 𝑥 ) = ∪ ( ∏t ‘ ∅ )
40 ixp0x ⊢ X 𝑥 ∈ ∅ ∪ ( ∅ ‘ 𝑥 ) = { ∅ }
41 snfi ⊢ { ∅ } ∈ Fin
42 40 41 eqeltri ⊢ X 𝑥 ∈ ∅ ∪ ( ∅ ‘ 𝑥 ) ∈ Fin
43 39 42 eqeltrri ⊢ ∪ ( ∏t ‘ ∅ ) ∈ Fin
44 pwfi ⊢ ( ∪ ( ∏t ‘ ∅ ) ∈ Fin ↔ 𝒫 ∪ ( ∏t ‘ ∅ ) ∈ Fin )
45 43 44 mpbi ⊢ 𝒫 ∪ ( ∏t ‘ ∅ ) ∈ Fin
46 pwuni ⊢ ( ∏t ‘ ∅ ) ⊆ 𝒫 ∪ ( ∏t ‘ ∅ )
47 ssfi ⊢ ( ( 𝒫 ∪ ( ∏t ‘ ∅ ) ∈ Fin ∧ ( ∏t ‘ ∅ ) ⊆ 𝒫 ∪ ( ∏t ‘ ∅ ) ) → ( ∏t ‘ ∅ ) ∈ Fin )
48 45 46 47 mp2an ⊢ ( ∏t ‘ ∅ ) ∈ Fin
49 36 48 elini ⊢ ( ∏t ‘ ∅ ) ∈ ( Top ∩ Fin )
50 fincmp ⊢ ( ( ∏t ‘ ∅ ) ∈ ( Top ∩ Fin ) → ( ∏t ‘ ∅ ) ∈ Comp )
51 49 50 ax-mp ⊢ ( ∏t ‘ ∅ ) ∈ Comp
52 51 2a1i ⊢ ( ∅ ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ∅ ) ∈ Comp ) )
53 ssun1 ⊢ 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } )
54 id ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 )
55 53 54 sstrid ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → 𝑦 ⊆ 𝐴 )
56 55 imim1i ⊢ ( ( 𝑦 ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ∈ Comp ) ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ∈ Comp ) ) )
57 eqid ⊢ ∪ ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) = ∪ ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) )
58 eqid ⊢ ∪ ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) = ∪ ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) )
59 eqid ⊢ ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) = ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) )
60 resabs1 ⊢ ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ↾ 𝑦 ) = ( 𝐹 ↾ 𝑦 ) )
61 53 60 ax-mp ⊢ ( ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ↾ 𝑦 ) = ( 𝐹 ↾ 𝑦 )
62 61 eqcomi ⊢ ( 𝐹 ↾ 𝑦 ) = ( ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ↾ 𝑦 )
63 62 fveq2i ⊢ ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) = ( ∏t ‘ ( ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ↾ 𝑦 ) )
64 ssun2 ⊢ { 𝑧 } ⊆ ( 𝑦 ∪ { 𝑧 } )
65 resabs1 ⊢ ( { 𝑧 } ⊆ ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ↾ { 𝑧 } ) = ( 𝐹 ↾ { 𝑧 } ) )
66 64 65 ax-mp ⊢ ( ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ↾ { 𝑧 } ) = ( 𝐹 ↾ { 𝑧 } )
67 66 eqcomi ⊢ ( 𝐹 ↾ { 𝑧 } ) = ( ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ↾ { 𝑧 } )
68 67 fveq2i ⊢ ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) = ( ∏t ‘ ( ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ↾ { 𝑧 } ) )
69 eqid ⊢ ( 𝑢 ∈ ∪ ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) , 𝑣 ∈ ∪ ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) ↦ ( 𝑢 ∪ 𝑣 ) ) = ( 𝑢 ∈ ∪ ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) , 𝑣 ∈ ∪ ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) ↦ ( 𝑢 ∪ 𝑣 ) )
70 vex ⊢ 𝑦 ∈ V
71 vsnex ⊢ { 𝑧 } ∈ V
72 70 71 unex ⊢ ( 𝑦 ∪ { 𝑧 } ) ∈ V
73 72 a1i ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑦 ∪ { 𝑧 } ) ∈ V )
74 simplr ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝐹 : 𝐴 ⟶ Comp )
75 cmptop ⊢ ( 𝑥 ∈ Comp → 𝑥 ∈ Top )
76 75 ssriv ⊢ Comp ⊆ Top
77 fss ⊢ ( ( 𝐹 : 𝐴 ⟶ Comp ∧ Comp ⊆ Top ) → 𝐹 : 𝐴 ⟶ Top )
78 74 76 77 sylancl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝐹 : 𝐴 ⟶ Top )
79 simprr ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 )
80 78 79 fssresd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) : ( 𝑦 ∪ { 𝑧 } ) ⟶ Top )
81 eqidd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑦 ∪ { 𝑧 } ) = ( 𝑦 ∪ { 𝑧 } ) )
82 simprl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ¬ 𝑧 ∈ 𝑦 )
83 disjsn ⊢ ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑦 )
84 82 83 sylibr ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ )
85 57 58 59 63 68 69 73 80 81 84 ptunhmeo ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑢 ∈ ∪ ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) , 𝑣 ∈ ∪ ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) ↦ ( 𝑢 ∪ 𝑣 ) ) ∈ ( ( ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ×t ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) ) Homeo ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ) )
86 hmphi ⊢ ( ( 𝑢 ∈ ∪ ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) , 𝑣 ∈ ∪ ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) ↦ ( 𝑢 ∪ 𝑣 ) ) ∈ ( ( ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ×t ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) ) Homeo ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ) → ( ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ×t ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) ) ≃ ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) )
87 85 86 syl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ×t ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) ) ≃ ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) )
88 1 ad2antlr ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝐹 Fn 𝐴 )
89 64 79 sstrid ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → { 𝑧 } ⊆ 𝐴 )
90 vex ⊢ 𝑧 ∈ V
91 90 snss ⊢ ( 𝑧 ∈ 𝐴 ↔ { 𝑧 } ⊆ 𝐴 )
92 89 91 sylibr ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑧 ∈ 𝐴 )
93 fnressn ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ↾ { 𝑧 } ) = { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } )
94 88 92 93 syl2anc ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝐹 ↾ { 𝑧 } ) = { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } )
95 94 fveq2d ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) = ( ∏t ‘ { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } ) )
96 eqid ⊢ ( ∏t ‘ { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } ) = ( ∏t ‘ { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } )
97 90 a1i ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑧 ∈ V )
98 74 92 ffvelcdmd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ Comp )
99 76 98 sselid ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ Top )
100 toptopon2 ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ Top ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( TopOn ‘ ∪ ( 𝐹 ‘ 𝑧 ) ) )
101 99 100 sylib ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( TopOn ‘ ∪ ( 𝐹 ‘ 𝑧 ) ) )
102 96 97 101 pt1hmeo ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑧 ) ↦ { ⟨ 𝑧 , 𝑥 ⟩ } ) ∈ ( ( 𝐹 ‘ 𝑧 ) Homeo ( ∏t ‘ { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } ) ) )
103 hmphi ⊢ ( ( 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑧 ) ↦ { ⟨ 𝑧 , 𝑥 ⟩ } ) ∈ ( ( 𝐹 ‘ 𝑧 ) Homeo ( ∏t ‘ { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } ) ) → ( 𝐹 ‘ 𝑧 ) ≃ ( ∏t ‘ { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } ) )
104 102 103 syl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝐹 ‘ 𝑧 ) ≃ ( ∏t ‘ { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } ) )
105 cmphmph ⊢ ( ( 𝐹 ‘ 𝑧 ) ≃ ( ∏t ‘ { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } ) → ( ( 𝐹 ‘ 𝑧 ) ∈ Comp → ( ∏t ‘ { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } ) ∈ Comp ) )
106 104 98 105 sylc ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( ∏t ‘ { ⟨ 𝑧 , ( 𝐹 ‘ 𝑧 ) ⟩ } ) ∈ Comp )
107 95 106 eqeltrd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) ∈ Comp )
108 txcmp ⊢ ( ( ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ∈ Comp ∧ ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) ∈ Comp ) → ( ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ×t ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) ) ∈ Comp )
109 108 expcom ⊢ ( ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) ∈ Comp → ( ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ∈ Comp → ( ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ×t ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) ) ∈ Comp ) )
110 107 109 syl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ∈ Comp → ( ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ×t ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) ) ∈ Comp ) )
111 cmphmph ⊢ ( ( ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ×t ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) ) ≃ ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) → ( ( ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ×t ( ∏t ‘ ( 𝐹 ↾ { 𝑧 } ) ) ) ∈ Comp → ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ∈ Comp ) )
112 87 110 111 sylsyld ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) ∧ ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ∈ Comp → ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ∈ Comp ) )
113 112 expcom ⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ∈ Comp → ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ∈ Comp ) ) )
114 113 a2d ⊢ ( ( ¬ 𝑧 ∈ 𝑦 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) → ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ∈ Comp ) → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ∈ Comp ) ) )
115 114 ex ⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ∈ Comp ) → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ∈ Comp ) ) ) )
116 115 a2d ⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ∈ Comp ) ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ∈ Comp ) ) ) )
117 56 116 syl5 ⊢ ( ¬ 𝑧 ∈ 𝑦 → ( ( 𝑦 ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ∈ Comp ) ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ∈ Comp ) ) ) )
118 117 adantl ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( 𝑦 ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝑦 ) ) ∈ Comp ) ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ∈ Comp ) ) ) )
119 14 20 26 32 52 118 findcard2s ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ⊆ 𝐴 → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ Comp ) ) )
120 6 119 mpi ⊢ ( 𝐴 ∈ Fin → ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ Comp ) )
121 120 anabsi5 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ Comp )
122 5 121 eqeltrrd ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 ⟶ Comp ) → ( ∏t ‘ 𝐹 ) ∈ Comp )