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𝐹 ) ) )