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 φ X V
txdis1cn.j φ J TopOn Y
txdis1cn.k φ K Top
txdis1cn.f φ F Fn X × Y
txdis1cn.1 φ x X y Y x F y J Cn K
Assertion txdis1cn φ F 𝒫 X × t J Cn K

Proof

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