fgabs

Description: Absorption law for filter generation. (Contributed by Mario Carneiro, 15-Oct-2015)

		Ref	Expression
	Assertion	fgabs	$⊢ (F \in fBas (Y) \land Y \subseteq X) \to X filGen (Y filGen F) = X filGen F$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to F \in fBas (Y)$
2		fgcl	$⊢ F \in fBas (Y) \to Y filGen F \in Fil (Y)$
3		filfbas	$⊢ Y filGen F \in Fil (Y) \to Y filGen F \in fBas (Y)$
4	1 2 3	3syl	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to Y filGen F \in fBas (Y)$
5		fbsspw	$⊢ Y filGen F \in fBas (Y) \to Y filGen F \subseteq 𝒫 Y$
6	4 5	syl	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to Y filGen F \subseteq 𝒫 Y$
7		simplr	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to Y \subseteq X$
8	7	sspwd	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to 𝒫 Y \subseteq 𝒫 X$
9	6 8	sstrd	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to Y filGen F \subseteq 𝒫 X$
10		simpr	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to X \in V$
11		fbasweak	$⊢ (Y filGen F \in fBas (Y) \land Y filGen F \subseteq 𝒫 X \land X \in V) \to Y filGen F \in fBas (X)$
12	4 9 10 11	syl3anc	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to Y filGen F \in fBas (X)$
13		elfg	$⊢ Y filGen F \in fBas (X) \to (x \in (X filGen (Y filGen F)) \leftrightarrow (x \subseteq X \land \exists y \in (Y filGen F) y \subseteq x))$
14	12 13	syl	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to (x \in (X filGen (Y filGen F)) \leftrightarrow (x \subseteq X \land \exists y \in (Y filGen F) y \subseteq x))$
15	1	adantr	$⊢ (((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land x \subseteq X) \to F \in fBas (Y)$
16		elfg	$⊢ F \in fBas (Y) \to (y \in (Y filGen F) \leftrightarrow (y \subseteq Y \land \exists z \in F z \subseteq y))$
17	15 16	syl	$⊢ (((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land x \subseteq X) \to (y \in (Y filGen F) \leftrightarrow (y \subseteq Y \land \exists z \in F z \subseteq y))$
18		fbsspw	$⊢ F \in fBas (Y) \to F \subseteq 𝒫 Y$
19	1 18	syl	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to F \subseteq 𝒫 Y$
20	19 8	sstrd	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to F \subseteq 𝒫 X$
21		fbasweak	$⊢ (F \in fBas (Y) \land F \subseteq 𝒫 X \land X \in V) \to F \in fBas (X)$
22	1 20 10 21	syl3anc	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to F \in fBas (X)$
23		fgcl	$⊢ F \in fBas (X) \to X filGen F \in Fil (X)$
24	22 23	syl	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to X filGen F \in Fil (X)$
25	24	ad2antrr	$⊢ ((((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land (x \subseteq X \land y \subseteq Y)) \land ((z \in F \land z \subseteq y) \land y \subseteq x)) \to X filGen F \in Fil (X)$
26		ssfg	$⊢ F \in fBas (X) \to F \subseteq X filGen F$
27	22 26	syl	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to F \subseteq X filGen F$
28	27	adantr	$⊢ (((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land (x \subseteq X \land y \subseteq Y)) \to F \subseteq X filGen F$
29	28	sselda	$⊢ ((((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land (x \subseteq X \land y \subseteq Y)) \land z \in F) \to z \in (X filGen F)$
30	29	adantrr	$⊢ ((((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land (x \subseteq X \land y \subseteq Y)) \land (z \in F \land z \subseteq y)) \to z \in (X filGen F)$
31	30	adantrr	$⊢ ((((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land (x \subseteq X \land y \subseteq Y)) \land ((z \in F \land z \subseteq y) \land y \subseteq x)) \to z \in (X filGen F)$
32		simplrl	$⊢ ((((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land (x \subseteq X \land y \subseteq Y)) \land ((z \in F \land z \subseteq y) \land y \subseteq x)) \to x \subseteq X$
33		simprlr	$⊢ ((((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land (x \subseteq X \land y \subseteq Y)) \land ((z \in F \land z \subseteq y) \land y \subseteq x)) \to z \subseteq y$
34		simprr	$⊢ ((((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land (x \subseteq X \land y \subseteq Y)) \land ((z \in F \land z \subseteq y) \land y \subseteq x)) \to y \subseteq x$
35	33 34	sstrd	$⊢ ((((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land (x \subseteq X \land y \subseteq Y)) \land ((z \in F \land z \subseteq y) \land y \subseteq x)) \to z \subseteq x$
36		filss	$⊢ (X filGen F \in Fil (X) \land (z \in (X filGen F) \land x \subseteq X \land z \subseteq x)) \to x \in (X filGen F)$
37	25 31 32 35 36	syl13anc	$⊢ ((((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land (x \subseteq X \land y \subseteq Y)) \land ((z \in F \land z \subseteq y) \land y \subseteq x)) \to x \in (X filGen F)$
38	37	expr	$⊢ ((((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land (x \subseteq X \land y \subseteq Y)) \land (z \in F \land z \subseteq y)) \to (y \subseteq x \to x \in (X filGen F))$
39	38	rexlimdvaa	$⊢ (((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land (x \subseteq X \land y \subseteq Y)) \to (\exists z \in F z \subseteq y \to (y \subseteq x \to x \in (X filGen F)))$
40	39	anassrs	$⊢ ((((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land x \subseteq X) \land y \subseteq Y) \to (\exists z \in F z \subseteq y \to (y \subseteq x \to x \in (X filGen F)))$
41	40	expimpd	$⊢ (((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land x \subseteq X) \to ((y \subseteq Y \land \exists z \in F z \subseteq y) \to (y \subseteq x \to x \in (X filGen F)))$
42	17 41	sylbid	$⊢ (((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land x \subseteq X) \to (y \in (Y filGen F) \to (y \subseteq x \to x \in (X filGen F)))$
43	42	rexlimdv	$⊢ (((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \land x \subseteq X) \to (\exists y \in (Y filGen F) y \subseteq x \to x \in (X filGen F))$
44	43	expimpd	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to ((x \subseteq X \land \exists y \in (Y filGen F) y \subseteq x) \to x \in (X filGen F))$
45	14 44	sylbid	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to (x \in (X filGen (Y filGen F)) \to x \in (X filGen F))$
46	45	ssrdv	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to X filGen (Y filGen F) \subseteq X filGen F$
47		ssfg	$⊢ F \in fBas (Y) \to F \subseteq Y filGen F$
48	47	ad2antrr	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to F \subseteq Y filGen F$
49		fgss	$⊢ (F \in fBas (X) \land Y filGen F \in fBas (X) \land F \subseteq Y filGen F) \to X filGen F \subseteq X filGen (Y filGen F)$
50	22 12 48 49	syl3anc	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to X filGen F \subseteq X filGen (Y filGen F)$
51	46 50	eqssd	$⊢ ((F \in fBas (Y) \land Y \subseteq X) \land X \in V) \to X filGen (Y filGen F) = X filGen F$
52	51	ex	$⊢ (F \in fBas (Y) \land Y \subseteq X) \to (X \in V \to X filGen (Y filGen F) = X filGen F)$
53		df-fg	$⊢ filGen = (w \in V, x \in fBas (w) ⟼ \{y \in 𝒫 w \| x \cap 𝒫 y \neq \emptyset\})$
54	53	reldmmpo	$⊢ Rel dom filGen$
55	54	ovprc1	$⊢ \neg X \in V \to X filGen (Y filGen F) = \emptyset$
56	54	ovprc1	$⊢ \neg X \in V \to X filGen F = \emptyset$
57	55 56	eqtr4d	$⊢ \neg X \in V \to X filGen (Y filGen F) = X filGen F$
58	52 57	pm2.61d1	$⊢ (F \in fBas (Y) \land Y \subseteq X) \to X filGen (Y filGen F) = X filGen F$

Metamath Proof Explorer

Theorem fgabs

Proof