Metamath Proof Explorer


Theorem txdis1cn

Description: A function is jointly continuous on a discrete left topology iff it is continuous as a function of its right argument, for each fixed left value. (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Hypotheses txdis1cn.x
|- ( ph -> X e. V )
txdis1cn.j
|- ( ph -> J e. ( TopOn ` Y ) )
txdis1cn.k
|- ( ph -> K e. Top )
txdis1cn.f
|- ( ph -> F Fn ( X X. Y ) )
txdis1cn.1
|- ( ( ph /\ x e. X ) -> ( y e. Y |-> ( x F y ) ) e. ( J Cn K ) )
Assertion txdis1cn
|- ( ph -> F e. ( ( ~P X tX J ) Cn K ) )

Proof

Step Hyp Ref Expression
1 txdis1cn.x
 |-  ( ph -> X e. V )
2 txdis1cn.j
 |-  ( ph -> J e. ( TopOn ` Y ) )
3 txdis1cn.k
 |-  ( ph -> K e. Top )
4 txdis1cn.f
 |-  ( ph -> F Fn ( X X. Y ) )
5 txdis1cn.1
 |-  ( ( ph /\ x e. X ) -> ( y e. Y |-> ( x F y ) ) e. ( J Cn K ) )
6 2 adantr
 |-  ( ( ph /\ x e. X ) -> J e. ( TopOn ` Y ) )
7 toptopon2
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
8 3 7 sylib
 |-  ( ph -> K e. ( TopOn ` U. K ) )
9 8 adantr
 |-  ( ( ph /\ x e. X ) -> K e. ( TopOn ` U. K ) )
10 cnf2
 |-  ( ( J e. ( TopOn ` Y ) /\ K e. ( TopOn ` U. K ) /\ ( y e. Y |-> ( x F y ) ) e. ( J Cn K ) ) -> ( y e. Y |-> ( x F y ) ) : Y --> U. K )
11 6 9 5 10 syl3anc
 |-  ( ( ph /\ x e. X ) -> ( y e. Y |-> ( x F y ) ) : Y --> U. K )
12 eqid
 |-  ( y e. Y |-> ( x F y ) ) = ( y e. Y |-> ( x F y ) )
13 12 fmpt
 |-  ( A. y e. Y ( x F y ) e. U. K <-> ( y e. Y |-> ( x F y ) ) : Y --> U. K )
14 11 13 sylibr
 |-  ( ( ph /\ x e. X ) -> A. y e. Y ( x F y ) e. U. K )
15 14 ralrimiva
 |-  ( ph -> A. x e. X A. y e. Y ( x F y ) e. U. K )
16 ffnov
 |-  ( F : ( X X. Y ) --> U. K <-> ( F Fn ( X X. Y ) /\ A. x e. X A. y e. Y ( x F y ) e. U. K ) )
17 4 15 16 sylanbrc
 |-  ( ph -> F : ( X X. Y ) --> U. K )
18 cnvimass
 |-  ( `' F " u ) C_ dom F
19 4 adantr
 |-  ( ( ph /\ u e. K ) -> F Fn ( X X. Y ) )
20 19 fndmd
 |-  ( ( ph /\ u e. K ) -> dom F = ( X X. Y ) )
21 18 20 sseqtrid
 |-  ( ( ph /\ u e. K ) -> ( `' F " u ) C_ ( X X. Y ) )
22 relxp
 |-  Rel ( X X. Y )
23 relss
 |-  ( ( `' F " u ) C_ ( X X. Y ) -> ( Rel ( X X. Y ) -> Rel ( `' F " u ) ) )
24 21 22 23 mpisyl
 |-  ( ( ph /\ u e. K ) -> Rel ( `' F " u ) )
25 elpreima
 |-  ( F Fn ( X X. Y ) -> ( <. x , z >. e. ( `' F " u ) <-> ( <. x , z >. e. ( X X. Y ) /\ ( F ` <. x , z >. ) e. u ) ) )
26 19 25 syl
 |-  ( ( ph /\ u e. K ) -> ( <. x , z >. e. ( `' F " u ) <-> ( <. x , z >. e. ( X X. Y ) /\ ( F ` <. x , z >. ) e. u ) ) )
27 opelxp
 |-  ( <. x , z >. e. ( X X. Y ) <-> ( x e. X /\ z e. Y ) )
28 df-ov
 |-  ( x F z ) = ( F ` <. x , z >. )
29 28 eqcomi
 |-  ( F ` <. x , z >. ) = ( x F z )
30 29 eleq1i
 |-  ( ( F ` <. x , z >. ) e. u <-> ( x F z ) e. u )
31 27 30 anbi12i
 |-  ( ( <. x , z >. e. ( X X. Y ) /\ ( F ` <. x , z >. ) e. u ) <-> ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) )
32 simprll
 |-  ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) -> x e. X )
33 snelpwi
 |-  ( x e. X -> { x } e. ~P X )
34 32 33 syl
 |-  ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) -> { x } e. ~P X )
35 12 mptpreima
 |-  ( `' ( y e. Y |-> ( x F y ) ) " u ) = { y e. Y | ( x F y ) e. u }
36 5 adantrr
 |-  ( ( ph /\ ( x e. X /\ z e. Y ) ) -> ( y e. Y |-> ( x F y ) ) e. ( J Cn K ) )
37 36 ad2ant2r
 |-  ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) -> ( y e. Y |-> ( x F y ) ) e. ( J Cn K ) )
38 simplr
 |-  ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) -> u e. K )
39 cnima
 |-  ( ( ( y e. Y |-> ( x F y ) ) e. ( J Cn K ) /\ u e. K ) -> ( `' ( y e. Y |-> ( x F y ) ) " u ) e. J )
40 37 38 39 syl2anc
 |-  ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) -> ( `' ( y e. Y |-> ( x F y ) ) " u ) e. J )
41 35 40 eqeltrrid
 |-  ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) -> { y e. Y | ( x F y ) e. u } e. J )
42 simprlr
 |-  ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) -> z e. Y )
43 simprr
 |-  ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) -> ( x F z ) e. u )
44 vsnid
 |-  x e. { x }
45 opelxp
 |-  ( <. x , z >. e. ( { x } X. { y e. Y | ( x F y ) e. u } ) <-> ( x e. { x } /\ z e. { y e. Y | ( x F y ) e. u } ) )
46 44 45 mpbiran
 |-  ( <. x , z >. e. ( { x } X. { y e. Y | ( x F y ) e. u } ) <-> z e. { y e. Y | ( x F y ) e. u } )
47 oveq2
 |-  ( y = z -> ( x F y ) = ( x F z ) )
48 47 eleq1d
 |-  ( y = z -> ( ( x F y ) e. u <-> ( x F z ) e. u ) )
49 48 elrab
 |-  ( z e. { y e. Y | ( x F y ) e. u } <-> ( z e. Y /\ ( x F z ) e. u ) )
50 46 49 bitri
 |-  ( <. x , z >. e. ( { x } X. { y e. Y | ( x F y ) e. u } ) <-> ( z e. Y /\ ( x F z ) e. u ) )
51 42 43 50 sylanbrc
 |-  ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) -> <. x , z >. e. ( { x } X. { y e. Y | ( x F y ) e. u } ) )
52 relxp
 |-  Rel ( { x } X. { y e. Y | ( x F y ) e. u } )
53 52 a1i
 |-  ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) -> Rel ( { x } X. { y e. Y | ( x F y ) e. u } ) )
54 opelxp
 |-  ( <. n , m >. e. ( { x } X. { y e. Y | ( x F y ) e. u } ) <-> ( n e. { x } /\ m e. { y e. Y | ( x F y ) e. u } ) )
55 32 snssd
 |-  ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) -> { x } C_ X )
56 55 sselda
 |-  ( ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) /\ n e. { x } ) -> n e. X )
57 56 adantrr
 |-  ( ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) /\ ( n e. { x } /\ m e. { y e. Y | ( x F y ) e. u } ) ) -> n e. X )
58 elrabi
 |-  ( m e. { y e. Y | ( x F y ) e. u } -> m e. Y )
59 58 ad2antll
 |-  ( ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) /\ ( n e. { x } /\ m e. { y e. Y | ( x F y ) e. u } ) ) -> m e. Y )
60 57 59 opelxpd
 |-  ( ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) /\ ( n e. { x } /\ m e. { y e. Y | ( x F y ) e. u } ) ) -> <. n , m >. e. ( X X. Y ) )
61 df-ov
 |-  ( n F m ) = ( F ` <. n , m >. )
62 elsni
 |-  ( n e. { x } -> n = x )
63 62 ad2antrl
 |-  ( ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) /\ ( n e. { x } /\ m e. { y e. Y | ( x F y ) e. u } ) ) -> n = x )
64 63 oveq1d
 |-  ( ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) /\ ( n e. { x } /\ m e. { y e. Y | ( x F y ) e. u } ) ) -> ( n F m ) = ( x F m ) )
65 61 64 eqtr3id
 |-  ( ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) /\ ( n e. { x } /\ m e. { y e. Y | ( x F y ) e. u } ) ) -> ( F ` <. n , m >. ) = ( x F m ) )
66 oveq2
 |-  ( y = m -> ( x F y ) = ( x F m ) )
67 66 eleq1d
 |-  ( y = m -> ( ( x F y ) e. u <-> ( x F m ) e. u ) )
68 67 elrab
 |-  ( m e. { y e. Y | ( x F y ) e. u } <-> ( m e. Y /\ ( x F m ) e. u ) )
69 68 simprbi
 |-  ( m e. { y e. Y | ( x F y ) e. u } -> ( x F m ) e. u )
70 69 ad2antll
 |-  ( ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) /\ ( n e. { x } /\ m e. { y e. Y | ( x F y ) e. u } ) ) -> ( x F m ) e. u )
71 65 70 eqeltrd
 |-  ( ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) /\ ( n e. { x } /\ m e. { y e. Y | ( x F y ) e. u } ) ) -> ( F ` <. n , m >. ) e. u )
72 elpreima
 |-  ( F Fn ( X X. Y ) -> ( <. n , m >. e. ( `' F " u ) <-> ( <. n , m >. e. ( X X. Y ) /\ ( F ` <. n , m >. ) e. u ) ) )
73 4 72 syl
 |-  ( ph -> ( <. n , m >. e. ( `' F " u ) <-> ( <. n , m >. e. ( X X. Y ) /\ ( F ` <. n , m >. ) e. u ) ) )
74 73 ad3antrrr
 |-  ( ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) /\ ( n e. { x } /\ m e. { y e. Y | ( x F y ) e. u } ) ) -> ( <. n , m >. e. ( `' F " u ) <-> ( <. n , m >. e. ( X X. Y ) /\ ( F ` <. n , m >. ) e. u ) ) )
75 60 71 74 mpbir2and
 |-  ( ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) /\ ( n e. { x } /\ m e. { y e. Y | ( x F y ) e. u } ) ) -> <. n , m >. e. ( `' F " u ) )
76 75 ex
 |-  ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) -> ( ( n e. { x } /\ m e. { y e. Y | ( x F y ) e. u } ) -> <. n , m >. e. ( `' F " u ) ) )
77 54 76 syl5bi
 |-  ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) -> ( <. n , m >. e. ( { x } X. { y e. Y | ( x F y ) e. u } ) -> <. n , m >. e. ( `' F " u ) ) )
78 53 77 relssdv
 |-  ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) -> ( { x } X. { y e. Y | ( x F y ) e. u } ) C_ ( `' F " u ) )
79 xpeq1
 |-  ( a = { x } -> ( a X. b ) = ( { x } X. b ) )
80 79 eleq2d
 |-  ( a = { x } -> ( <. x , z >. e. ( a X. b ) <-> <. x , z >. e. ( { x } X. b ) ) )
81 79 sseq1d
 |-  ( a = { x } -> ( ( a X. b ) C_ ( `' F " u ) <-> ( { x } X. b ) C_ ( `' F " u ) ) )
82 80 81 anbi12d
 |-  ( a = { x } -> ( ( <. x , z >. e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) <-> ( <. x , z >. e. ( { x } X. b ) /\ ( { x } X. b ) C_ ( `' F " u ) ) ) )
83 xpeq2
 |-  ( b = { y e. Y | ( x F y ) e. u } -> ( { x } X. b ) = ( { x } X. { y e. Y | ( x F y ) e. u } ) )
84 83 eleq2d
 |-  ( b = { y e. Y | ( x F y ) e. u } -> ( <. x , z >. e. ( { x } X. b ) <-> <. x , z >. e. ( { x } X. { y e. Y | ( x F y ) e. u } ) ) )
85 83 sseq1d
 |-  ( b = { y e. Y | ( x F y ) e. u } -> ( ( { x } X. b ) C_ ( `' F " u ) <-> ( { x } X. { y e. Y | ( x F y ) e. u } ) C_ ( `' F " u ) ) )
86 84 85 anbi12d
 |-  ( b = { y e. Y | ( x F y ) e. u } -> ( ( <. x , z >. e. ( { x } X. b ) /\ ( { x } X. b ) C_ ( `' F " u ) ) <-> ( <. x , z >. e. ( { x } X. { y e. Y | ( x F y ) e. u } ) /\ ( { x } X. { y e. Y | ( x F y ) e. u } ) C_ ( `' F " u ) ) ) )
87 82 86 rspc2ev
 |-  ( ( { x } e. ~P X /\ { y e. Y | ( x F y ) e. u } e. J /\ ( <. x , z >. e. ( { x } X. { y e. Y | ( x F y ) e. u } ) /\ ( { x } X. { y e. Y | ( x F y ) e. u } ) C_ ( `' F " u ) ) ) -> E. a e. ~P X E. b e. J ( <. x , z >. e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) )
88 34 41 51 78 87 syl112anc
 |-  ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) -> E. a e. ~P X E. b e. J ( <. x , z >. e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) )
89 opex
 |-  <. x , z >. e. _V
90 eleq1
 |-  ( v = <. x , z >. -> ( v e. ( a X. b ) <-> <. x , z >. e. ( a X. b ) ) )
91 90 anbi1d
 |-  ( v = <. x , z >. -> ( ( v e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) <-> ( <. x , z >. e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) ) )
92 91 2rexbidv
 |-  ( v = <. x , z >. -> ( E. a e. ~P X E. b e. J ( v e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) <-> E. a e. ~P X E. b e. J ( <. x , z >. e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) ) )
93 89 92 elab
 |-  ( <. x , z >. e. { v | E. a e. ~P X E. b e. J ( v e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) } <-> E. a e. ~P X E. b e. J ( <. x , z >. e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) )
94 88 93 sylibr
 |-  ( ( ( ph /\ u e. K ) /\ ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) ) -> <. x , z >. e. { v | E. a e. ~P X E. b e. J ( v e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) } )
95 94 ex
 |-  ( ( ph /\ u e. K ) -> ( ( ( x e. X /\ z e. Y ) /\ ( x F z ) e. u ) -> <. x , z >. e. { v | E. a e. ~P X E. b e. J ( v e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) } ) )
96 31 95 syl5bi
 |-  ( ( ph /\ u e. K ) -> ( ( <. x , z >. e. ( X X. Y ) /\ ( F ` <. x , z >. ) e. u ) -> <. x , z >. e. { v | E. a e. ~P X E. b e. J ( v e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) } ) )
97 26 96 sylbid
 |-  ( ( ph /\ u e. K ) -> ( <. x , z >. e. ( `' F " u ) -> <. x , z >. e. { v | E. a e. ~P X E. b e. J ( v e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) } ) )
98 24 97 relssdv
 |-  ( ( ph /\ u e. K ) -> ( `' F " u ) C_ { v | E. a e. ~P X E. b e. J ( v e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) } )
99 ssabral
 |-  ( ( `' F " u ) C_ { v | E. a e. ~P X E. b e. J ( v e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) } <-> A. v e. ( `' F " u ) E. a e. ~P X E. b e. J ( v e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) )
100 98 99 sylib
 |-  ( ( ph /\ u e. K ) -> A. v e. ( `' F " u ) E. a e. ~P X E. b e. J ( v e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) )
101 distopon
 |-  ( X e. V -> ~P X e. ( TopOn ` X ) )
102 1 101 syl
 |-  ( ph -> ~P X e. ( TopOn ` X ) )
103 102 adantr
 |-  ( ( ph /\ u e. K ) -> ~P X e. ( TopOn ` X ) )
104 2 adantr
 |-  ( ( ph /\ u e. K ) -> J e. ( TopOn ` Y ) )
105 eltx
 |-  ( ( ~P X e. ( TopOn ` X ) /\ J e. ( TopOn ` Y ) ) -> ( ( `' F " u ) e. ( ~P X tX J ) <-> A. v e. ( `' F " u ) E. a e. ~P X E. b e. J ( v e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) ) )
106 103 104 105 syl2anc
 |-  ( ( ph /\ u e. K ) -> ( ( `' F " u ) e. ( ~P X tX J ) <-> A. v e. ( `' F " u ) E. a e. ~P X E. b e. J ( v e. ( a X. b ) /\ ( a X. b ) C_ ( `' F " u ) ) ) )
107 100 106 mpbird
 |-  ( ( ph /\ u e. K ) -> ( `' F " u ) e. ( ~P X tX J ) )
108 107 ralrimiva
 |-  ( ph -> A. u e. K ( `' F " u ) e. ( ~P X tX J ) )
109 txtopon
 |-  ( ( ~P X e. ( TopOn ` X ) /\ J e. ( TopOn ` Y ) ) -> ( ~P X tX J ) e. ( TopOn ` ( X X. Y ) ) )
110 102 2 109 syl2anc
 |-  ( ph -> ( ~P X tX J ) e. ( TopOn ` ( X X. Y ) ) )
111 iscn
 |-  ( ( ( ~P X tX J ) e. ( TopOn ` ( X X. Y ) ) /\ K e. ( TopOn ` U. K ) ) -> ( F e. ( ( ~P X tX J ) Cn K ) <-> ( F : ( X X. Y ) --> U. K /\ A. u e. K ( `' F " u ) e. ( ~P X tX J ) ) ) )
112 110 8 111 syl2anc
 |-  ( ph -> ( F e. ( ( ~P X tX J ) Cn K ) <-> ( F : ( X X. Y ) --> U. K /\ A. u e. K ( `' F " u ) e. ( ~P X tX J ) ) ) )
113 17 108 112 mpbir2and
 |-  ( ph -> F e. ( ( ~P X tX J ) Cn K ) )