trfg

Description: The trace operation and the filGen operation are inverses to one another in some sense, with filGen growing the base set and ` |``t ` shrinking it. See fgtr for the converse cancellation law. (Contributed by Mario Carneiro, 15-Oct-2015)

		Ref	Expression
	Assertion	trfg	$⊢ (F \in Fil (A) \land A \subseteq X \land X \in V) \to (X filGen F) ↾_{𝑡} A = F$

Proof

Step	Hyp	Ref	Expression
1		filfbas	$⊢ F \in Fil (A) \to F \in fBas (A)$
2	1	3ad2ant1	$⊢ (F \in Fil (A) \land A \subseteq X \land X \in V) \to F \in fBas (A)$
3		filsspw	$⊢ F \in Fil (A) \to F \subseteq 𝒫 A$
4	3	3ad2ant1	$⊢ (F \in Fil (A) \land A \subseteq X \land X \in V) \to F \subseteq 𝒫 A$
5		simp2	$⊢ (F \in Fil (A) \land A \subseteq X \land X \in V) \to A \subseteq X$
6	5	sspwd	$⊢ (F \in Fil (A) \land A \subseteq X \land X \in V) \to 𝒫 A \subseteq 𝒫 X$
7	4 6	sstrd	$⊢ (F \in Fil (A) \land A \subseteq X \land X \in V) \to F \subseteq 𝒫 X$
8		simp3	$⊢ (F \in Fil (A) \land A \subseteq X \land X \in V) \to X \in V$
9		fbasweak	$⊢ (F \in fBas (A) \land F \subseteq 𝒫 X \land X \in V) \to F \in fBas (X)$
10	2 7 8 9	syl3anc	$⊢ (F \in Fil (A) \land A \subseteq X \land X \in V) \to F \in fBas (X)$
11		fgcl	$⊢ F \in fBas (X) \to X filGen F \in Fil (X)$
12	10 11	syl	$⊢ (F \in Fil (A) \land A \subseteq X \land X \in V) \to X filGen F \in Fil (X)$
13		filtop	$⊢ F \in Fil (A) \to A \in F$
14	13	3ad2ant1	$⊢ (F \in Fil (A) \land A \subseteq X \land X \in V) \to A \in F$
15		restval	$⊢ (X filGen F \in Fil (X) \land A \in F) \to (X filGen F) ↾_{𝑡} A = ran (x \in (X filGen F) ⟼ x \cap A)$
16	12 14 15	syl2anc	$⊢ (F \in Fil (A) \land A \subseteq X \land X \in V) \to (X filGen F) ↾_{𝑡} A = ran (x \in (X filGen F) ⟼ x \cap A)$
17		elfg	$⊢ F \in fBas (X) \to (x \in (X filGen F) \leftrightarrow (x \subseteq X \land \exists y \in F y \subseteq x))$
18	10 17	syl	$⊢ (F \in Fil (A) \land A \subseteq X \land X \in V) \to (x \in (X filGen F) \leftrightarrow (x \subseteq X \land \exists y \in F y \subseteq x))$
19	18	simplbda	$⊢ ((F \in Fil (A) \land A \subseteq X \land X \in V) \land x \in (X filGen F)) \to \exists y \in F y \subseteq x$
20		simpll1	$⊢ (((F \in Fil (A) \land A \subseteq X \land X \in V) \land x \in (X filGen F)) \land (y \in F \land y \subseteq x)) \to F \in Fil (A)$
21		simprl	$⊢ (((F \in Fil (A) \land A \subseteq X \land X \in V) \land x \in (X filGen F)) \land (y \in F \land y \subseteq x)) \to y \in F$
22		inss2	$⊢ x \cap A \subseteq A$
23	22	a1i	$⊢ (((F \in Fil (A) \land A \subseteq X \land X \in V) \land x \in (X filGen F)) \land (y \in F \land y \subseteq x)) \to x \cap A \subseteq A$
24		simprr	$⊢ (((F \in Fil (A) \land A \subseteq X \land X \in V) \land x \in (X filGen F)) \land (y \in F \land y \subseteq x)) \to y \subseteq x$
25		filelss	$⊢ (F \in Fil (A) \land y \in F) \to y \subseteq A$
26	25	3ad2antl1	$⊢ ((F \in Fil (A) \land A \subseteq X \land X \in V) \land y \in F) \to y \subseteq A$
27	26	ad2ant2r	$⊢ (((F \in Fil (A) \land A \subseteq X \land X \in V) \land x \in (X filGen F)) \land (y \in F \land y \subseteq x)) \to y \subseteq A$
28	24 27	ssind	$⊢ (((F \in Fil (A) \land A \subseteq X \land X \in V) \land x \in (X filGen F)) \land (y \in F \land y \subseteq x)) \to y \subseteq x \cap A$
29		filss	$⊢ (F \in Fil (A) \land (y \in F \land x \cap A \subseteq A \land y \subseteq x \cap A)) \to x \cap A \in F$
30	20 21 23 28 29	syl13anc	$⊢ (((F \in Fil (A) \land A \subseteq X \land X \in V) \land x \in (X filGen F)) \land (y \in F \land y \subseteq x)) \to x \cap A \in F$
31	19 30	rexlimddv	$⊢ ((F \in Fil (A) \land A \subseteq X \land X \in V) \land x \in (X filGen F)) \to x \cap A \in F$
32	31	fmpttd	$⊢ (F \in Fil (A) \land A \subseteq X \land X \in V) \to (x \in (X filGen F) ⟼ x \cap A) : X filGen F ⟶ F$
33	32	frnd	$⊢ (F \in Fil (A) \land A \subseteq X \land X \in V) \to ran (x \in (X filGen F) ⟼ x \cap A) \subseteq F$
34	16 33	eqsstrd	$⊢ (F \in Fil (A) \land A \subseteq X \land X \in V) \to (X filGen F) ↾_{𝑡} A \subseteq F$
35		filelss	$⊢ (F \in Fil (A) \land x \in F) \to x \subseteq A$
36	35	3ad2antl1	$⊢ ((F \in Fil (A) \land A \subseteq X \land X \in V) \land x \in F) \to x \subseteq A$
37		dfss2	$⊢ x \subseteq A \leftrightarrow x \cap A = x$
38	36 37	sylib	$⊢ ((F \in Fil (A) \land A \subseteq X \land X \in V) \land x \in F) \to x \cap A = x$
39	12	adantr	$⊢ ((F \in Fil (A) \land A \subseteq X \land X \in V) \land x \in F) \to X filGen F \in Fil (X)$
40	14	adantr	$⊢ ((F \in Fil (A) \land A \subseteq X \land X \in V) \land x \in F) \to A \in F$
41		ssfg	$⊢ F \in fBas (X) \to F \subseteq X filGen F$
42	10 41	syl	$⊢ (F \in Fil (A) \land A \subseteq X \land X \in V) \to F \subseteq X filGen F$
43	42	sselda	$⊢ ((F \in Fil (A) \land A \subseteq X \land X \in V) \land x \in F) \to x \in (X filGen F)$
44		elrestr	$⊢ (X filGen F \in Fil (X) \land A \in F \land x \in (X filGen F)) \to x \cap A \in ((X filGen F) ↾_{𝑡} A)$
45	39 40 43 44	syl3anc	$⊢ ((F \in Fil (A) \land A \subseteq X \land X \in V) \land x \in F) \to x \cap A \in ((X filGen F) ↾_{𝑡} A)$
46	38 45	eqeltrrd	$⊢ ((F \in Fil (A) \land A \subseteq X \land X \in V) \land x \in F) \to x \in ((X filGen F) ↾_{𝑡} A)$
47	34 46	eqelssd	$⊢ (F \in Fil (A) \land A \subseteq X \land X \in V) \to (X filGen F) ↾_{𝑡} A = F$

Metamath Proof Explorer

Theorem trfg

Proof