Theorem trfil2 24013

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

Assertion

Ref	Expression
trfil2	⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ∀𝑣 ∈ 𝐿 (𝑣 ∩ 𝐴) ≠ ∅))

Distinct variable groups:   𝑣,𝐴   𝑣,𝐿   𝑣,𝑌

Proof of Theorem trfil2

Dummy variables 𝑢 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 489	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐴 ⊆ 𝑌)
2		sseqin2 4184	. . . . 5 ⊢ (𝐴 ⊆ 𝑌 ↔ (𝑌 ∩ 𝐴) = 𝐴)
3	1, 2	sylib 221	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑌 ∩ 𝐴) = 𝐴)
4		simpl 487	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐿 ∈ (Fil‘𝑌))
5		id 23	. . . . . 6 ⊢ (𝐴 ⊆ 𝑌 → 𝐴 ⊆ 𝑌)
6		filtop 23981	. . . . . 6 ⊢ (𝐿 ∈ (Fil‘𝑌) → 𝑌 ∈ 𝐿)
7		ssexg 5294	. . . . . 6 ⊢ ((𝐴 ⊆ 𝑌 ∧ 𝑌 ∈ 𝐿) → 𝐴 ∈ V)
8	5, 6, 7	syl2anr 608	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐴 ∈ V)
9	6	adantr 485	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝑌 ∈ 𝐿)
10		elrestr 17481	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ 𝑌 ∈ 𝐿) → (𝑌 ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
11	4, 8, 9, 10	syl3anc 1396	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑌 ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
12	3, 11	eqeltrrd 2870	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐴 ∈ (𝐿 ↾t 𝐴))
13		elpwi 4574	. . . . 5 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴)
14		vex 3467	. . . . . . . . . 10 ⊢ 𝑢 ∈ V
15	14	inex1 5288	. . . . . . . . 9 ⊢ (𝑢 ∩ 𝐴) ∈ V
16	15	a1i 11	. . . . . . . 8 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑢 ∈ 𝐿) → (𝑢 ∩ 𝐴) ∈ V)
17		elrest 17480	. . . . . . . . . 10 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
18	8, 17	syldan 602	. . . . . . . . 9 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
19	18	adantr 485	. . . . . . . 8 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
20		simpr 489	. . . . . . . . 9 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → 𝑦 = (𝑢 ∩ 𝐴))
21	20	sseq1d 3976	. . . . . . . 8 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑦 ⊆ 𝑥 ↔ (𝑢 ∩ 𝐴) ⊆ 𝑥))
22	16, 19, 21	rexxfr2d 5383	. . . . . . 7 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 ↔ ∃𝑢 ∈ 𝐿 (𝑢 ∩ 𝐴) ⊆ 𝑥))
23		indir 4247	. . . . . . . . . 10 ⊢ ((𝑢 ∪ 𝑥) ∩ 𝐴) = ((𝑢 ∩ 𝐴) ∪ (𝑥 ∩ 𝐴))
24		simplr 780	. . . . . . . . . . . . 13 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑥 ⊆ 𝐴)
25		dfss2 3931	. . . . . . . . . . . . 13 ⊢ (𝑥 ⊆ 𝐴 ↔ (𝑥 ∩ 𝐴) = 𝑥)
26	24, 25	sylib 221	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑥 ∩ 𝐴) = 𝑥)
27	26	uneq2d 4130	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∩ 𝐴) ∪ (𝑥 ∩ 𝐴)) = ((𝑢 ∩ 𝐴) ∪ 𝑥))
28		simprr 784	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑢 ∩ 𝐴) ⊆ 𝑥)
29		ssequn1 4147	. . . . . . . . . . . 12 ⊢ ((𝑢 ∩ 𝐴) ⊆ 𝑥 ↔ ((𝑢 ∩ 𝐴) ∪ 𝑥) = 𝑥)
30	28, 29	sylib 221	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∩ 𝐴) ∪ 𝑥) = 𝑥)
31	27, 30	eqtrd 2804	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∩ 𝐴) ∪ (𝑥 ∩ 𝐴)) = 𝑥)
32	23, 31	eqtrid 2816	. . . . . . . . 9 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∪ 𝑥) ∩ 𝐴) = 𝑥)
33		simplll 786	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝐿 ∈ (Fil‘𝑌))
34		simpllr 787	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝐴 ⊆ 𝑌)
35	33, 34, 8	syl2anc 595	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝐴 ∈ V)
36		simprl 782	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑢 ∈ 𝐿)
37		filelss 23978	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑢 ∈ 𝐿) → 𝑢 ⊆ 𝑌)
38	33, 36, 37	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑢 ⊆ 𝑌)
39	24, 34	sstrd 3955	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑥 ⊆ 𝑌)
40	38, 39	unssd 4153	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑢 ∪ 𝑥) ⊆ 𝑌)
41		ssun1 4139	. . . . . . . . . . . 12 ⊢ 𝑢 ⊆ (𝑢 ∪ 𝑥)
42	41	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑢 ⊆ (𝑢 ∪ 𝑥))
43		filss 23979	. . . . . . . . . . 11 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∪ 𝑥) ⊆ 𝑌 ∧ 𝑢 ⊆ (𝑢 ∪ 𝑥))) → (𝑢 ∪ 𝑥) ∈ 𝐿)
44	33, 36, 40, 42, 43	syl13anc 1397	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑢 ∪ 𝑥) ∈ 𝐿)
45		elrestr 17481	. . . . . . . . . 10 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑢 ∪ 𝑥) ∈ 𝐿) → ((𝑢 ∪ 𝑥) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
46	33, 35, 44, 45	syl3anc 1396	. . . . . . . . 9 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∪ 𝑥) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
47	32, 46	eqeltrrd 2870	. . . . . . . 8 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑥 ∈ (𝐿 ↾t 𝐴))
48	47	rexlimdvaa 3173	. . . . . . 7 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (∃𝑢 ∈ 𝐿 (𝑢 ∩ 𝐴) ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)))
49	22, 48	sylbid 243	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)))
50	49	ex 417	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑥 ⊆ 𝐴 → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴))))
51	13, 50	syl5 35	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑥 ∈ 𝒫 𝐴 → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴))))
52	51	ralrimiv 3162	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)))
53		simpll 778	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → 𝐿 ∈ (Fil‘𝑌))
54	8	adantr 485	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → 𝐴 ∈ V)
55		filin 23980	. . . . . . . 8 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿) → (𝑧 ∩ 𝑢) ∈ 𝐿)
56	55	3expb 1136	. . . . . . 7 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → (𝑧 ∩ 𝑢) ∈ 𝐿)
57	56	adantlr 727	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → (𝑧 ∩ 𝑢) ∈ 𝐿)
58		elrestr 17481	. . . . . 6 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑧 ∩ 𝑢) ∈ 𝐿) → ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
59	53, 54, 57, 58	syl3anc 1396	. . . . 5 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
60	59	ralrimivva 3214	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ∀𝑧 ∈ 𝐿 ∀𝑢 ∈ 𝐿 ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
61		vex 3467	. . . . . . 7 ⊢ 𝑧 ∈ V
62	61	inex1 5288	. . . . . 6 ⊢ (𝑧 ∩ 𝐴) ∈ V
63	62	a1i 11	. . . . 5 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑧 ∈ 𝐿) → (𝑧 ∩ 𝐴) ∈ V)
64		elrest 17480	. . . . . 6 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑥 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑧 ∈ 𝐿 𝑥 = (𝑧 ∩ 𝐴)))
65	8, 64	syldan 602	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑥 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑧 ∈ 𝐿 𝑥 = (𝑧 ∩ 𝐴)))
66	15	a1i 11	. . . . . 6 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) ∧ 𝑢 ∈ 𝐿) → (𝑢 ∩ 𝐴) ∈ V)
67	18	adantr 485	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
68		ineq12 4176	. . . . . . . . 9 ⊢ ((𝑥 = (𝑧 ∩ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑥 ∩ 𝑦) = ((𝑧 ∩ 𝐴) ∩ (𝑢 ∩ 𝐴)))
69		inindir 4196	. . . . . . . . 9 ⊢ ((𝑧 ∩ 𝑢) ∩ 𝐴) = ((𝑧 ∩ 𝐴) ∩ (𝑢 ∩ 𝐴))
70	68, 69	eqtr4di 2822	. . . . . . . 8 ⊢ ((𝑥 = (𝑧 ∩ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑥 ∩ 𝑦) = ((𝑧 ∩ 𝑢) ∩ 𝐴))
71	70	adantll 726	. . . . . . 7 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑥 ∩ 𝑦) = ((𝑧 ∩ 𝑢) ∩ 𝐴))
72	71	eleq1d 2854	. . . . . 6 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → ((𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴) ↔ ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴)))
73	66, 67, 72	ralxfr2d 5382	. . . . 5 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) → (∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴) ↔ ∀𝑢 ∈ 𝐿 ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴)))
74	63, 65, 73	ralxfr2d 5382	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴) ↔ ∀𝑧 ∈ 𝐿 ∀𝑢 ∈ 𝐿 ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴)))
75	60, 74	mpbird 260	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))
76		isfil2 23982	. . . . . 6 ⊢ ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ (((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))
77		restsspw 17484	. . . . . . . 8 ⊢ (𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴
78		3anass 1109	. . . . . . . 8 ⊢ (((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ↔ ((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ (¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴))))
79	77, 78	mpbiran 721	. . . . . . 7 ⊢ (((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ↔ (¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)))
80	79	3anbi1i 1173	. . . . . 6 ⊢ ((((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))
81		3anass 1109	. . . . . 6 ⊢ (((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))))
82	76, 80, 81	3bitri 300	. . . . 5 ⊢ ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))))
83		anass 473	. . . . 5 ⊢ (((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) ↔ (¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ (𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))))
84		ancom 465	. . . . 5 ⊢ ((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ (𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))) ↔ ((𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
85	82, 83, 84	3bitri 300	. . . 4 ⊢ ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ((𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
86	85	baib 544	. . 3 ⊢ ((𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
87	12, 52, 75, 86	syl12anc 849	. 2 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
88		nesym 3020	. . . 4 ⊢ ((𝑣 ∩ 𝐴) ≠ ∅ ↔ ¬ ∅ = (𝑣 ∩ 𝐴))
89	88	ralbii 3117	. . 3 ⊢ (∀𝑣 ∈ 𝐿 (𝑣 ∩ 𝐴) ≠ ∅ ↔ ∀𝑣 ∈ 𝐿 ¬ ∅ = (𝑣 ∩ 𝐴))
90		elrest 17480	. . . . . 6 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (∅ ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑣 ∈ 𝐿 ∅ = (𝑣 ∩ 𝐴)))
91	8, 90	syldan 602	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∅ ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑣 ∈ 𝐿 ∅ = (𝑣 ∩ 𝐴)))
92		dfrex2 3098	. . . . 5 ⊢ (∃𝑣 ∈ 𝐿 ∅ = (𝑣 ∩ 𝐴) ↔ ¬ ∀𝑣 ∈ 𝐿 ¬ ∅ = (𝑣 ∩ 𝐴))
93	91, 92	bitrdi 290	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∅ ∈ (𝐿 ↾t 𝐴) ↔ ¬ ∀𝑣 ∈ 𝐿 ¬ ∅ = (𝑣 ∩ 𝐴)))
94	93	con2bid 357	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∀𝑣 ∈ 𝐿 ¬ ∅ = (𝑣 ∩ 𝐴) ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
95	89, 94	bitrid 286	. 2 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∀𝑣 ∈ 𝐿 (𝑣 ∩ 𝐴) ≠ ∅ ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
96	87, 95	bitr4d 285	1 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ∀𝑣 ∈ 𝐿 (𝑣 ∩ 𝐴) ≠ ∅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  ∀wral 3085  ∃wrex 3095  Vcvv 3463   ∪ cun 3911   ∩ cin 3912   ⊆ wss 3913  ∅c0 4294  𝒫 cpw 4567  ‘cfv 6537  (class class class)co 7411   ↾_t crest 17473  Filcfil 23971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7986  df-2nd 7987  df-rest 17475  df-fbas 21488  df-fil 23972

This theorem is referenced by:  trfil3  24014  trnei  24018