fgss2

Description: A condition for a filter to be finer than another involving their filter bases. (Contributed by Jeff Hankins, 3-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	fgss2	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (X filGen F \subseteq X filGen G \leftrightarrow \forall x \in F \exists y \in G y \subseteq x)$

Proof

Step	Hyp	Ref	Expression
1		ssfg	$⊢ F \in fBas (X) \to F \subseteq X filGen F$
2	1	adantr	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to F \subseteq X filGen F$
3	2	sseld	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (x \in F \to x \in (X filGen F))$
4		ssel2	$⊢ (X filGen F \subseteq X filGen G \land x \in (X filGen F)) \to x \in (X filGen G)$
5		elfg	$⊢ G \in fBas (X) \to (x \in (X filGen G) \leftrightarrow (x \subseteq X \land \exists y \in G y \subseteq x))$
6		simpr	$⊢ (x \subseteq X \land \exists y \in G y \subseteq x) \to \exists y \in G y \subseteq x$
7	5 6	biimtrdi	$⊢ G \in fBas (X) \to (x \in (X filGen G) \to \exists y \in G y \subseteq x)$
8	7	adantl	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (x \in (X filGen G) \to \exists y \in G y \subseteq x)$
9	4 8	syl5	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to ((X filGen F \subseteq X filGen G \land x \in (X filGen F)) \to \exists y \in G y \subseteq x)$
10	9	expd	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (X filGen F \subseteq X filGen G \to (x \in (X filGen F) \to \exists y \in G y \subseteq x))$
11	3 10	syl5d	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (X filGen F \subseteq X filGen G \to (x \in F \to \exists y \in G y \subseteq x))$
12	11	ralrimdv	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (X filGen F \subseteq X filGen G \to \forall x \in F \exists y \in G y \subseteq x)$
13		sseq2	$⊢ x = u \to (y \subseteq x \leftrightarrow y \subseteq u)$
14	13	rexbidv	$⊢ x = u \to (\exists y \in G y \subseteq x \leftrightarrow \exists y \in G y \subseteq u)$
15	14	rspcv	$⊢ u \in F \to (\forall x \in F \exists y \in G y \subseteq x \to \exists y \in G y \subseteq u)$
16	15	adantl	$⊢ ((F \in fBas (X) \land G \in fBas (X)) \land u \in F) \to (\forall x \in F \exists y \in G y \subseteq x \to \exists y \in G y \subseteq u)$
17		sstr	$⊢ (y \subseteq u \land u \subseteq t) \to y \subseteq t$
18		sseq1	$⊢ v = y \to (v \subseteq t \leftrightarrow y \subseteq t)$
19	18	rspcev	$⊢ (y \in G \land y \subseteq t) \to \exists v \in G v \subseteq t$
20	19	adantl	$⊢ (((F \in fBas (X) \land G \in fBas (X)) \land u \in F) \land (y \in G \land y \subseteq t)) \to \exists v \in G v \subseteq t$
21	20	a1d	$⊢ (((F \in fBas (X) \land G \in fBas (X)) \land u \in F) \land (y \in G \land y \subseteq t)) \to (t \subseteq X \to \exists v \in G v \subseteq t)$
22	17 21	sylanr2	$⊢ (((F \in fBas (X) \land G \in fBas (X)) \land u \in F) \land (y \in G \land (y \subseteq u \land u \subseteq t))) \to (t \subseteq X \to \exists v \in G v \subseteq t)$
23	22	ancld	$⊢ (((F \in fBas (X) \land G \in fBas (X)) \land u \in F) \land (y \in G \land (y \subseteq u \land u \subseteq t))) \to (t \subseteq X \to (t \subseteq X \land \exists v \in G v \subseteq t))$
24	23	exp45	$⊢ ((F \in fBas (X) \land G \in fBas (X)) \land u \in F) \to (y \in G \to (y \subseteq u \to (u \subseteq t \to (t \subseteq X \to (t \subseteq X \land \exists v \in G v \subseteq t)))))$
25	24	rexlimdv	$⊢ ((F \in fBas (X) \land G \in fBas (X)) \land u \in F) \to (\exists y \in G y \subseteq u \to (u \subseteq t \to (t \subseteq X \to (t \subseteq X \land \exists v \in G v \subseteq t))))$
26	16 25	syld	$⊢ ((F \in fBas (X) \land G \in fBas (X)) \land u \in F) \to (\forall x \in F \exists y \in G y \subseteq x \to (u \subseteq t \to (t \subseteq X \to (t \subseteq X \land \exists v \in G v \subseteq t))))$
27	26	impancom	$⊢ ((F \in fBas (X) \land G \in fBas (X)) \land \forall x \in F \exists y \in G y \subseteq x) \to (u \in F \to (u \subseteq t \to (t \subseteq X \to (t \subseteq X \land \exists v \in G v \subseteq t))))$
28	27	rexlimdv	$⊢ ((F \in fBas (X) \land G \in fBas (X)) \land \forall x \in F \exists y \in G y \subseteq x) \to (\exists u \in F u \subseteq t \to (t \subseteq X \to (t \subseteq X \land \exists v \in G v \subseteq t)))$
29	28	impcomd	$⊢ ((F \in fBas (X) \land G \in fBas (X)) \land \forall x \in F \exists y \in G y \subseteq x) \to ((t \subseteq X \land \exists u \in F u \subseteq t) \to (t \subseteq X \land \exists v \in G v \subseteq t))$
30		elfg	$⊢ F \in fBas (X) \to (t \in (X filGen F) \leftrightarrow (t \subseteq X \land \exists u \in F u \subseteq t))$
31	30	adantr	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (t \in (X filGen F) \leftrightarrow (t \subseteq X \land \exists u \in F u \subseteq t))$
32	31	adantr	$⊢ ((F \in fBas (X) \land G \in fBas (X)) \land \forall x \in F \exists y \in G y \subseteq x) \to (t \in (X filGen F) \leftrightarrow (t \subseteq X \land \exists u \in F u \subseteq t))$
33		elfg	$⊢ G \in fBas (X) \to (t \in (X filGen G) \leftrightarrow (t \subseteq X \land \exists v \in G v \subseteq t))$
34	33	adantl	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (t \in (X filGen G) \leftrightarrow (t \subseteq X \land \exists v \in G v \subseteq t))$
35	34	adantr	$⊢ ((F \in fBas (X) \land G \in fBas (X)) \land \forall x \in F \exists y \in G y \subseteq x) \to (t \in (X filGen G) \leftrightarrow (t \subseteq X \land \exists v \in G v \subseteq t))$
36	29 32 35	3imtr4d	$⊢ ((F \in fBas (X) \land G \in fBas (X)) \land \forall x \in F \exists y \in G y \subseteq x) \to (t \in (X filGen F) \to t \in (X filGen G))$
37	36	ssrdv	$⊢ ((F \in fBas (X) \land G \in fBas (X)) \land \forall x \in F \exists y \in G y \subseteq x) \to X filGen F \subseteq X filGen G$
38	37	ex	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (\forall x \in F \exists y \in G y \subseteq x \to X filGen F \subseteq X filGen G)$
39	12 38	impbid	$⊢ (F \in fBas (X) \land G \in fBas (X)) \to (X filGen F \subseteq X filGen G \leftrightarrow \forall x \in F \exists y \in G y \subseteq x)$

Metamath Proof Explorer

Theorem fgss2

Proof