Metamath Proof Explorer

Theorem ptcld

Description: A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Hypotheses ptcld.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
ptcld.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ Top )
ptcld.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( Clsd ‘ ( 𝐹 ‘ 𝑘 ) ) )
Assertion ptcld ( 𝜑 → X 𝑘 ∈ 𝐴 𝐶 ∈ ( Clsd ‘ ( ∏t ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 ptcld.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 ptcld.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ Top )
3 ptcld.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ( Clsd ‘ ( 𝐹 ‘ 𝑘 ) ) )
4 eqid ⊢ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 )
5 4 cldss ⊢ ( 𝐶 ∈ ( Clsd ‘ ( 𝐹 ‘ 𝑘 ) ) → 𝐶 ⊆ ∪ ( 𝐹 ‘ 𝑘 ) )
6 3 5 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ⊆ ∪ ( 𝐹 ‘ 𝑘 ) )
7 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ ∪ ( 𝐹 ‘ 𝑘 ) )
8 boxriin ⊢ ( ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ ∪ ( 𝐹 ‘ 𝑘 ) → X 𝑘 ∈ 𝐴 𝐶 = ( X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∩ ∩ 𝑥 ∈ 𝐴 X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) )
9 7 8 syl ⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 𝐶 = ( X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∩ ∩ 𝑥 ∈ 𝐴 X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) )
10 eqid ⊢ ( ∏t ‘ 𝐹 ) = ( ∏t ‘ 𝐹 )
11 10 ptuni ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( ∏t ‘ 𝐹 ) )
12 1 2 11 syl2anc ⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( ∏t ‘ 𝐹 ) )
13 12 ineq1d ⊢ ( 𝜑 → ( X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∩ ∩ 𝑥 ∈ 𝐴 X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) = ( ∪ ( ∏t ‘ 𝐹 ) ∩ ∩ 𝑥 ∈ 𝐴 X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) )
14 pttop ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ Top ) → ( ∏t ‘ 𝐹 ) ∈ Top )
15 1 2 14 syl2anc ⊢ ( 𝜑 → ( ∏t ‘ 𝐹 ) ∈ Top )
16 sseq1 ⊢ ( 𝐶 = if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) → ( 𝐶 ⊆ ∪ ( 𝐹 ‘ 𝑘 ) ↔ if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ⊆ ∪ ( 𝐹 ‘ 𝑘 ) ) )
17 sseq1 ⊢ ( ∪ ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) → ( ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ ( 𝐹 ‘ 𝑘 ) ↔ if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ⊆ ∪ ( 𝐹 ‘ 𝑘 ) ) )
18 simpl ⊢ ( ( 𝐶 ⊆ ∪ ( 𝐹 ‘ 𝑘 ) ∧ 𝑘 = 𝑥 ) → 𝐶 ⊆ ∪ ( 𝐹 ‘ 𝑘 ) )
19 ssidd ⊢ ( ( 𝐶 ⊆ ∪ ( 𝐹 ‘ 𝑘 ) ∧ ¬ 𝑘 = 𝑥 ) → ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ ( 𝐹 ‘ 𝑘 ) )
20 16 17 18 19 ifbothda ⊢ ( 𝐶 ⊆ ∪ ( 𝐹 ‘ 𝑘 ) → if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ⊆ ∪ ( 𝐹 ‘ 𝑘 ) )
21 20 ralimi ⊢ ( ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ ∪ ( 𝐹 ‘ 𝑘 ) → ∀ 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ⊆ ∪ ( 𝐹 ‘ 𝑘 ) )
22 ss2ixp ⊢ ( ∀ 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ⊆ ∪ ( 𝐹 ‘ 𝑘 ) → X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ⊆ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) )
23 7 21 22 3syl ⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ⊆ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ⊆ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) )
25 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( ∏t ‘ 𝐹 ) )
26 24 25 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ⊆ ∪ ( ∏t ‘ 𝐹 ) )
27 12 eqcomd ⊢ ( 𝜑 → ∪ ( ∏t ‘ 𝐹 ) = X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) )
28 27 difeq1d ⊢ ( 𝜑 → ( ∪ ( ∏t ‘ 𝐹 ) ∖ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) = ( X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∖ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∪ ( ∏t ‘ 𝐹 ) ∖ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) = ( X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∖ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) )
30 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
31 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ ∪ ( 𝐹 ‘ 𝑘 ) )
32 boxcutc ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ ∪ ( 𝐹 ‘ 𝑘 ) ) → ( X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∖ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) = X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ 𝐶 ) , ∪ ( 𝐹 ‘ 𝑘 ) ) )
33 30 31 32 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∖ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) = X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ 𝐶 ) , ∪ ( 𝐹 ‘ 𝑘 ) ) )
34 ixpeq2 ⊢ ( ∀ 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ 𝐶 ) , ∪ ( 𝐹 ‘ 𝑘 ) ) = if ( 𝑘 = 𝑥 , ( ∪ ( 𝐹 ‘ 𝑥 ) ∖ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ) , ∪ ( 𝐹 ‘ 𝑘 ) ) → X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ 𝐶 ) , ∪ ( 𝐹 ‘ 𝑘 ) ) = X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , ( ∪ ( 𝐹 ‘ 𝑥 ) ∖ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ) , ∪ ( 𝐹 ‘ 𝑘 ) ) )
35 fveq2 ⊢ ( 𝑘 = 𝑥 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑥 ) )
36 35 unieqd ⊢ ( 𝑘 = 𝑥 → ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑥 ) )
37 csbeq1a ⊢ ( 𝑘 = 𝑥 → 𝐶 = ⦋ 𝑥 / 𝑘 ⦌ 𝐶 )
38 36 37 difeq12d ⊢ ( 𝑘 = 𝑥 → ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ 𝐶 ) = ( ∪ ( 𝐹 ‘ 𝑥 ) ∖ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ) )
39 38 adantl ⊢ ( ( 𝑘 ∈ 𝐴 ∧ 𝑘 = 𝑥 ) → ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ 𝐶 ) = ( ∪ ( 𝐹 ‘ 𝑥 ) ∖ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ) )
40 39 ifeq1da ⊢ ( 𝑘 ∈ 𝐴 → if ( 𝑘 = 𝑥 , ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ 𝐶 ) , ∪ ( 𝐹 ‘ 𝑘 ) ) = if ( 𝑘 = 𝑥 , ( ∪ ( 𝐹 ‘ 𝑥 ) ∖ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ) , ∪ ( 𝐹 ‘ 𝑘 ) ) )
41 34 40 mprg ⊢ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ 𝐶 ) , ∪ ( 𝐹 ‘ 𝑘 ) ) = X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , ( ∪ ( 𝐹 ‘ 𝑥 ) ∖ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ) , ∪ ( 𝐹 ‘ 𝑘 ) )
42 41 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ 𝐶 ) , ∪ ( 𝐹 ‘ 𝑘 ) ) = X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , ( ∪ ( 𝐹 ‘ 𝑥 ) ∖ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ) , ∪ ( 𝐹 ‘ 𝑘 ) ) )
43 29 33 42 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∪ ( ∏t ‘ 𝐹 ) ∖ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) = X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , ( ∪ ( 𝐹 ‘ 𝑥 ) ∖ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ) , ∪ ( 𝐹 ‘ 𝑘 ) ) )
44 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ∈ 𝑉 )
45 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 : 𝐴 ⟶ Top )
46 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ( Clsd ‘ ( 𝐹 ‘ 𝑘 ) ) )
47 nfv ⊢ Ⅎ 𝑥 𝐶 ∈ ( Clsd ‘ ( 𝐹 ‘ 𝑘 ) )
48 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑥 / 𝑘 ⦌ 𝐶
49 48 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ ( Clsd ‘ ( 𝐹 ‘ 𝑥 ) )
50 2fveq3 ⊢ ( 𝑘 = 𝑥 → ( Clsd ‘ ( 𝐹 ‘ 𝑘 ) ) = ( Clsd ‘ ( 𝐹 ‘ 𝑥 ) ) )
51 37 50 eleq12d ⊢ ( 𝑘 = 𝑥 → ( 𝐶 ∈ ( Clsd ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ ( Clsd ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
52 47 49 51 cbvralw ⊢ ( ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ( Clsd ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ ( Clsd ‘ ( 𝐹 ‘ 𝑥 ) ) )
53 46 52 sylib ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ ( Clsd ‘ ( 𝐹 ‘ 𝑥 ) ) )
54 53 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ ( Clsd ‘ ( 𝐹 ‘ 𝑥 ) ) )
55 eqid ⊢ ∪ ( 𝐹 ‘ 𝑥 ) = ∪ ( 𝐹 ‘ 𝑥 )
56 55 cldopn ⊢ ( ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ∈ ( Clsd ‘ ( 𝐹 ‘ 𝑥 ) ) → ( ∪ ( 𝐹 ‘ 𝑥 ) ∖ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ) ∈ ( 𝐹 ‘ 𝑥 ) )
57 54 56 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∪ ( 𝐹 ‘ 𝑥 ) ∖ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ) ∈ ( 𝐹 ‘ 𝑥 ) )
58 44 45 57 ptopn2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , ( ∪ ( 𝐹 ‘ 𝑥 ) ∖ ⦋ 𝑥 / 𝑘 ⦌ 𝐶 ) , ∪ ( 𝐹 ‘ 𝑘 ) ) ∈ ( ∏t ‘ 𝐹 ) )
59 43 58 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∪ ( ∏t ‘ 𝐹 ) ∖ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ( ∏t ‘ 𝐹 ) )
60 eqid ⊢ ∪ ( ∏t ‘ 𝐹 ) = ∪ ( ∏t ‘ 𝐹 )
61 60 iscld ⊢ ( ( ∏t ‘ 𝐹 ) ∈ Top → ( X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ∈ ( Clsd ‘ ( ∏t ‘ 𝐹 ) ) ↔ ( X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ⊆ ∪ ( ∏t ‘ 𝐹 ) ∧ ( ∪ ( ∏t ‘ 𝐹 ) ∖ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ( ∏t ‘ 𝐹 ) ) ) )
62 15 61 syl ⊢ ( 𝜑 → ( X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ∈ ( Clsd ‘ ( ∏t ‘ 𝐹 ) ) ↔ ( X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ⊆ ∪ ( ∏t ‘ 𝐹 ) ∧ ( ∪ ( ∏t ‘ 𝐹 ) ∖ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ( ∏t ‘ 𝐹 ) ) ) )
63 62 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ∈ ( Clsd ‘ ( ∏t ‘ 𝐹 ) ) ↔ ( X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ⊆ ∪ ( ∏t ‘ 𝐹 ) ∧ ( ∪ ( ∏t ‘ 𝐹 ) ∖ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ( ∏t ‘ 𝐹 ) ) ) )
64 26 59 63 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ∈ ( Clsd ‘ ( ∏t ‘ 𝐹 ) ) )
65 64 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ∈ ( Clsd ‘ ( ∏t ‘ 𝐹 ) ) )
66 60 riincld ⊢ ( ( ( ∏t ‘ 𝐹 ) ∈ Top ∧ ∀ 𝑥 ∈ 𝐴 X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ∈ ( Clsd ‘ ( ∏t ‘ 𝐹 ) ) ) → ( ∪ ( ∏t ‘ 𝐹 ) ∩ ∩ 𝑥 ∈ 𝐴 X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ( Clsd ‘ ( ∏t ‘ 𝐹 ) ) )
67 15 65 66 syl2anc ⊢ ( 𝜑 → ( ∪ ( ∏t ‘ 𝐹 ) ∩ ∩ 𝑥 ∈ 𝐴 X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ( Clsd ‘ ( ∏t ‘ 𝐹 ) ) )
68 13 67 eqeltrd ⊢ ( 𝜑 → ( X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∩ ∩ 𝑥 ∈ 𝐴 X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝐶 , ∪ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ( Clsd ‘ ( ∏t ‘ 𝐹 ) ) )
69 9 68 eqeltrd ⊢ ( 𝜑 → X 𝑘 ∈ 𝐴 𝐶 ∈ ( Clsd ‘ ( ∏t ‘ 𝐹 ) ) )