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

Metamath Proof Explorer

Theorem tmdcn2

Description: Write out the definition of continuity of +g explicitly. (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Hypotheses tmdcn2.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
tmdcn2.2 ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
tmdcn2.3 ⊢ + = ( +g ‘ 𝐺 )
Assertion tmdcn2 ( ( ( 𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) ) → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀ 𝑥 ∈ 𝑢 ∀ 𝑦 ∈ 𝑣 ( 𝑥 + 𝑦 ) ∈ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 tmdcn2.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 tmdcn2.2 ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
3 tmdcn2.3 ⊢ + = ( +g ‘ 𝐺 )
4 2 1 tmdtopon ⊢ ( 𝐺 ∈ TopMnd → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
5 4 ad2antrr ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) ) → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
6 eqid ⊢ ( +𝑓 ‘ 𝐺 ) = ( +𝑓 ‘ 𝐺 )
7 2 6 tmdcn ⊢ ( 𝐺 ∈ TopMnd → ( +𝑓 ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
8 7 ad2antrr ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) ) → ( +𝑓 ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
9 simpr1 ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) ) → 𝑋 ∈ 𝐵 )
10 simpr2 ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) ) → 𝑌 ∈ 𝐵 )
11 9 10 opelxpd ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
12 txtopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ∧ 𝐽 ∈ ( TopOn ‘ 𝐵 ) ) → ( 𝐽 ×t 𝐽 ) ∈ ( TopOn ‘ ( 𝐵 × 𝐵 ) ) )
13 5 5 12 syl2anc ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) ) → ( 𝐽 ×t 𝐽 ) ∈ ( TopOn ‘ ( 𝐵 × 𝐵 ) ) )
14 toponuni ⊢ ( ( 𝐽 ×t 𝐽 ) ∈ ( TopOn ‘ ( 𝐵 × 𝐵 ) ) → ( 𝐵 × 𝐵 ) = ∪ ( 𝐽 ×t 𝐽 ) )
15 13 14 syl ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) ) → ( 𝐵 × 𝐵 ) = ∪ ( 𝐽 ×t 𝐽 ) )
16 11 15 eleqtrd ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ∪ ( 𝐽 ×t 𝐽 ) )
17 eqid ⊢ ∪ ( 𝐽 ×t 𝐽 ) = ∪ ( 𝐽 ×t 𝐽 )
18 17 cncnpi ⊢ ( ( ( +𝑓 ‘ 𝐺 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ∧ ⟨ 𝑋 , 𝑌 ⟩ ∈ ∪ ( 𝐽 ×t 𝐽 ) ) → ( +𝑓 ‘ 𝐺 ) ∈ ( ( ( 𝐽 ×t 𝐽 ) CnP 𝐽 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
19 8 16 18 syl2anc ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) ) → ( +𝑓 ‘ 𝐺 ) ∈ ( ( ( 𝐽 ×t 𝐽 ) CnP 𝐽 ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
20 simplr ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) ) → 𝑈 ∈ 𝐽 )
21 1 3 6 plusfval ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( +𝑓 ‘ 𝐺 ) 𝑌 ) = ( 𝑋 + 𝑌 ) )
22 9 10 21 syl2anc ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) ) → ( 𝑋 ( +𝑓 ‘ 𝐺 ) 𝑌 ) = ( 𝑋 + 𝑌 ) )
23 simpr3 ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝑈 )
24 22 23 eqeltrd ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) ) → ( 𝑋 ( +𝑓 ‘ 𝐺 ) 𝑌 ) ∈ 𝑈 )
25 5 5 19 20 9 10 24 txcnpi ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) ) → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ ( +𝑓 ‘ 𝐺 ) “ 𝑈 ) ) )
26 dfss3 ⊢ ( ( 𝑢 × 𝑣 ) ⊆ ( ◡ ( +𝑓 ‘ 𝐺 ) “ 𝑈 ) ↔ ∀ 𝑧 ∈ ( 𝑢 × 𝑣 ) 𝑧 ∈ ( ◡ ( +𝑓 ‘ 𝐺 ) “ 𝑈 ) )
27 eleq1 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ ( ◡ ( +𝑓 ‘ 𝐺 ) “ 𝑈 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( +𝑓 ‘ 𝐺 ) “ 𝑈 ) ) )
28 1 6 plusffn ⊢ ( +𝑓 ‘ 𝐺 ) Fn ( 𝐵 × 𝐵 )
29 elpreima ⊢ ( ( +𝑓 ‘ 𝐺 ) Fn ( 𝐵 × 𝐵 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( +𝑓 ‘ 𝐺 ) “ 𝑈 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) ∧ ( ( +𝑓 ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝑈 ) ) )
30 28 29 ax-mp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ ( +𝑓 ‘ 𝐺 ) “ 𝑈 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) ∧ ( ( +𝑓 ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝑈 ) )
31 27 30 bitrdi ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ ( ◡ ( +𝑓 ‘ 𝐺 ) “ 𝑈 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) ∧ ( ( +𝑓 ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝑈 ) ) )
32 31 ralxp ⊢ ( ∀ 𝑧 ∈ ( 𝑢 × 𝑣 ) 𝑧 ∈ ( ◡ ( +𝑓 ‘ 𝐺 ) “ 𝑈 ) ↔ ∀ 𝑥 ∈ 𝑢 ∀ 𝑦 ∈ 𝑣 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) ∧ ( ( +𝑓 ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝑈 ) )
33 26 32 bitri ⊢ ( ( 𝑢 × 𝑣 ) ⊆ ( ◡ ( +𝑓 ‘ 𝐺 ) “ 𝑈 ) ↔ ∀ 𝑥 ∈ 𝑢 ∀ 𝑦 ∈ 𝑣 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) ∧ ( ( +𝑓 ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝑈 ) )
34 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
35 df-ov ⊢ ( 𝑥 ( +𝑓 ‘ 𝐺 ) 𝑦 ) = ( ( +𝑓 ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ )
36 1 3 6 plusfval ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +𝑓 ‘ 𝐺 ) 𝑦 ) = ( 𝑥 + 𝑦 ) )
37 35 36 eqtr3id ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( +𝑓 ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 𝑥 + 𝑦 ) )
38 34 37 sylbi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) → ( ( +𝑓 ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 𝑥 + 𝑦 ) )
39 38 eleq1d ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) → ( ( ( +𝑓 ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝑈 ↔ ( 𝑥 + 𝑦 ) ∈ 𝑈 ) )
40 39 biimpa ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) ∧ ( ( +𝑓 ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝑈 ) → ( 𝑥 + 𝑦 ) ∈ 𝑈 )
41 40 2ralimi ⊢ ( ∀ 𝑥 ∈ 𝑢 ∀ 𝑦 ∈ 𝑣 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐵 ) ∧ ( ( +𝑓 ‘ 𝐺 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ 𝑈 ) → ∀ 𝑥 ∈ 𝑢 ∀ 𝑦 ∈ 𝑣 ( 𝑥 + 𝑦 ) ∈ 𝑈 )
42 33 41 sylbi ⊢ ( ( 𝑢 × 𝑣 ) ⊆ ( ◡ ( +𝑓 ‘ 𝐺 ) “ 𝑈 ) → ∀ 𝑥 ∈ 𝑢 ∀ 𝑦 ∈ 𝑣 ( 𝑥 + 𝑦 ) ∈ 𝑈 )
43 42 3anim3i ⊢ ( ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ ( +𝑓 ‘ 𝐺 ) “ 𝑈 ) ) → ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀ 𝑥 ∈ 𝑢 ∀ 𝑦 ∈ 𝑣 ( 𝑥 + 𝑦 ) ∈ 𝑈 ) )
44 43 reximi ⊢ ( ∃ 𝑣 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ ( +𝑓 ‘ 𝐺 ) “ 𝑈 ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀ 𝑥 ∈ 𝑢 ∀ 𝑦 ∈ 𝑣 ( 𝑥 + 𝑦 ) ∈ 𝑈 ) )
45 44 reximi ⊢ ( ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ ( ◡ ( +𝑓 ‘ 𝐺 ) “ 𝑈 ) ) → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀ 𝑥 ∈ 𝑢 ∀ 𝑦 ∈ 𝑣 ( 𝑥 + 𝑦 ) ∈ 𝑈 ) )
46 25 45 syl ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) ) → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀ 𝑥 ∈ 𝑢 ∀ 𝑦 ∈ 𝑣 ( 𝑥 + 𝑦 ) ∈ 𝑈 ) )