txcnpi

Description: Continuity of a two-argument function at a point. (Contributed by Mario Carneiro, 20-Sep-2015)

	Ref	Expression
Hypotheses	txcnpi.1	$⊢ φ \to J \in TopOn (X)$
	txcnpi.2	$⊢ φ \to K \in TopOn (Y)$
	txcnpi.3	$⊢ φ \to F \in ((J \times_{t} K) CnP L) (⟨A, B⟩)$
	txcnpi.4	$⊢ φ \to U \in L$
	txcnpi.5	$⊢ φ \to A \in X$
	txcnpi.6	$⊢ φ \to B \in Y$
	txcnpi.7	$⊢ φ \to A F B \in U$
Assertion	txcnpi	$⊢ φ \to \exists u \in J \exists v \in K (A \in u \land B \in v \land u \times v \subseteq F^{-1} [U])$

Proof

Step	Hyp	Ref	Expression
1		txcnpi.1	$⊢ φ \to J \in TopOn (X)$
2		txcnpi.2	$⊢ φ \to K \in TopOn (Y)$
3		txcnpi.3	$⊢ φ \to F \in ((J \times_{t} K) CnP L) (⟨A, B⟩)$
4		txcnpi.4	$⊢ φ \to U \in L$
5		txcnpi.5	$⊢ φ \to A \in X$
6		txcnpi.6	$⊢ φ \to B \in Y$
7		txcnpi.7	$⊢ φ \to A F B \in U$
8		df-ov	$⊢ A F B = F (⟨A, B⟩)$
9	8 7	eqeltrrid	$⊢ φ \to F (⟨A, B⟩) \in U$
10		cnpimaex	$⊢ (F \in ((J \times_{t} K) CnP L) (⟨A, B⟩) \land U \in L \land F (⟨A, B⟩) \in U) \to \exists w \in (J \times_{t} K) (⟨A, B⟩ \in w \land F [w] \subseteq U)$
11	3 4 9 10	syl3anc	$⊢ φ \to \exists w \in (J \times_{t} K) (⟨A, B⟩ \in w \land F [w] \subseteq U)$
12		eqid	$⊢ ⋃ (J \times_{t} K) = ⋃ (J \times_{t} K)$
13		eqid	$⊢ ⋃ L = ⋃ L$
14	12 13	cnpf	$⊢ F \in ((J \times_{t} K) CnP L) (⟨A, B⟩) \to F : ⋃ (J \times_{t} K) ⟶ ⋃ L$
15	3 14	syl	$⊢ φ \to F : ⋃ (J \times_{t} K) ⟶ ⋃ L$
16	15	adantr	$⊢ (φ \land w \in (J \times_{t} K)) \to F : ⋃ (J \times_{t} K) ⟶ ⋃ L$
17	16	ffund	$⊢ (φ \land w \in (J \times_{t} K)) \to Fun F$
18		elssuni	$⊢ w \in (J \times_{t} K) \to w \subseteq ⋃ (J \times_{t} K)$
19	15	fdmd	$⊢ φ \to dom F = ⋃ (J \times_{t} K)$
20	19	sseq2d	$⊢ φ \to (w \subseteq dom F \leftrightarrow w \subseteq ⋃ (J \times_{t} K))$
21	20	biimpar	$⊢ (φ \land w \subseteq ⋃ (J \times_{t} K)) \to w \subseteq dom F$
22	18 21	sylan2	$⊢ (φ \land w \in (J \times_{t} K)) \to w \subseteq dom F$
23		funimass3	$⊢ (Fun F \land w \subseteq dom F) \to (F [w] \subseteq U \leftrightarrow w \subseteq F^{-1} [U])$
24	17 22 23	syl2anc	$⊢ (φ \land w \in (J \times_{t} K)) \to (F [w] \subseteq U \leftrightarrow w \subseteq F^{-1} [U])$
25	24	anbi2d	$⊢ (φ \land w \in (J \times_{t} K)) \to ((⟨A, B⟩ \in w \land F [w] \subseteq U) \leftrightarrow (⟨A, B⟩ \in w \land w \subseteq F^{-1} [U]))$
26		eltx	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (w \in (J \times_{t} K) \leftrightarrow \forall z \in w \exists u \in J \exists v \in K (z \in (u \times v) \land u \times v \subseteq w))$
27	1 2 26	syl2anc	$⊢ φ \to (w \in (J \times_{t} K) \leftrightarrow \forall z \in w \exists u \in J \exists v \in K (z \in (u \times v) \land u \times v \subseteq w))$
28	27	biimpa	$⊢ (φ \land w \in (J \times_{t} K)) \to \forall z \in w \exists u \in J \exists v \in K (z \in (u \times v) \land u \times v \subseteq w)$
29		eleq1	$⊢ z = ⟨A, B⟩ \to (z \in (u \times v) \leftrightarrow ⟨A, B⟩ \in (u \times v))$
30	29	anbi1d	$⊢ z = ⟨A, B⟩ \to ((z \in (u \times v) \land u \times v \subseteq w) \leftrightarrow (⟨A, B⟩ \in (u \times v) \land u \times v \subseteq w))$
31	30	2rexbidv	$⊢ z = ⟨A, B⟩ \to (\exists u \in J \exists v \in K (z \in (u \times v) \land u \times v \subseteq w) \leftrightarrow \exists u \in J \exists v \in K (⟨A, B⟩ \in (u \times v) \land u \times v \subseteq w))$
32	31	rspccv	$⊢ \forall z \in w \exists u \in J \exists v \in K (z \in (u \times v) \land u \times v \subseteq w) \to (⟨A, B⟩ \in w \to \exists u \in J \exists v \in K (⟨A, B⟩ \in (u \times v) \land u \times v \subseteq w))$
33		sstr2	$⊢ u \times v \subseteq w \to (w \subseteq F^{-1} [U] \to u \times v \subseteq F^{-1} [U])$
34	33	com12	$⊢ w \subseteq F^{-1} [U] \to (u \times v \subseteq w \to u \times v \subseteq F^{-1} [U])$
35	34	anim2d	$⊢ w \subseteq F^{-1} [U] \to (((A \in u \land B \in v) \land u \times v \subseteq w) \to ((A \in u \land B \in v) \land u \times v \subseteq F^{-1} [U]))$
36		opelxp	$⊢ ⟨A, B⟩ \in (u \times v) \leftrightarrow (A \in u \land B \in v)$
37	36	anbi1i	$⊢ (⟨A, B⟩ \in (u \times v) \land u \times v \subseteq w) \leftrightarrow ((A \in u \land B \in v) \land u \times v \subseteq w)$
38		df-3an	$⊢ (A \in u \land B \in v \land u \times v \subseteq F^{-1} [U]) \leftrightarrow ((A \in u \land B \in v) \land u \times v \subseteq F^{-1} [U])$
39	35 37 38	3imtr4g	$⊢ w \subseteq F^{-1} [U] \to ((⟨A, B⟩ \in (u \times v) \land u \times v \subseteq w) \to (A \in u \land B \in v \land u \times v \subseteq F^{-1} [U]))$
40	39	reximdv	$⊢ w \subseteq F^{-1} [U] \to (\exists v \in K (⟨A, B⟩ \in (u \times v) \land u \times v \subseteq w) \to \exists v \in K (A \in u \land B \in v \land u \times v \subseteq F^{-1} [U]))$
41	40	reximdv	$⊢ w \subseteq F^{-1} [U] \to (\exists u \in J \exists v \in K (⟨A, B⟩ \in (u \times v) \land u \times v \subseteq w) \to \exists u \in J \exists v \in K (A \in u \land B \in v \land u \times v \subseteq F^{-1} [U]))$
42	41	com12	$⊢ \exists u \in J \exists v \in K (⟨A, B⟩ \in (u \times v) \land u \times v \subseteq w) \to (w \subseteq F^{-1} [U] \to \exists u \in J \exists v \in K (A \in u \land B \in v \land u \times v \subseteq F^{-1} [U]))$
43	32 42	syl6	$⊢ \forall z \in w \exists u \in J \exists v \in K (z \in (u \times v) \land u \times v \subseteq w) \to (⟨A, B⟩ \in w \to (w \subseteq F^{-1} [U] \to \exists u \in J \exists v \in K (A \in u \land B \in v \land u \times v \subseteq F^{-1} [U])))$
44	43	impd	$⊢ \forall z \in w \exists u \in J \exists v \in K (z \in (u \times v) \land u \times v \subseteq w) \to ((⟨A, B⟩ \in w \land w \subseteq F^{-1} [U]) \to \exists u \in J \exists v \in K (A \in u \land B \in v \land u \times v \subseteq F^{-1} [U]))$
45	28 44	syl	$⊢ (φ \land w \in (J \times_{t} K)) \to ((⟨A, B⟩ \in w \land w \subseteq F^{-1} [U]) \to \exists u \in J \exists v \in K (A \in u \land B \in v \land u \times v \subseteq F^{-1} [U]))$
46	25 45	sylbid	$⊢ (φ \land w \in (J \times_{t} K)) \to ((⟨A, B⟩ \in w \land F [w] \subseteq U) \to \exists u \in J \exists v \in K (A \in u \land B \in v \land u \times v \subseteq F^{-1} [U]))$
47	46	rexlimdva	$⊢ φ \to (\exists w \in (J \times_{t} K) (⟨A, B⟩ \in w \land F [w] \subseteq U) \to \exists u \in J \exists v \in K (A \in u \land B \in v \land u \times v \subseteq F^{-1} [U]))$
48	11 47	mpd	$⊢ φ \to \exists u \in J \exists v \in K (A \in u \land B \in v \land u \times v \subseteq F^{-1} [U])$

Metamath Proof Explorer

Theorem txcnpi

Proof