Theorem txcnpi

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

	Ref	Expression
Hypotheses	txcnpi.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	txcnpi.2	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
	txcnpi.3	⊢ ( 𝜑 → 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
	txcnpi.4	⊢ ( 𝜑 → 𝑈 ∈ 𝐿 )
	txcnpi.5	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
	txcnpi.6	⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
	txcnpi.7	⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) ∈ 𝑈 )
Assertion	txcnpi	⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) )

Proof

Step	Hyp	Ref	Expression
1		txcnpi.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		txcnpi.2	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3		txcnpi.3	⊢ ( 𝜑 → 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
4		txcnpi.4	⊢ ( 𝜑 → 𝑈 ∈ 𝐿 )
5		txcnpi.5	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
6		txcnpi.6	⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
7		txcnpi.7	⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) ∈ 𝑈 )
8		df-ov	⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
9	8 7	eqeltrrid	⊢ ( 𝜑 → ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ 𝑈 )
10		cnpimaex	⊢ ( ( 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∧ 𝑈 ∈ 𝐿 ∧ ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ 𝑈 ) → ∃ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑤 ∧ ( 𝐹 “ 𝑤 ) ⊆ 𝑈 ) )
11	3 4 9 10	syl3anc	⊢ ( 𝜑 → ∃ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑤 ∧ ( 𝐹 “ 𝑤 ) ⊆ 𝑈 ) )
12		eqid	⊢ ∪ ( 𝐽 ×t 𝐾 ) = ∪ ( 𝐽 ×t 𝐾 )
13		eqid	⊢ ∪ 𝐿 = ∪ 𝐿
14	12 13	cnpf	⊢ ( 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) → 𝐹 : ∪ ( 𝐽 ×t 𝐾 ) ⟶ ∪ 𝐿 )
15	3 14	syl	⊢ ( 𝜑 → 𝐹 : ∪ ( 𝐽 ×t 𝐾 ) ⟶ ∪ 𝐿 )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ) → 𝐹 : ∪ ( 𝐽 ×t 𝐾 ) ⟶ ∪ 𝐿 )
17	16	ffund	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ) → Fun 𝐹 )
18		elssuni	⊢ ( 𝑤 ∈ ( 𝐽 ×t 𝐾 ) → 𝑤 ⊆ ∪ ( 𝐽 ×t 𝐾 ) )
19	15	fdmd	⊢ ( 𝜑 → dom 𝐹 = ∪ ( 𝐽 ×t 𝐾 ) )
20	19	sseq2d	⊢ ( 𝜑 → ( 𝑤 ⊆ dom 𝐹 ↔ 𝑤 ⊆ ∪ ( 𝐽 ×t 𝐾 ) ) )
21	20	biimpar	⊢ ( ( 𝜑 ∧ 𝑤 ⊆ ∪ ( 𝐽 ×t 𝐾 ) ) → 𝑤 ⊆ dom 𝐹 )
22	18 21	sylan2	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ) → 𝑤 ⊆ dom 𝐹 )
23		funimass3	⊢ ( ( Fun 𝐹 ∧ 𝑤 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝑤 ) ⊆ 𝑈 ↔ 𝑤 ⊆ ( ◡ 𝐹 “ 𝑈 ) ) )
24	17 22 23	syl2anc	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ) → ( ( 𝐹 “ 𝑤 ) ⊆ 𝑈 ↔ 𝑤 ⊆ ( ◡ 𝐹 “ 𝑈 ) ) )
25	24	anbi2d	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑤 ∧ ( 𝐹 “ 𝑤 ) ⊆ 𝑈 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ ( ◡ 𝐹 “ 𝑈 ) ) ) )
26		eltx	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ↔ ∀ 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( 𝑧 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) )
27	1 2 26	syl2anc	⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ↔ ∀ 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( 𝑧 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) )
28	27	biimpa	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ) → ∀ 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( 𝑧 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) )
29		eleq1	⊢ ( 𝑧 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑧 ∈ ( 𝑢 × 𝑣 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑢 × 𝑣 ) ) )
30	29	anbi1d	⊢ ( 𝑧 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 𝑧 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) )
31	30	2rexbidv	⊢ ( 𝑧 = ⟨ 𝐴 , 𝐵 ⟩ → ( ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( 𝑧 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ↔ ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) )
32	31	rspccv	⊢ ( ∀ 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( 𝑧 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑤 → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ) )
33		sstr2	⊢ ( ( 𝑢 × 𝑣 ) ⊆ 𝑤 → ( 𝑤 ⊆ ( ◡ 𝐹 “ 𝑈 ) → ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) )
34	33	com12	⊢ ( 𝑤 ⊆ ( ◡ 𝐹 “ 𝑈 ) → ( ( 𝑢 × 𝑣 ) ⊆ 𝑤 → ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) )
35	34	anim2d	⊢ ( 𝑤 ⊆ ( ◡ 𝐹 “ 𝑈 ) → ( ( ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) → ( ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) ) )
36		opelxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑢 × 𝑣 ) ↔ ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ) )
37	36	anbi1i	⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) ↔ ( ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) )
38		df-3an	⊢ ( ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) ↔ ( ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) )
39	35 37 38	3imtr4g	⊢ ( 𝑤 ⊆ ( ◡ 𝐹 “ 𝑈 ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) → ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) ) )
40	39	reximdv	⊢ ( 𝑤 ⊆ ( ◡ 𝐹 “ 𝑈 ) → ( ∃ 𝑣 ∈ 𝐾 ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) → ∃ 𝑣 ∈ 𝐾 ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) ) )
41	40	reximdv	⊢ ( 𝑤 ⊆ ( ◡ 𝐹 “ 𝑈 ) → ( ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) ) )
42	41	com12	⊢ ( ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) → ( 𝑤 ⊆ ( ◡ 𝐹 “ 𝑈 ) → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) ) )
43	32 42	syl6	⊢ ( ∀ 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( 𝑧 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑤 → ( 𝑤 ⊆ ( ◡ 𝐹 “ 𝑈 ) → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) ) ) )
44	43	impd	⊢ ( ∀ 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( 𝑧 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑤 ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ ( ◡ 𝐹 “ 𝑈 ) ) → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) ) )
45	28 44	syl	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑤 ∧ 𝑤 ⊆ ( ◡ 𝐹 “ 𝑈 ) ) → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) ) )
46	25 45	sylbid	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑤 ∧ ( 𝐹 “ 𝑤 ) ⊆ 𝑈 ) → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) ) )
47	46	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ( 𝐽 ×t 𝐾 ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑤 ∧ ( 𝐹 “ 𝑤 ) ⊆ 𝑈 ) → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) ) )
48	11 47	mpd	⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) )