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

Metamath Proof Explorer

Theorem tgfiss

Description: If a subbase is included into a topology, so is the generated topology. (Contributed by FL, 20-Apr-2012) (Proof shortened by Mario Carneiro, 10-Jan-2015)

		Ref	Expression
	Assertion	tgfiss	$⊢ (J \in Top \land A \subseteq J) \to topGen (fi (A)) \subseteq J$

Proof

Step	Hyp	Ref	Expression
1		fiss	$⊢ (J \in Top \land A \subseteq J) \to fi (A) \subseteq fi (J)$
2		fitop	$⊢ J \in Top \to fi (J) = J$
3	2	adantr	$⊢ (J \in Top \land A \subseteq J) \to fi (J) = J$
4	1 3	sseqtrd	$⊢ (J \in Top \land A \subseteq J) \to fi (A) \subseteq J$
5		tgss	$⊢ (J \in Top \land fi (A) \subseteq J) \to topGen (fi (A)) \subseteq topGen (J)$
6	4 5	syldan	$⊢ (J \in Top \land A \subseteq J) \to topGen (fi (A)) \subseteq topGen (J)$
7		tgtop	$⊢ J \in Top \to topGen (J) = J$
8	7	adantr	$⊢ (J \in Top \land A \subseteq J) \to topGen (J) = J$
9	6 8	sseqtrd	$⊢ (J \in Top \land A \subseteq J) \to topGen (fi (A)) \subseteq J$