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	$⊢ φ \to X \in V$
	txdis1cn.j	$⊢ φ \to J \in TopOn (Y)$
	txdis1cn.k	$⊢ φ \to K \in Top$
	txdis1cn.f	$⊢ φ \to F Fn (X \times Y)$
	txdis1cn.1	$⊢ (φ \land x \in X) \to (y \in Y ⟼ x F y) \in (J Cn K)$
Assertion	txdis1cn	$⊢ φ \to F \in ((𝒫 X \times_{t} J) Cn K)$

Proof

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

Metamath Proof Explorer

Theorem txdis1cn

Proof