Theorem trfil2 23829

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 484	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐴 ⊆ 𝑌)
2		sseqin2 4173	. . . . 5 ⊢ (𝐴 ⊆ 𝑌 ↔ (𝑌 ∩ 𝐴) = 𝐴)
3	1, 2	sylib 218	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑌 ∩ 𝐴) = 𝐴)
4		simpl 482	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐿 ∈ (Fil‘𝑌))
5		id 22	. . . . . 6 ⊢ (𝐴 ⊆ 𝑌 → 𝐴 ⊆ 𝑌)
6		filtop 23797	. . . . . 6 ⊢ (𝐿 ∈ (Fil‘𝑌) → 𝑌 ∈ 𝐿)
7		ssexg 5266	. . . . . 6 ⊢ ((𝐴 ⊆ 𝑌 ∧ 𝑌 ∈ 𝐿) → 𝐴 ∈ V)
8	5, 6, 7	syl2anr 597	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐴 ∈ V)
9	6	adantr 480	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝑌 ∈ 𝐿)
10		elrestr 17346	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ 𝑌 ∈ 𝐿) → (𝑌 ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
11	4, 8, 9, 10	syl3anc 1373	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑌 ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
12	3, 11	eqeltrrd 2835	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐴 ∈ (𝐿 ↾t 𝐴))
13		elpwi 4559	. . . . 5 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴)
14		vex 3442	. . . . . . . . . 10 ⊢ 𝑢 ∈ V
15	14	inex1 5260	. . . . . . . . 9 ⊢ (𝑢 ∩ 𝐴) ∈ V
16	15	a1i 11	. . . . . . . 8 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑢 ∈ 𝐿) → (𝑢 ∩ 𝐴) ∈ V)
17		elrest 17345	. . . . . . . . . 10 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
18	8, 17	syldan 591	. . . . . . . . 9 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
19	18	adantr 480	. . . . . . . 8 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
20		simpr 484	. . . . . . . . 9 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → 𝑦 = (𝑢 ∩ 𝐴))
21	20	sseq1d 3963	. . . . . . . 8 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑦 ⊆ 𝑥 ↔ (𝑢 ∩ 𝐴) ⊆ 𝑥))
22	16, 19, 21	rexxfr2d 5354	. . . . . . 7 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 ↔ ∃𝑢 ∈ 𝐿 (𝑢 ∩ 𝐴) ⊆ 𝑥))
23		indir 4236	. . . . . . . . . 10 ⊢ ((𝑢 ∪ 𝑥) ∩ 𝐴) = ((𝑢 ∩ 𝐴) ∪ (𝑥 ∩ 𝐴))
24		simplr 768	. . . . . . . . . . . . 13 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑥 ⊆ 𝐴)
25		dfss2 3917	. . . . . . . . . . . . 13 ⊢ (𝑥 ⊆ 𝐴 ↔ (𝑥 ∩ 𝐴) = 𝑥)
26	24, 25	sylib 218	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑥 ∩ 𝐴) = 𝑥)
27	26	uneq2d 4118	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∩ 𝐴) ∪ (𝑥 ∩ 𝐴)) = ((𝑢 ∩ 𝐴) ∪ 𝑥))
28		simprr 772	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑢 ∩ 𝐴) ⊆ 𝑥)
29		ssequn1 4136	. . . . . . . . . . . 12 ⊢ ((𝑢 ∩ 𝐴) ⊆ 𝑥 ↔ ((𝑢 ∩ 𝐴) ∪ 𝑥) = 𝑥)
30	28, 29	sylib 218	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∩ 𝐴) ∪ 𝑥) = 𝑥)
31	27, 30	eqtrd 2769	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∩ 𝐴) ∪ (𝑥 ∩ 𝐴)) = 𝑥)
32	23, 31	eqtrid 2781	. . . . . . . . 9 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∪ 𝑥) ∩ 𝐴) = 𝑥)
33		simplll 774	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝐿 ∈ (Fil‘𝑌))
34		simpllr 775	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝐴 ⊆ 𝑌)
35	33, 34, 8	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝐴 ∈ V)
36		simprl 770	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑢 ∈ 𝐿)
37		filelss 23794	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑢 ∈ 𝐿) → 𝑢 ⊆ 𝑌)
38	33, 36, 37	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑢 ⊆ 𝑌)
39	24, 34	sstrd 3942	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑥 ⊆ 𝑌)
40	38, 39	unssd 4142	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑢 ∪ 𝑥) ⊆ 𝑌)
41		ssun1 4128	. . . . . . . . . . . 12 ⊢ 𝑢 ⊆ (𝑢 ∪ 𝑥)
42	41	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑢 ⊆ (𝑢 ∪ 𝑥))
43		filss 23795	. . . . . . . . . . 11 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∪ 𝑥) ⊆ 𝑌 ∧ 𝑢 ⊆ (𝑢 ∪ 𝑥))) → (𝑢 ∪ 𝑥) ∈ 𝐿)
44	33, 36, 40, 42, 43	syl13anc 1374	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑢 ∪ 𝑥) ∈ 𝐿)
45		elrestr 17346	. . . . . . . . . 10 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑢 ∪ 𝑥) ∈ 𝐿) → ((𝑢 ∪ 𝑥) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
46	33, 35, 44, 45	syl3anc 1373	. . . . . . . . 9 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∪ 𝑥) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
47	32, 46	eqeltrrd 2835	. . . . . . . 8 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑥 ∈ (𝐿 ↾t 𝐴))
48	47	rexlimdvaa 3136	. . . . . . 7 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (∃𝑢 ∈ 𝐿 (𝑢 ∩ 𝐴) ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)))
49	22, 48	sylbid 240	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)))
50	49	ex 412	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑥 ⊆ 𝐴 → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴))))
51	13, 50	syl5 34	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑥 ∈ 𝒫 𝐴 → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴))))
52	51	ralrimiv 3125	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)))
53		simpll 766	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → 𝐿 ∈ (Fil‘𝑌))
54	8	adantr 480	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → 𝐴 ∈ V)
55		filin 23796	. . . . . . . 8 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿) → (𝑧 ∩ 𝑢) ∈ 𝐿)
56	55	3expb 1120	. . . . . . 7 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → (𝑧 ∩ 𝑢) ∈ 𝐿)
57	56	adantlr 715	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → (𝑧 ∩ 𝑢) ∈ 𝐿)
58		elrestr 17346	. . . . . 6 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑧 ∩ 𝑢) ∈ 𝐿) → ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
59	53, 54, 57, 58	syl3anc 1373	. . . . 5 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
60	59	ralrimivva 3177	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ∀𝑧 ∈ 𝐿 ∀𝑢 ∈ 𝐿 ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
61		vex 3442	. . . . . . 7 ⊢ 𝑧 ∈ V
62	61	inex1 5260	. . . . . 6 ⊢ (𝑧 ∩ 𝐴) ∈ V
63	62	a1i 11	. . . . 5 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑧 ∈ 𝐿) → (𝑧 ∩ 𝐴) ∈ V)
64		elrest 17345	. . . . . 6 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑥 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑧 ∈ 𝐿 𝑥 = (𝑧 ∩ 𝐴)))
65	8, 64	syldan 591	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑥 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑧 ∈ 𝐿 𝑥 = (𝑧 ∩ 𝐴)))
66	15	a1i 11	. . . . . 6 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) ∧ 𝑢 ∈ 𝐿) → (𝑢 ∩ 𝐴) ∈ V)
67	18	adantr 480	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
68		ineq12 4165	. . . . . . . . 9 ⊢ ((𝑥 = (𝑧 ∩ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑥 ∩ 𝑦) = ((𝑧 ∩ 𝐴) ∩ (𝑢 ∩ 𝐴)))
69		inindir 4186	. . . . . . . . 9 ⊢ ((𝑧 ∩ 𝑢) ∩ 𝐴) = ((𝑧 ∩ 𝐴) ∩ (𝑢 ∩ 𝐴))
70	68, 69	eqtr4di 2787	. . . . . . . 8 ⊢ ((𝑥 = (𝑧 ∩ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑥 ∩ 𝑦) = ((𝑧 ∩ 𝑢) ∩ 𝐴))
71	70	adantll 714	. . . . . . 7 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑥 ∩ 𝑦) = ((𝑧 ∩ 𝑢) ∩ 𝐴))
72	71	eleq1d 2819	. . . . . 6 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → ((𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴) ↔ ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴)))
73	66, 67, 72	ralxfr2d 5353	. . . . 5 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) → (∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴) ↔ ∀𝑢 ∈ 𝐿 ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴)))
74	63, 65, 73	ralxfr2d 5353	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴) ↔ ∀𝑧 ∈ 𝐿 ∀𝑢 ∈ 𝐿 ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴)))
75	60, 74	mpbird 257	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))
76		isfil2 23798	. . . . . 6 ⊢ ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ (((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))
77		restsspw 17349	. . . . . . . 8 ⊢ (𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴
78		3anass 1094	. . . . . . . 8 ⊢ (((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ↔ ((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ (¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴))))
79	77, 78	mpbiran 709	. . . . . . 7 ⊢ (((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ↔ (¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)))
80	79	3anbi1i 1157	. . . . . 6 ⊢ ((((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))
81		3anass 1094	. . . . . 6 ⊢ (((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))))
82	76, 80, 81	3bitri 297	. . . . 5 ⊢ ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))))
83		anass 468	. . . . 5 ⊢ (((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) ↔ (¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ (𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))))
84		ancom 460	. . . . 5 ⊢ ((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ (𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))) ↔ ((𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
85	82, 83, 84	3bitri 297	. . . 4 ⊢ ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ((𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
86	85	baib 535	. . 3 ⊢ ((𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
87	12, 52, 75, 86	syl12anc 836	. 2 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
88		nesym 2986	. . . 4 ⊢ ((𝑣 ∩ 𝐴) ≠ ∅ ↔ ¬ ∅ = (𝑣 ∩ 𝐴))
89	88	ralbii 3080	. . 3 ⊢ (∀𝑣 ∈ 𝐿 (𝑣 ∩ 𝐴) ≠ ∅ ↔ ∀𝑣 ∈ 𝐿 ¬ ∅ = (𝑣 ∩ 𝐴))
90		elrest 17345	. . . . . 6 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (∅ ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑣 ∈ 𝐿 ∅ = (𝑣 ∩ 𝐴)))
91	8, 90	syldan 591	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∅ ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑣 ∈ 𝐿 ∅ = (𝑣 ∩ 𝐴)))
92		dfrex2 3061	. . . . 5 ⊢ (∃𝑣 ∈ 𝐿 ∅ = (𝑣 ∩ 𝐴) ↔ ¬ ∀𝑣 ∈ 𝐿 ¬ ∅ = (𝑣 ∩ 𝐴))
93	91, 92	bitrdi 287	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∅ ∈ (𝐿 ↾t 𝐴) ↔ ¬ ∀𝑣 ∈ 𝐿 ¬ ∅ = (𝑣 ∩ 𝐴)))
94	93	con2bid 354	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∀𝑣 ∈ 𝐿 ¬ ∅ = (𝑣 ∩ 𝐴) ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
95	89, 94	bitrid 283	. 2 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∀𝑣 ∈ 𝐿 (𝑣 ∩ 𝐴) ≠ ∅ ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
96	87, 95	bitr4d 282	1 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ∀𝑣 ∈ 𝐿 (𝑣 ∩ 𝐴) ≠ ∅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113   ≠ wne 2930  ∀wral 3049  ∃wrex 3058  Vcvv 3438   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ∅c0 4283  𝒫 cpw 4552  ‘cfv 6490  (class class class)co 7356   ↾_t crest 17338  Filcfil 23787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-rest 17340  df-fbas 21304  df-fil 23788

This theorem is referenced by:  trfil3  23830  trnei  23834