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 ∧ 𝑈 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 + 𝑌 ) ∈ 𝑈 ) ) → ∃ 𝑢 ∈ 𝐽 ∃ 𝑣 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀ 𝑥 ∈ 𝑢 ∀ 𝑦 ∈ 𝑣 ( 𝑥 + 𝑦 ) ∈ 𝑈 ) )