tgss2

Description: A criterion for determining whether one topology is finer than another, based on a comparison of their bases. Lemma 2.2 of Munkres p. 80. (Contributed by NM, 20-Jul-2006) (Proof shortened by Mario Carneiro, 2-Sep-2015)

		Ref	Expression
	Assertion	tgss2	$⊢ (B \in V \land ⋃ B = ⋃ C) \to (topGen (B) \subseteq topGen (C) \leftrightarrow \forall x \in ⋃ B \forall y \in B (x \in y \to \exists z \in C (x \in z \land z \subseteq y)))$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (B \in V \land ⋃ B = ⋃ C) \to ⋃ B = ⋃ C$
2		uniexg	$⊢ B \in V \to ⋃ B \in V$
3	2	adantr	$⊢ (B \in V \land ⋃ B = ⋃ C) \to ⋃ B \in V$
4	1 3	eqeltrrd	$⊢ (B \in V \land ⋃ B = ⋃ C) \to ⋃ C \in V$
5		uniexb	$⊢ C \in V \leftrightarrow ⋃ C \in V$
6	4 5	sylibr	$⊢ (B \in V \land ⋃ B = ⋃ C) \to C \in V$
7		tgss3	$⊢ (B \in V \land C \in V) \to (topGen (B) \subseteq topGen (C) \leftrightarrow B \subseteq topGen (C))$
8	6 7	syldan	$⊢ (B \in V \land ⋃ B = ⋃ C) \to (topGen (B) \subseteq topGen (C) \leftrightarrow B \subseteq topGen (C))$
9		eltg2b	$⊢ C \in V \to (y \in topGen (C) \leftrightarrow \forall x \in y \exists z \in C (x \in z \land z \subseteq y))$
10	6 9	syl	$⊢ (B \in V \land ⋃ B = ⋃ C) \to (y \in topGen (C) \leftrightarrow \forall x \in y \exists z \in C (x \in z \land z \subseteq y))$
11		elunii	$⊢ (x \in y \land y \in B) \to x \in ⋃ B$
12	11	ancoms	$⊢ (y \in B \land x \in y) \to x \in ⋃ B$
13		biimt	$⊢ x \in ⋃ B \to (\exists z \in C (x \in z \land z \subseteq y) \leftrightarrow (x \in ⋃ B \to \exists z \in C (x \in z \land z \subseteq y)))$
14	12 13	syl	$⊢ (y \in B \land x \in y) \to (\exists z \in C (x \in z \land z \subseteq y) \leftrightarrow (x \in ⋃ B \to \exists z \in C (x \in z \land z \subseteq y)))$
15	14	ralbidva	$⊢ y \in B \to (\forall x \in y \exists z \in C (x \in z \land z \subseteq y) \leftrightarrow \forall x \in y (x \in ⋃ B \to \exists z \in C (x \in z \land z \subseteq y)))$
16	10 15	sylan9bb	$⊢ ((B \in V \land ⋃ B = ⋃ C) \land y \in B) \to (y \in topGen (C) \leftrightarrow \forall x \in y (x \in ⋃ B \to \exists z \in C (x \in z \land z \subseteq y)))$
17		ralcom3	$⊢ \forall x \in y (x \in ⋃ B \to \exists z \in C (x \in z \land z \subseteq y)) \leftrightarrow \forall x \in ⋃ B (x \in y \to \exists z \in C (x \in z \land z \subseteq y))$
18	16 17	bitrdi	$⊢ ((B \in V \land ⋃ B = ⋃ C) \land y \in B) \to (y \in topGen (C) \leftrightarrow \forall x \in ⋃ B (x \in y \to \exists z \in C (x \in z \land z \subseteq y)))$
19	18	ralbidva	$⊢ (B \in V \land ⋃ B = ⋃ C) \to (\forall y \in B y \in topGen (C) \leftrightarrow \forall y \in B \forall x \in ⋃ B (x \in y \to \exists z \in C (x \in z \land z \subseteq y)))$
20		dfss3	$⊢ B \subseteq topGen (C) \leftrightarrow \forall y \in B y \in topGen (C)$
21		ralcom	$⊢ \forall x \in ⋃ B \forall y \in B (x \in y \to \exists z \in C (x \in z \land z \subseteq y)) \leftrightarrow \forall y \in B \forall x \in ⋃ B (x \in y \to \exists z \in C (x \in z \land z \subseteq y))$
22	19 20 21	3bitr4g	$⊢ (B \in V \land ⋃ B = ⋃ C) \to (B \subseteq topGen (C) \leftrightarrow \forall x \in ⋃ B \forall y \in B (x \in y \to \exists z \in C (x \in z \land z \subseteq y)))$
23	8 22	bitrd	$⊢ (B \in V \land ⋃ B = ⋃ C) \to (topGen (B) \subseteq topGen (C) \leftrightarrow \forall x \in ⋃ B \forall y \in B (x \in y \to \exists z \in C (x \in z \land z \subseteq y)))$

Metamath Proof Explorer

Theorem tgss2

Proof