istmd

Description: The predicate "is a topological monoid". (Contributed by Mario Carneiro, 19-Sep-2015)

	Ref	Expression
Hypotheses	istmd.1	$⊢ F = +_{𝑓} (G)$
	istmd.2	$⊢ J = TopOpen (G)$
Assertion	istmd	$⊢ G \in TopMnd \leftrightarrow (G \in Mnd \land G \in TopSp \land F \in ((J \times_{t} J) Cn J))$

Proof

Step	Hyp	Ref	Expression
1		istmd.1	$⊢ F = +_{𝑓} (G)$
2		istmd.2	$⊢ J = TopOpen (G)$
3		elin	$⊢ G \in (Mnd \cap TopSp) \leftrightarrow (G \in Mnd \land G \in TopSp)$
4	3	anbi1i	$⊢ (G \in (Mnd \cap TopSp) \land F \in ((J \times_{t} J) Cn J)) \leftrightarrow ((G \in Mnd \land G \in TopSp) \land F \in ((J \times_{t} J) Cn J))$
5		fvexd	$⊢ f = G \to TopOpen (f) \in V$
6		simpl	$⊢ (f = G \land j = TopOpen (f)) \to f = G$
7	6	fveq2d	$⊢ (f = G \land j = TopOpen (f)) \to +_{𝑓} (f) = +_{𝑓} (G)$
8	7 1	eqtr4di	$⊢ (f = G \land j = TopOpen (f)) \to +_{𝑓} (f) = F$
9		id	$⊢ j = TopOpen (f) \to j = TopOpen (f)$
10		fveq2	$⊢ f = G \to TopOpen (f) = TopOpen (G)$
11	10 2	eqtr4di	$⊢ f = G \to TopOpen (f) = J$
12	9 11	sylan9eqr	$⊢ (f = G \land j = TopOpen (f)) \to j = J$
13	12 12	oveq12d	$⊢ (f = G \land j = TopOpen (f)) \to j \times_{t} j = J \times_{t} J$
14	13 12	oveq12d	$⊢ (f = G \land j = TopOpen (f)) \to (j \times_{t} j) Cn j = (J \times_{t} J) Cn J$
15	8 14	eleq12d	$⊢ (f = G \land j = TopOpen (f)) \to (+_{𝑓} (f) \in ((j \times_{t} j) Cn j) \leftrightarrow F \in ((J \times_{t} J) Cn J))$
16	5 15	sbcied	$⊢ f = G \to (\underset{˙}{[} TopOpen (f) / j \underset{˙}{]} +_{𝑓} (f) \in ((j \times_{t} j) Cn j) \leftrightarrow F \in ((J \times_{t} J) Cn J))$
17		df-tmd	$⊢ TopMnd = \{f \in (Mnd \cap TopSp) \| \underset{˙}{[} TopOpen (f) / j \underset{˙}{]} +_{𝑓} (f) \in ((j \times_{t} j) Cn j)\}$
18	16 17	elrab2	$⊢ G \in TopMnd \leftrightarrow (G \in (Mnd \cap TopSp) \land F \in ((J \times_{t} J) Cn J))$
19		df-3an	$⊢ (G \in Mnd \land G \in TopSp \land F \in ((J \times_{t} J) Cn J)) \leftrightarrow ((G \in Mnd \land G \in TopSp) \land F \in ((J \times_{t} J) Cn J))$
20	4 18 19	3bitr4i	$⊢ G \in TopMnd \leftrightarrow (G \in Mnd \land G \in TopSp \land F \in ((J \times_{t} J) Cn J))$

Metamath Proof Explorer

Theorem istmd

Proof