trfil2

Description: Conditions for the trace of a filter L to be a filter. (Contributed by FL, 2-Sep-2013) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	trfil2	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to (L ↾_{𝑡} A \in Fil (A) \leftrightarrow \forall v \in L v \cap A \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to A \subseteq Y$
2		sseqin2	$⊢ A \subseteq Y \leftrightarrow Y \cap A = A$
3	1 2	sylib	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to Y \cap A = A$
4		simpl	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to L \in Fil (Y)$
5		id	$⊢ A \subseteq Y \to A \subseteq Y$
6		filtop	$⊢ L \in Fil (Y) \to Y \in L$
7		ssexg	$⊢ (A \subseteq Y \land Y \in L) \to A \in V$
8	5 6 7	syl2anr	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to A \in V$
9	6	adantr	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to Y \in L$
10		elrestr	$⊢ (L \in Fil (Y) \land A \in V \land Y \in L) \to Y \cap A \in (L ↾_{𝑡} A)$
11	4 8 9 10	syl3anc	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to Y \cap A \in (L ↾_{𝑡} A)$
12	3 11	eqeltrrd	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to A \in (L ↾_{𝑡} A)$
13		elpwi	$⊢ x \in 𝒫 A \to x \subseteq A$
14		vex	$⊢ u \in V$
15	14	inex1	$⊢ u \cap A \in V$
16	15	a1i	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land u \in L) \to u \cap A \in V$
17		elrest	$⊢ (L \in Fil (Y) \land A \in V) \to (y \in (L ↾_{𝑡} A) \leftrightarrow \exists u \in L y = u \cap A)$
18	8 17	syldan	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to (y \in (L ↾_{𝑡} A) \leftrightarrow \exists u \in L y = u \cap A)$
19	18	adantr	$⊢ ((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \to (y \in (L ↾_{𝑡} A) \leftrightarrow \exists u \in L y = u \cap A)$
20		simpr	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land y = u \cap A) \to y = u \cap A$
21	20	sseq1d	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land y = u \cap A) \to (y \subseteq x \leftrightarrow u \cap A \subseteq x)$
22	16 19 21	rexxfr2d	$⊢ ((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \to (\exists y \in (L ↾_{𝑡} A) y \subseteq x \leftrightarrow \exists u \in L u \cap A \subseteq x)$
23		indir	$⊢ (u \cup x) \cap A = (u \cap A) \cup (x \cap A)$
24		simplr	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to x \subseteq A$
25		dfss2	$⊢ x \subseteq A \leftrightarrow x \cap A = x$
26	24 25	sylib	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to x \cap A = x$
27	26	uneq2d	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to (u \cap A) \cup (x \cap A) = (u \cap A) \cup x$
28		simprr	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to u \cap A \subseteq x$
29		ssequn1	$⊢ u \cap A \subseteq x \leftrightarrow (u \cap A) \cup x = x$
30	28 29	sylib	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to (u \cap A) \cup x = x$
31	27 30	eqtrd	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to (u \cap A) \cup (x \cap A) = x$
32	23 31	eqtrid	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to (u \cup x) \cap A = x$
33		simplll	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to L \in Fil (Y)$
34		simpllr	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to A \subseteq Y$
35	33 34 8	syl2anc	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to A \in V$
36		simprl	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to u \in L$
37		filelss	$⊢ (L \in Fil (Y) \land u \in L) \to u \subseteq Y$
38	33 36 37	syl2anc	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to u \subseteq Y$
39	24 34	sstrd	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to x \subseteq Y$
40	38 39	unssd	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to u \cup x \subseteq Y$
41		ssun1	$⊢ u \subseteq u \cup x$
42	41	a1i	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to u \subseteq u \cup x$
43		filss	$⊢ (L \in Fil (Y) \land (u \in L \land u \cup x \subseteq Y \land u \subseteq u \cup x)) \to u \cup x \in L$
44	33 36 40 42 43	syl13anc	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to u \cup x \in L$
45		elrestr	$⊢ (L \in Fil (Y) \land A \in V \land u \cup x \in L) \to (u \cup x) \cap A \in (L ↾_{𝑡} A)$
46	33 35 44 45	syl3anc	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to (u \cup x) \cap A \in (L ↾_{𝑡} A)$
47	32 46	eqeltrrd	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \land (u \in L \land u \cap A \subseteq x)) \to x \in (L ↾_{𝑡} A)$
48	47	rexlimdvaa	$⊢ ((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \to (\exists u \in L u \cap A \subseteq x \to x \in (L ↾_{𝑡} A))$
49	22 48	sylbid	$⊢ ((L \in Fil (Y) \land A \subseteq Y) \land x \subseteq A) \to (\exists y \in (L ↾_{𝑡} A) y \subseteq x \to x \in (L ↾_{𝑡} A))$
50	49	ex	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to (x \subseteq A \to (\exists y \in (L ↾_{𝑡} A) y \subseteq x \to x \in (L ↾_{𝑡} A)))$
51	13 50	syl5	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to (x \in 𝒫 A \to (\exists y \in (L ↾_{𝑡} A) y \subseteq x \to x \in (L ↾_{𝑡} A)))$
52	51	ralrimiv	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to \forall x \in 𝒫 A (\exists y \in (L ↾_{𝑡} A) y \subseteq x \to x \in (L ↾_{𝑡} A))$
53		simpll	$⊢ ((L \in Fil (Y) \land A \subseteq Y) \land (z \in L \land u \in L)) \to L \in Fil (Y)$
54	8	adantr	$⊢ ((L \in Fil (Y) \land A \subseteq Y) \land (z \in L \land u \in L)) \to A \in V$
55		filin	$⊢ (L \in Fil (Y) \land z \in L \land u \in L) \to z \cap u \in L$
56	55	3expb	$⊢ (L \in Fil (Y) \land (z \in L \land u \in L)) \to z \cap u \in L$
57	56	adantlr	$⊢ ((L \in Fil (Y) \land A \subseteq Y) \land (z \in L \land u \in L)) \to z \cap u \in L$
58		elrestr	$⊢ (L \in Fil (Y) \land A \in V \land z \cap u \in L) \to (z \cap u) \cap A \in (L ↾_{𝑡} A)$
59	53 54 57 58	syl3anc	$⊢ ((L \in Fil (Y) \land A \subseteq Y) \land (z \in L \land u \in L)) \to (z \cap u) \cap A \in (L ↾_{𝑡} A)$
60	59	ralrimivva	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to \forall z \in L \forall u \in L (z \cap u) \cap A \in (L ↾_{𝑡} A)$
61		vex	$⊢ z \in V$
62	61	inex1	$⊢ z \cap A \in V$
63	62	a1i	$⊢ ((L \in Fil (Y) \land A \subseteq Y) \land z \in L) \to z \cap A \in V$
64		elrest	$⊢ (L \in Fil (Y) \land A \in V) \to (x \in (L ↾_{𝑡} A) \leftrightarrow \exists z \in L x = z \cap A)$
65	8 64	syldan	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to (x \in (L ↾_{𝑡} A) \leftrightarrow \exists z \in L x = z \cap A)$
66	15	a1i	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x = z \cap A) \land u \in L) \to u \cap A \in V$
67	18	adantr	$⊢ ((L \in Fil (Y) \land A \subseteq Y) \land x = z \cap A) \to (y \in (L ↾_{𝑡} A) \leftrightarrow \exists u \in L y = u \cap A)$
68		ineq12	$⊢ (x = z \cap A \land y = u \cap A) \to x \cap y = (z \cap A) \cap (u \cap A)$
69		inindir	$⊢ (z \cap u) \cap A = (z \cap A) \cap (u \cap A)$
70	68 69	eqtr4di	$⊢ (x = z \cap A \land y = u \cap A) \to x \cap y = (z \cap u) \cap A$
71	70	adantll	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x = z \cap A) \land y = u \cap A) \to x \cap y = (z \cap u) \cap A$
72	71	eleq1d	$⊢ (((L \in Fil (Y) \land A \subseteq Y) \land x = z \cap A) \land y = u \cap A) \to (x \cap y \in (L ↾_{𝑡} A) \leftrightarrow (z \cap u) \cap A \in (L ↾_{𝑡} A))$
73	66 67 72	ralxfr2d	$⊢ ((L \in Fil (Y) \land A \subseteq Y) \land x = z \cap A) \to (\forall y \in (L ↾_{𝑡} A) x \cap y \in (L ↾_{𝑡} A) \leftrightarrow \forall u \in L (z \cap u) \cap A \in (L ↾_{𝑡} A))$
74	63 65 73	ralxfr2d	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to (\forall x \in (L ↾_{𝑡} A) \forall y \in (L ↾_{𝑡} A) x \cap y \in (L ↾_{𝑡} A) \leftrightarrow \forall z \in L \forall u \in L (z \cap u) \cap A \in (L ↾_{𝑡} A))$
75	60 74	mpbird	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to \forall x \in (L ↾_{𝑡} A) \forall y \in (L ↾_{𝑡} A) x \cap y \in (L ↾_{𝑡} A)$
76		isfil2	$⊢ L ↾_{𝑡} A \in Fil (A) \leftrightarrow ((L ↾_{𝑡} A \subseteq 𝒫 A \land \neg \emptyset \in (L ↾_{𝑡} A) \land A \in (L ↾_{𝑡} A)) \land \forall x \in 𝒫 A (\exists y \in (L ↾_{𝑡} A) y \subseteq x \to x \in (L ↾_{𝑡} A)) \land \forall x \in (L ↾_{𝑡} A) \forall y \in (L ↾_{𝑡} A) x \cap y \in (L ↾_{𝑡} A))$
77		restsspw	$⊢ L ↾_{𝑡} A \subseteq 𝒫 A$
78		3anass	$⊢ (L ↾_{𝑡} A \subseteq 𝒫 A \land \neg \emptyset \in (L ↾_{𝑡} A) \land A \in (L ↾_{𝑡} A)) \leftrightarrow (L ↾_{𝑡} A \subseteq 𝒫 A \land (\neg \emptyset \in (L ↾_{𝑡} A) \land A \in (L ↾_{𝑡} A)))$
79	77 78	mpbiran	$⊢ (L ↾_{𝑡} A \subseteq 𝒫 A \land \neg \emptyset \in (L ↾_{𝑡} A) \land A \in (L ↾_{𝑡} A)) \leftrightarrow (\neg \emptyset \in (L ↾_{𝑡} A) \land A \in (L ↾_{𝑡} A))$
80	79	3anbi1i	$⊢ ((L ↾_{𝑡} A \subseteq 𝒫 A \land \neg \emptyset \in (L ↾_{𝑡} A) \land A \in (L ↾_{𝑡} A)) \land \forall x \in 𝒫 A (\exists y \in (L ↾_{𝑡} A) y \subseteq x \to x \in (L ↾_{𝑡} A)) \land \forall x \in (L ↾_{𝑡} A) \forall y \in (L ↾_{𝑡} A) x \cap y \in (L ↾_{𝑡} A)) \leftrightarrow ((\neg \emptyset \in (L ↾_{𝑡} A) \land A \in (L ↾_{𝑡} A)) \land \forall x \in 𝒫 A (\exists y \in (L ↾_{𝑡} A) y \subseteq x \to x \in (L ↾_{𝑡} A)) \land \forall x \in (L ↾_{𝑡} A) \forall y \in (L ↾_{𝑡} A) x \cap y \in (L ↾_{𝑡} A))$
81		3anass	$⊢ ((\neg \emptyset \in (L ↾_{𝑡} A) \land A \in (L ↾_{𝑡} A)) \land \forall x \in 𝒫 A (\exists y \in (L ↾_{𝑡} A) y \subseteq x \to x \in (L ↾_{𝑡} A)) \land \forall x \in (L ↾_{𝑡} A) \forall y \in (L ↾_{𝑡} A) x \cap y \in (L ↾_{𝑡} A)) \leftrightarrow ((\neg \emptyset \in (L ↾_{𝑡} A) \land A \in (L ↾_{𝑡} A)) \land (\forall x \in 𝒫 A (\exists y \in (L ↾_{𝑡} A) y \subseteq x \to x \in (L ↾_{𝑡} A)) \land \forall x \in (L ↾_{𝑡} A) \forall y \in (L ↾_{𝑡} A) x \cap y \in (L ↾_{𝑡} A)))$
82	76 80 81	3bitri	$⊢ L ↾_{𝑡} A \in Fil (A) \leftrightarrow ((\neg \emptyset \in (L ↾_{𝑡} A) \land A \in (L ↾_{𝑡} A)) \land (\forall x \in 𝒫 A (\exists y \in (L ↾_{𝑡} A) y \subseteq x \to x \in (L ↾_{𝑡} A)) \land \forall x \in (L ↾_{𝑡} A) \forall y \in (L ↾_{𝑡} A) x \cap y \in (L ↾_{𝑡} A)))$
83		anass	$⊢ ((\neg \emptyset \in (L ↾_{𝑡} A) \land A \in (L ↾_{𝑡} A)) \land (\forall x \in 𝒫 A (\exists y \in (L ↾_{𝑡} A) y \subseteq x \to x \in (L ↾_{𝑡} A)) \land \forall x \in (L ↾_{𝑡} A) \forall y \in (L ↾_{𝑡} A) x \cap y \in (L ↾_{𝑡} A))) \leftrightarrow (\neg \emptyset \in (L ↾_{𝑡} A) \land (A \in (L ↾_{𝑡} A) \land (\forall x \in 𝒫 A (\exists y \in (L ↾_{𝑡} A) y \subseteq x \to x \in (L ↾_{𝑡} A)) \land \forall x \in (L ↾_{𝑡} A) \forall y \in (L ↾_{𝑡} A) x \cap y \in (L ↾_{𝑡} A))))$
84		ancom	$⊢ (\neg \emptyset \in (L ↾_{𝑡} A) \land (A \in (L ↾_{𝑡} A) \land (\forall x \in 𝒫 A (\exists y \in (L ↾_{𝑡} A) y \subseteq x \to x \in (L ↾_{𝑡} A)) \land \forall x \in (L ↾_{𝑡} A) \forall y \in (L ↾_{𝑡} A) x \cap y \in (L ↾_{𝑡} A)))) \leftrightarrow ((A \in (L ↾_{𝑡} A) \land (\forall x \in 𝒫 A (\exists y \in (L ↾_{𝑡} A) y \subseteq x \to x \in (L ↾_{𝑡} A)) \land \forall x \in (L ↾_{𝑡} A) \forall y \in (L ↾_{𝑡} A) x \cap y \in (L ↾_{𝑡} A))) \land \neg \emptyset \in (L ↾_{𝑡} A))$
85	82 83 84	3bitri	$⊢ L ↾_{𝑡} A \in Fil (A) \leftrightarrow ((A \in (L ↾_{𝑡} A) \land (\forall x \in 𝒫 A (\exists y \in (L ↾_{𝑡} A) y \subseteq x \to x \in (L ↾_{𝑡} A)) \land \forall x \in (L ↾_{𝑡} A) \forall y \in (L ↾_{𝑡} A) x \cap y \in (L ↾_{𝑡} A))) \land \neg \emptyset \in (L ↾_{𝑡} A))$
86	85	baib	$⊢ (A \in (L ↾_{𝑡} A) \land (\forall x \in 𝒫 A (\exists y \in (L ↾_{𝑡} A) y \subseteq x \to x \in (L ↾_{𝑡} A)) \land \forall x \in (L ↾_{𝑡} A) \forall y \in (L ↾_{𝑡} A) x \cap y \in (L ↾_{𝑡} A))) \to (L ↾_{𝑡} A \in Fil (A) \leftrightarrow \neg \emptyset \in (L ↾_{𝑡} A))$
87	12 52 75 86	syl12anc	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to (L ↾_{𝑡} A \in Fil (A) \leftrightarrow \neg \emptyset \in (L ↾_{𝑡} A))$
88		nesym	$⊢ v \cap A \neq \emptyset \leftrightarrow \neg \emptyset = v \cap A$
89	88	ralbii	$⊢ \forall v \in L v \cap A \neq \emptyset \leftrightarrow \forall v \in L \neg \emptyset = v \cap A$
90		elrest	$⊢ (L \in Fil (Y) \land A \in V) \to (\emptyset \in (L ↾_{𝑡} A) \leftrightarrow \exists v \in L \emptyset = v \cap A)$
91	8 90	syldan	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to (\emptyset \in (L ↾_{𝑡} A) \leftrightarrow \exists v \in L \emptyset = v \cap A)$
92		dfrex2	$⊢ \exists v \in L \emptyset = v \cap A \leftrightarrow \neg \forall v \in L \neg \emptyset = v \cap A$
93	91 92	bitrdi	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to (\emptyset \in (L ↾_{𝑡} A) \leftrightarrow \neg \forall v \in L \neg \emptyset = v \cap A)$
94	93	con2bid	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to (\forall v \in L \neg \emptyset = v \cap A \leftrightarrow \neg \emptyset \in (L ↾_{𝑡} A))$
95	89 94	bitrid	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to (\forall v \in L v \cap A \neq \emptyset \leftrightarrow \neg \emptyset \in (L ↾_{𝑡} A))$
96	87 95	bitr4d	$⊢ (L \in Fil (Y) \land A \subseteq Y) \to (L ↾_{𝑡} A \in Fil (A) \leftrightarrow \forall v \in L v \cap A \neq \emptyset)$

Metamath Proof Explorer

Theorem trfil2

Proof