tmdcn2

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

	Ref	Expression
Hypotheses	tmdcn2.1	$⊢ B = {Base}_{G}$
	tmdcn2.2	$⊢ J = TopOpen (G)$
	tmdcn2.3	$⊢ \underset{˙}{+} = +_{G}$
Assertion	tmdcn2	$⊢ ((G \in TopMnd \land U \in J) \land (X \in B \land Y \in B \land X \underset{˙}{+} Y \in U)) \to \exists u \in J \exists v \in J (X \in u \land Y \in v \land \forall x \in u \forall y \in v x \underset{˙}{+} y \in U)$

Proof

Step	Hyp	Ref	Expression
1		tmdcn2.1	$⊢ B = {Base}_{G}$
2		tmdcn2.2	$⊢ J = TopOpen (G)$
3		tmdcn2.3	$⊢ \underset{˙}{+} = +_{G}$
4	2 1	tmdtopon	$⊢ G \in TopMnd \to J \in TopOn (B)$
5	4	ad2antrr	$⊢ ((G \in TopMnd \land U \in J) \land (X \in B \land Y \in B \land X \underset{˙}{+} Y \in U)) \to J \in TopOn (B)$
6		eqid	$⊢ +_{𝑓} (G) = +_{𝑓} (G)$
7	2 6	tmdcn	$⊢ G \in TopMnd \to +_{𝑓} (G) \in ((J \times_{t} J) Cn J)$
8	7	ad2antrr	$⊢ ((G \in TopMnd \land U \in J) \land (X \in B \land Y \in B \land X \underset{˙}{+} Y \in U)) \to +_{𝑓} (G) \in ((J \times_{t} J) Cn J)$
9		simpr1	$⊢ ((G \in TopMnd \land U \in J) \land (X \in B \land Y \in B \land X \underset{˙}{+} Y \in U)) \to X \in B$
10		simpr2	$⊢ ((G \in TopMnd \land U \in J) \land (X \in B \land Y \in B \land X \underset{˙}{+} Y \in U)) \to Y \in B$
11	9 10	opelxpd	$⊢ ((G \in TopMnd \land U \in J) \land (X \in B \land Y \in B \land X \underset{˙}{+} Y \in U)) \to ⟨X, Y⟩ \in (B \times B)$
12		txtopon	$⊢ (J \in TopOn (B) \land J \in TopOn (B)) \to J \times_{t} J \in TopOn (B \times B)$
13	5 5 12	syl2anc	$⊢ ((G \in TopMnd \land U \in J) \land (X \in B \land Y \in B \land X \underset{˙}{+} Y \in U)) \to J \times_{t} J \in TopOn (B \times B)$
14		toponuni	$⊢ J \times_{t} J \in TopOn (B \times B) \to B \times B = ⋃ (J \times_{t} J)$
15	13 14	syl	$⊢ ((G \in TopMnd \land U \in J) \land (X \in B \land Y \in B \land X \underset{˙}{+} Y \in U)) \to B \times B = ⋃ (J \times_{t} J)$
16	11 15	eleqtrd	$⊢ ((G \in TopMnd \land U \in J) \land (X \in B \land Y \in B \land X \underset{˙}{+} Y \in U)) \to ⟨X, Y⟩ \in ⋃ (J \times_{t} J)$
17		eqid	$⊢ ⋃ (J \times_{t} J) = ⋃ (J \times_{t} J)$
18	17	cncnpi	$⊢ (+_{𝑓} (G) \in ((J \times_{t} J) Cn J) \land ⟨X, Y⟩ \in ⋃ (J \times_{t} J)) \to +_{𝑓} (G) \in ((J \times_{t} J) CnP J) (⟨X, Y⟩)$
19	8 16 18	syl2anc	$⊢ ((G \in TopMnd \land U \in J) \land (X \in B \land Y \in B \land X \underset{˙}{+} Y \in U)) \to +_{𝑓} (G) \in ((J \times_{t} J) CnP J) (⟨X, Y⟩)$
20		simplr	$⊢ ((G \in TopMnd \land U \in J) \land (X \in B \land Y \in B \land X \underset{˙}{+} Y \in U)) \to U \in J$
21	1 3 6	plusfval	$⊢ (X \in B \land Y \in B) \to X +_{𝑓} (G) Y = X \underset{˙}{+} Y$
22	9 10 21	syl2anc	$⊢ ((G \in TopMnd \land U \in J) \land (X \in B \land Y \in B \land X \underset{˙}{+} Y \in U)) \to X +_{𝑓} (G) Y = X \underset{˙}{+} Y$
23		simpr3	$⊢ ((G \in TopMnd \land U \in J) \land (X \in B \land Y \in B \land X \underset{˙}{+} Y \in U)) \to X \underset{˙}{+} Y \in U$
24	22 23	eqeltrd	$⊢ ((G \in TopMnd \land U \in J) \land (X \in B \land Y \in B \land X \underset{˙}{+} Y \in U)) \to X +_{𝑓} (G) Y \in U$
25	5 5 19 20 9 10 24	txcnpi	$⊢ ((G \in TopMnd \land U \in J) \land (X \in B \land Y \in B \land X \underset{˙}{+} Y \in U)) \to \exists u \in J \exists v \in J (X \in u \land Y \in v \land u \times v \subseteq {+_{𝑓} (G)}^{-1} [U])$
26		dfss3	$⊢ u \times v \subseteq {+_{𝑓} (G)}^{-1} [U] \leftrightarrow \forall z \in (u \times v) z \in {+_{𝑓} (G)}^{-1} [U]$
27		eleq1	$⊢ z = ⟨x, y⟩ \to (z \in {+_{𝑓} (G)}^{-1} [U] \leftrightarrow ⟨x, y⟩ \in {+_{𝑓} (G)}^{-1} [U])$
28	1 6	plusffn	$⊢ +_{𝑓} (G) Fn (B \times B)$
29		elpreima	$⊢ +_{𝑓} (G) Fn (B \times B) \to (⟨x, y⟩ \in {+_{𝑓} (G)}^{-1} [U] \leftrightarrow (⟨x, y⟩ \in (B \times B) \land +_{𝑓} (G) (⟨x, y⟩) \in U))$
30	28 29	ax-mp	$⊢ ⟨x, y⟩ \in {+_{𝑓} (G)}^{-1} [U] \leftrightarrow (⟨x, y⟩ \in (B \times B) \land +_{𝑓} (G) (⟨x, y⟩) \in U)$
31	27 30	bitrdi	$⊢ z = ⟨x, y⟩ \to (z \in {+_{𝑓} (G)}^{-1} [U] \leftrightarrow (⟨x, y⟩ \in (B \times B) \land +_{𝑓} (G) (⟨x, y⟩) \in U))$
32	31	ralxp	$⊢ \forall z \in (u \times v) z \in {+_{𝑓} (G)}^{-1} [U] \leftrightarrow \forall x \in u \forall y \in v (⟨x, y⟩ \in (B \times B) \land +_{𝑓} (G) (⟨x, y⟩) \in U)$
33	26 32	bitri	$⊢ u \times v \subseteq {+_{𝑓} (G)}^{-1} [U] \leftrightarrow \forall x \in u \forall y \in v (⟨x, y⟩ \in (B \times B) \land +_{𝑓} (G) (⟨x, y⟩) \in U)$
34		opelxp	$⊢ ⟨x, y⟩ \in (B \times B) \leftrightarrow (x \in B \land y \in B)$
35		df-ov	$⊢ x +_{𝑓} (G) y = +_{𝑓} (G) (⟨x, y⟩)$
36	1 3 6	plusfval	$⊢ (x \in B \land y \in B) \to x +_{𝑓} (G) y = x \underset{˙}{+} y$
37	35 36	syl5eqr	$⊢ (x \in B \land y \in B) \to +_{𝑓} (G) (⟨x, y⟩) = x \underset{˙}{+} y$
38	34 37	sylbi	$⊢ ⟨x, y⟩ \in (B \times B) \to +_{𝑓} (G) (⟨x, y⟩) = x \underset{˙}{+} y$
39	38	eleq1d	$⊢ ⟨x, y⟩ \in (B \times B) \to (+_{𝑓} (G) (⟨x, y⟩) \in U \leftrightarrow x \underset{˙}{+} y \in U)$
40	39	biimpa	$⊢ (⟨x, y⟩ \in (B \times B) \land +_{𝑓} (G) (⟨x, y⟩) \in U) \to x \underset{˙}{+} y \in U$
41	40	2ralimi	$⊢ \forall x \in u \forall y \in v (⟨x, y⟩ \in (B \times B) \land +_{𝑓} (G) (⟨x, y⟩) \in U) \to \forall x \in u \forall y \in v x \underset{˙}{+} y \in U$
42	33 41	sylbi	$⊢ u \times v \subseteq {+_{𝑓} (G)}^{-1} [U] \to \forall x \in u \forall y \in v x \underset{˙}{+} y \in U$
43	42	3anim3i	$⊢ (X \in u \land Y \in v \land u \times v \subseteq {+_{𝑓} (G)}^{-1} [U]) \to (X \in u \land Y \in v \land \forall x \in u \forall y \in v x \underset{˙}{+} y \in U)$
44	43	reximi	$⊢ \exists v \in J (X \in u \land Y \in v \land u \times v \subseteq {+_{𝑓} (G)}^{-1} [U]) \to \exists v \in J (X \in u \land Y \in v \land \forall x \in u \forall y \in v x \underset{˙}{+} y \in U)$
45	44	reximi	$⊢ \exists u \in J \exists v \in J (X \in u \land Y \in v \land u \times v \subseteq {+_{𝑓} (G)}^{-1} [U]) \to \exists u \in J \exists v \in J (X \in u \land Y \in v \land \forall x \in u \forall y \in v x \underset{˙}{+} y \in U)$
46	25 45	syl	$⊢ ((G \in TopMnd \land U \in J) \land (X \in B \land Y \in B \land X \underset{˙}{+} Y \in U)) \to \exists u \in J \exists v \in J (X \in u \land Y \in v \land \forall x \in u \forall y \in v x \underset{˙}{+} y \in U)$

Metamath Proof Explorer

Theorem tmdcn2

Proof