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 
|- ( ph -> A e. V )
ptcld.f 
|- ( ph -> F : A --> Top )
ptcld.c 
|- ( ( ph /\ k e. A ) -> C e. ( Clsd ` ( F ` k ) ) )
Assertion ptcld 
|- ( ph -> X_ k e. A C e. ( Clsd ` ( Xt_ ` F ) ) )

Proof

Step Hyp Ref Expression
1 ptcld.a 
 |-  ( ph -> A e. V )
2 ptcld.f 
 |-  ( ph -> F : A --> Top )
3 ptcld.c 
 |-  ( ( ph /\ k e. A ) -> C e. ( Clsd ` ( F ` k ) ) )
4 eqid 
 |-  U. ( F ` k ) = U. ( F ` k )
5 4 cldss 
 |-  ( C e. ( Clsd ` ( F ` k ) ) -> C C_ U. ( F ` k ) )
6 3 5 syl 
 |-  ( ( ph /\ k e. A ) -> C C_ U. ( F ` k ) )
7 6 ralrimiva 
 |-  ( ph -> A. k e. A C C_ U. ( F ` k ) )
8 boxriin 
 |-  ( A. k e. A C C_ U. ( F ` k ) -> X_ k e. A C = ( X_ k e. A U. ( F ` k ) i^i |^|_ x e. A X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) )
9 7 8 syl 
 |-  ( ph -> X_ k e. A C = ( X_ k e. A U. ( F ` k ) i^i |^|_ x e. A X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) )
10 eqid 
 |-  ( Xt_ ` F ) = ( Xt_ ` F )
11 10 ptuni 
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) = U. ( Xt_ ` F ) )
12 1 2 11 syl2anc 
 |-  ( ph -> X_ k e. A U. ( F ` k ) = U. ( Xt_ ` F ) )
13 12 ineq1d 
 |-  ( ph -> ( X_ k e. A U. ( F ` k ) i^i |^|_ x e. A X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) = ( U. ( Xt_ ` F ) i^i |^|_ x e. A X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) )
14 pttop 
 |-  ( ( A e. V /\ F : A --> Top ) -> ( Xt_ ` F ) e. Top )
15 1 2 14 syl2anc 
 |-  ( ph -> ( Xt_ ` F ) e. Top )
16 sseq1 
 |-  ( C = if ( k = x , C , U. ( F ` k ) ) -> ( C C_ U. ( F ` k ) <-> if ( k = x , C , U. ( F ` k ) ) C_ U. ( F ` k ) ) )
17 sseq1 
 |-  ( U. ( F ` k ) = if ( k = x , C , U. ( F ` k ) ) -> ( U. ( F ` k ) C_ U. ( F ` k ) <-> if ( k = x , C , U. ( F ` k ) ) C_ U. ( F ` k ) ) )
18 simpl 
 |-  ( ( C C_ U. ( F ` k ) /\ k = x ) -> C C_ U. ( F ` k ) )
19 ssidd 
 |-  ( ( C C_ U. ( F ` k ) /\ -. k = x ) -> U. ( F ` k ) C_ U. ( F ` k ) )
20 16 17 18 19 ifbothda 
 |-  ( C C_ U. ( F ` k ) -> if ( k = x , C , U. ( F ` k ) ) C_ U. ( F ` k ) )
21 20 ralimi 
 |-  ( A. k e. A C C_ U. ( F ` k ) -> A. k e. A if ( k = x , C , U. ( F ` k ) ) C_ U. ( F ` k ) )
22 ss2ixp 
 |-  ( A. k e. A if ( k = x , C , U. ( F ` k ) ) C_ U. ( F ` k ) -> X_ k e. A if ( k = x , C , U. ( F ` k ) ) C_ X_ k e. A U. ( F ` k ) )
23 7 21 22 3syl 
 |-  ( ph -> X_ k e. A if ( k = x , C , U. ( F ` k ) ) C_ X_ k e. A U. ( F ` k ) )
24 23 adantr 
 |-  ( ( ph /\ x e. A ) -> X_ k e. A if ( k = x , C , U. ( F ` k ) ) C_ X_ k e. A U. ( F ` k ) )
25 12 adantr 
 |-  ( ( ph /\ x e. A ) -> X_ k e. A U. ( F ` k ) = U. ( Xt_ ` F ) )
26 24 25 sseqtrd 
 |-  ( ( ph /\ x e. A ) -> X_ k e. A if ( k = x , C , U. ( F ` k ) ) C_ U. ( Xt_ ` F ) )
27 12 eqcomd 
 |-  ( ph -> U. ( Xt_ ` F ) = X_ k e. A U. ( F ` k ) )
28 27 difeq1d 
 |-  ( ph -> ( U. ( Xt_ ` F ) \ X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) = ( X_ k e. A U. ( F ` k ) \ X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) )
29 28 adantr 
 |-  ( ( ph /\ x e. A ) -> ( U. ( Xt_ ` F ) \ X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) = ( X_ k e. A U. ( F ` k ) \ X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) )
30 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
31 7 adantr 
 |-  ( ( ph /\ x e. A ) -> A. k e. A C C_ U. ( F ` k ) )
32 boxcutc 
 |-  ( ( x e. A /\ A. k e. A C C_ U. ( F ` k ) ) -> ( X_ k e. A U. ( F ` k ) \ X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) = X_ k e. A if ( k = x , ( U. ( F ` k ) \ C ) , U. ( F ` k ) ) )
33 30 31 32 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( X_ k e. A U. ( F ` k ) \ X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) = X_ k e. A if ( k = x , ( U. ( F ` k ) \ C ) , U. ( F ` k ) ) )
34 ixpeq2 
 |-  ( A. k e. A if ( k = x , ( U. ( F ` k ) \ C ) , U. ( F ` k ) ) = if ( k = x , ( U. ( F ` x ) \ [_ x / k ]_ C ) , U. ( F ` k ) ) -> X_ k e. A if ( k = x , ( U. ( F ` k ) \ C ) , U. ( F ` k ) ) = X_ k e. A if ( k = x , ( U. ( F ` x ) \ [_ x / k ]_ C ) , U. ( F ` k ) ) )
35 fveq2 
 |-  ( k = x -> ( F ` k ) = ( F ` x ) )
36 35 unieqd 
 |-  ( k = x -> U. ( F ` k ) = U. ( F ` x ) )
37 csbeq1a 
 |-  ( k = x -> C = [_ x / k ]_ C )
38 36 37 difeq12d 
 |-  ( k = x -> ( U. ( F ` k ) \ C ) = ( U. ( F ` x ) \ [_ x / k ]_ C ) )
39 38 adantl 
 |-  ( ( k e. A /\ k = x ) -> ( U. ( F ` k ) \ C ) = ( U. ( F ` x ) \ [_ x / k ]_ C ) )
40 39 ifeq1da 
 |-  ( k e. A -> if ( k = x , ( U. ( F ` k ) \ C ) , U. ( F ` k ) ) = if ( k = x , ( U. ( F ` x ) \ [_ x / k ]_ C ) , U. ( F ` k ) ) )
41 34 40 mprg 
 |-  X_ k e. A if ( k = x , ( U. ( F ` k ) \ C ) , U. ( F ` k ) ) = X_ k e. A if ( k = x , ( U. ( F ` x ) \ [_ x / k ]_ C ) , U. ( F ` k ) )
42 41 a1i 
 |-  ( ( ph /\ x e. A ) -> X_ k e. A if ( k = x , ( U. ( F ` k ) \ C ) , U. ( F ` k ) ) = X_ k e. A if ( k = x , ( U. ( F ` x ) \ [_ x / k ]_ C ) , U. ( F ` k ) ) )
43 29 33 42 3eqtrd 
 |-  ( ( ph /\ x e. A ) -> ( U. ( Xt_ ` F ) \ X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) = X_ k e. A if ( k = x , ( U. ( F ` x ) \ [_ x / k ]_ C ) , U. ( F ` k ) ) )
44 1 adantr 
 |-  ( ( ph /\ x e. A ) -> A e. V )
45 2 adantr 
 |-  ( ( ph /\ x e. A ) -> F : A --> Top )
46 3 ralrimiva 
 |-  ( ph -> A. k e. A C e. ( Clsd ` ( F ` k ) ) )
47 nfv 
 |-  F/ x C e. ( Clsd ` ( F ` k ) )
48 nfcsb1v 
 |-  F/_ k [_ x / k ]_ C
49 48 nfel1 
 |-  F/ k [_ x / k ]_ C e. ( Clsd ` ( F ` x ) )
50 2fveq3 
 |-  ( k = x -> ( Clsd ` ( F ` k ) ) = ( Clsd ` ( F ` x ) ) )
51 37 50 eleq12d 
 |-  ( k = x -> ( C e. ( Clsd ` ( F ` k ) ) <-> [_ x / k ]_ C e. ( Clsd ` ( F ` x ) ) ) )
52 47 49 51 cbvralw 
 |-  ( A. k e. A C e. ( Clsd ` ( F ` k ) ) <-> A. x e. A [_ x / k ]_ C e. ( Clsd ` ( F ` x ) ) )
53 46 52 sylib 
 |-  ( ph -> A. x e. A [_ x / k ]_ C e. ( Clsd ` ( F ` x ) ) )
54 53 r19.21bi 
 |-  ( ( ph /\ x e. A ) -> [_ x / k ]_ C e. ( Clsd ` ( F ` x ) ) )
55 eqid 
 |-  U. ( F ` x ) = U. ( F ` x )
56 55 cldopn 
 |-  ( [_ x / k ]_ C e. ( Clsd ` ( F ` x ) ) -> ( U. ( F ` x ) \ [_ x / k ]_ C ) e. ( F ` x ) )
57 54 56 syl 
 |-  ( ( ph /\ x e. A ) -> ( U. ( F ` x ) \ [_ x / k ]_ C ) e. ( F ` x ) )
58 44 45 57 ptopn2 
 |-  ( ( ph /\ x e. A ) -> X_ k e. A if ( k = x , ( U. ( F ` x ) \ [_ x / k ]_ C ) , U. ( F ` k ) ) e. ( Xt_ ` F ) )
59 43 58 eqeltrd 
 |-  ( ( ph /\ x e. A ) -> ( U. ( Xt_ ` F ) \ X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) e. ( Xt_ ` F ) )
60 eqid 
 |-  U. ( Xt_ ` F ) = U. ( Xt_ ` F )
61 60 iscld 
 |-  ( ( Xt_ ` F ) e. Top -> ( X_ k e. A if ( k = x , C , U. ( F ` k ) ) e. ( Clsd ` ( Xt_ ` F ) ) <-> ( X_ k e. A if ( k = x , C , U. ( F ` k ) ) C_ U. ( Xt_ ` F ) /\ ( U. ( Xt_ ` F ) \ X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) e. ( Xt_ ` F ) ) ) )
62 15 61 syl 
 |-  ( ph -> ( X_ k e. A if ( k = x , C , U. ( F ` k ) ) e. ( Clsd ` ( Xt_ ` F ) ) <-> ( X_ k e. A if ( k = x , C , U. ( F ` k ) ) C_ U. ( Xt_ ` F ) /\ ( U. ( Xt_ ` F ) \ X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) e. ( Xt_ ` F ) ) ) )
63 62 adantr 
 |-  ( ( ph /\ x e. A ) -> ( X_ k e. A if ( k = x , C , U. ( F ` k ) ) e. ( Clsd ` ( Xt_ ` F ) ) <-> ( X_ k e. A if ( k = x , C , U. ( F ` k ) ) C_ U. ( Xt_ ` F ) /\ ( U. ( Xt_ ` F ) \ X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) e. ( Xt_ ` F ) ) ) )
64 26 59 63 mpbir2and 
 |-  ( ( ph /\ x e. A ) -> X_ k e. A if ( k = x , C , U. ( F ` k ) ) e. ( Clsd ` ( Xt_ ` F ) ) )
65 64 ralrimiva 
 |-  ( ph -> A. x e. A X_ k e. A if ( k = x , C , U. ( F ` k ) ) e. ( Clsd ` ( Xt_ ` F ) ) )
66 60 riincld 
 |-  ( ( ( Xt_ ` F ) e. Top /\ A. x e. A X_ k e. A if ( k = x , C , U. ( F ` k ) ) e. ( Clsd ` ( Xt_ ` F ) ) ) -> ( U. ( Xt_ ` F ) i^i |^|_ x e. A X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) e. ( Clsd ` ( Xt_ ` F ) ) )
67 15 65 66 syl2anc 
 |-  ( ph -> ( U. ( Xt_ ` F ) i^i |^|_ x e. A X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) e. ( Clsd ` ( Xt_ ` F ) ) )
68 13 67 eqeltrd 
 |-  ( ph -> ( X_ k e. A U. ( F ` k ) i^i |^|_ x e. A X_ k e. A if ( k = x , C , U. ( F ` k ) ) ) e. ( Clsd ` ( Xt_ ` F ) ) )
69 9 68 eqeltrd 
 |-  ( ph -> X_ k e. A C e. ( Clsd ` ( Xt_ ` F ) ) )