This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐾 ( 𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) ) )