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