fgtr

Description: If A is a member of the filter, then truncating F to A and regenerating the behavior outside A using filGen recovers the original filter. (Contributed by Mario Carneiro, 15-Oct-2015)

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

Proof

Step	Hyp	Ref	Expression
1		filfbas	$⊢ F \in Fil (X) \to F \in fBas (X)$
2		fbncp	$⊢ (F \in fBas (X) \land A \in F) \to \neg X ∖ A \in F$
3	1 2	sylan	$⊢ (F \in Fil (X) \land A \in F) \to \neg X ∖ A \in F$
4		filelss	$⊢ (F \in Fil (X) \land A \in F) \to A \subseteq X$
5		trfil3	$⊢ (F \in Fil (X) \land A \subseteq X) \to (F ↾_{𝑡} A \in Fil (A) \leftrightarrow \neg X ∖ A \in F)$
6	4 5	syldan	$⊢ (F \in Fil (X) \land A \in F) \to (F ↾_{𝑡} A \in Fil (A) \leftrightarrow \neg X ∖ A \in F)$
7	3 6	mpbird	$⊢ (F \in Fil (X) \land A \in F) \to F ↾_{𝑡} A \in Fil (A)$
8		filfbas	$⊢ F ↾_{𝑡} A \in Fil (A) \to F ↾_{𝑡} A \in fBas (A)$
9	7 8	syl	$⊢ (F \in Fil (X) \land A \in F) \to F ↾_{𝑡} A \in fBas (A)$
10		restsspw	$⊢ F ↾_{𝑡} A \subseteq 𝒫 A$
11	4	sspwd	$⊢ (F \in Fil (X) \land A \in F) \to 𝒫 A \subseteq 𝒫 X$
12	10 11	sstrid	$⊢ (F \in Fil (X) \land A \in F) \to F ↾_{𝑡} A \subseteq 𝒫 X$
13		filtop	$⊢ F \in Fil (X) \to X \in F$
14	13	adantr	$⊢ (F \in Fil (X) \land A \in F) \to X \in F$
15		fbasweak	$⊢ (F ↾_{𝑡} A \in fBas (A) \land F ↾_{𝑡} A \subseteq 𝒫 X \land X \in F) \to F ↾_{𝑡} A \in fBas (X)$
16	9 12 14 15	syl3anc	$⊢ (F \in Fil (X) \land A \in F) \to F ↾_{𝑡} A \in fBas (X)$
17	1	adantr	$⊢ (F \in Fil (X) \land A \in F) \to F \in fBas (X)$
18		trfilss	$⊢ (F \in Fil (X) \land A \in F) \to F ↾_{𝑡} A \subseteq F$
19		fgss	$⊢ (F ↾_{𝑡} A \in fBas (X) \land F \in fBas (X) \land F ↾_{𝑡} A \subseteq F) \to X filGen (F ↾_{𝑡} A) \subseteq X filGen F$
20	16 17 18 19	syl3anc	$⊢ (F \in Fil (X) \land A \in F) \to X filGen (F ↾_{𝑡} A) \subseteq X filGen F$
21		fgfil	$⊢ F \in Fil (X) \to X filGen F = F$
22	21	adantr	$⊢ (F \in Fil (X) \land A \in F) \to X filGen F = F$
23	20 22	sseqtrd	$⊢ (F \in Fil (X) \land A \in F) \to X filGen (F ↾_{𝑡} A) \subseteq F$
24		filelss	$⊢ (F \in Fil (X) \land x \in F) \to x \subseteq X$
25	24	ex	$⊢ F \in Fil (X) \to (x \in F \to x \subseteq X)$
26	25	adantr	$⊢ (F \in Fil (X) \land A \in F) \to (x \in F \to x \subseteq X)$
27		elrestr	$⊢ (F \in Fil (X) \land A \in F \land x \in F) \to x \cap A \in (F ↾_{𝑡} A)$
28	27	3expa	$⊢ ((F \in Fil (X) \land A \in F) \land x \in F) \to x \cap A \in (F ↾_{𝑡} A)$
29		inss1	$⊢ x \cap A \subseteq x$
30		sseq1	$⊢ y = x \cap A \to (y \subseteq x \leftrightarrow x \cap A \subseteq x)$
31	30	rspcev	$⊢ (x \cap A \in (F ↾_{𝑡} A) \land x \cap A \subseteq x) \to \exists y \in (F ↾_{𝑡} A) y \subseteq x$
32	28 29 31	sylancl	$⊢ ((F \in Fil (X) \land A \in F) \land x \in F) \to \exists y \in (F ↾_{𝑡} A) y \subseteq x$
33	32	ex	$⊢ (F \in Fil (X) \land A \in F) \to (x \in F \to \exists y \in (F ↾_{𝑡} A) y \subseteq x)$
34	26 33	jcad	$⊢ (F \in Fil (X) \land A \in F) \to (x \in F \to (x \subseteq X \land \exists y \in (F ↾_{𝑡} A) y \subseteq x))$
35		elfg	$⊢ F ↾_{𝑡} A \in fBas (X) \to (x \in (X filGen (F ↾_{𝑡} A)) \leftrightarrow (x \subseteq X \land \exists y \in (F ↾_{𝑡} A) y \subseteq x))$
36	16 35	syl	$⊢ (F \in Fil (X) \land A \in F) \to (x \in (X filGen (F ↾_{𝑡} A)) \leftrightarrow (x \subseteq X \land \exists y \in (F ↾_{𝑡} A) y \subseteq x))$
37	34 36	sylibrd	$⊢ (F \in Fil (X) \land A \in F) \to (x \in F \to x \in (X filGen (F ↾_{𝑡} A)))$
38	37	ssrdv	$⊢ (F \in Fil (X) \land A \in F) \to F \subseteq X filGen (F ↾_{𝑡} A)$
39	23 38	eqssd	$⊢ (F \in Fil (X) \land A \in F) \to X filGen (F ↾_{𝑡} A) = F$

Metamath Proof Explorer

Theorem fgtr

Proof