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