Theorem trfil2 23947

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 488	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐴 ⊆ 𝑌)
2		sseqin2 4175	. . . . 5 ⊢ (𝐴 ⊆ 𝑌 ↔ (𝑌 ∩ 𝐴) = 𝐴)
3	1, 2	sylib 220	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑌 ∩ 𝐴) = 𝐴)
4		simpl 486	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐿 ∈ (Fil‘𝑌))
5		id 22	. . . . . 6 ⊢ (𝐴 ⊆ 𝑌 → 𝐴 ⊆ 𝑌)
6		filtop 23915	. . . . . 6 ⊢ (𝐿 ∈ (Fil‘𝑌) → 𝑌 ∈ 𝐿)
7		ssexg 5279	. . . . . 6 ⊢ ((𝐴 ⊆ 𝑌 ∧ 𝑌 ∈ 𝐿) → 𝐴 ∈ V)
8	5, 6, 7	syl2anr 606	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐴 ∈ V)
9	6	adantr 484	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝑌 ∈ 𝐿)
10		elrestr 17457	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ 𝑌 ∈ 𝐿) → (𝑌 ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
11	4, 8, 9, 10	syl3anc 1390	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑌 ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
12	3, 11	eqeltrrd 2863	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐴 ∈ (𝐿 ↾t 𝐴))
13		elpwi 4562	. . . . 5 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴)
14		vex 3458	. . . . . . . . . 10 ⊢ 𝑢 ∈ V
15	14	inex1 5273	. . . . . . . . 9 ⊢ (𝑢 ∩ 𝐴) ∈ V
16	15	a1i 11	. . . . . . . 8 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑢 ∈ 𝐿) → (𝑢 ∩ 𝐴) ∈ V)
17		elrest 17456	. . . . . . . . . 10 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
18	8, 17	syldan 600	. . . . . . . . 9 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
19	18	adantr 484	. . . . . . . 8 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
20		simpr 488	. . . . . . . . 9 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → 𝑦 = (𝑢 ∩ 𝐴))
21	20	sseq1d 3967	. . . . . . . 8 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑦 ⊆ 𝑥 ↔ (𝑢 ∩ 𝐴) ⊆ 𝑥))
22	16, 19, 21	rexxfr2d 5368	. . . . . . 7 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 ↔ ∃𝑢 ∈ 𝐿 (𝑢 ∩ 𝐴) ⊆ 𝑥))
23		indir 4238	. . . . . . . . . 10 ⊢ ((𝑢 ∪ 𝑥) ∩ 𝐴) = ((𝑢 ∩ 𝐴) ∪ (𝑥 ∩ 𝐴))
24		simplr 778	. . . . . . . . . . . . 13 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑥 ⊆ 𝐴)
25		dfss2 3922	. . . . . . . . . . . . 13 ⊢ (𝑥 ⊆ 𝐴 ↔ (𝑥 ∩ 𝐴) = 𝑥)
26	24, 25	sylib 220	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑥 ∩ 𝐴) = 𝑥)
27	26	uneq2d 4121	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∩ 𝐴) ∪ (𝑥 ∩ 𝐴)) = ((𝑢 ∩ 𝐴) ∪ 𝑥))
28		simprr 782	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑢 ∩ 𝐴) ⊆ 𝑥)
29		ssequn1 4138	. . . . . . . . . . . 12 ⊢ ((𝑢 ∩ 𝐴) ⊆ 𝑥 ↔ ((𝑢 ∩ 𝐴) ∪ 𝑥) = 𝑥)
30	28, 29	sylib 220	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∩ 𝐴) ∪ 𝑥) = 𝑥)
31	27, 30	eqtrd 2797	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∩ 𝐴) ∪ (𝑥 ∩ 𝐴)) = 𝑥)
32	23, 31	eqtrid 2809	. . . . . . . . 9 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∪ 𝑥) ∩ 𝐴) = 𝑥)
33		simplll 784	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝐿 ∈ (Fil‘𝑌))
34		simpllr 785	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝐴 ⊆ 𝑌)
35	33, 34, 8	syl2anc 593	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝐴 ∈ V)
36		simprl 780	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑢 ∈ 𝐿)
37		filelss 23912	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑢 ∈ 𝐿) → 𝑢 ⊆ 𝑌)
38	33, 36, 37	syl2anc 593	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑢 ⊆ 𝑌)
39	24, 34	sstrd 3946	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑥 ⊆ 𝑌)
40	38, 39	unssd 4144	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑢 ∪ 𝑥) ⊆ 𝑌)
41		ssun1 4130	. . . . . . . . . . . 12 ⊢ 𝑢 ⊆ (𝑢 ∪ 𝑥)
42	41	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑢 ⊆ (𝑢 ∪ 𝑥))
43		filss 23913	. . . . . . . . . . 11 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∪ 𝑥) ⊆ 𝑌 ∧ 𝑢 ⊆ (𝑢 ∪ 𝑥))) → (𝑢 ∪ 𝑥) ∈ 𝐿)
44	33, 36, 40, 42, 43	syl13anc 1391	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑢 ∪ 𝑥) ∈ 𝐿)
45		elrestr 17457	. . . . . . . . . 10 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑢 ∪ 𝑥) ∈ 𝐿) → ((𝑢 ∪ 𝑥) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
46	33, 35, 44, 45	syl3anc 1390	. . . . . . . . 9 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∪ 𝑥) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
47	32, 46	eqeltrrd 2863	. . . . . . . 8 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑥 ∈ (𝐿 ↾t 𝐴))
48	47	rexlimdvaa 3164	. . . . . . 7 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (∃𝑢 ∈ 𝐿 (𝑢 ∩ 𝐴) ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)))
49	22, 48	sylbid 242	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)))
50	49	ex 416	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑥 ⊆ 𝐴 → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴))))
51	13, 50	syl5 34	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑥 ∈ 𝒫 𝐴 → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴))))
52	51	ralrimiv 3153	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)))
53		simpll 776	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → 𝐿 ∈ (Fil‘𝑌))
54	8	adantr 484	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → 𝐴 ∈ V)
55		filin 23914	. . . . . . . 8 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿) → (𝑧 ∩ 𝑢) ∈ 𝐿)
56	55	3expb 1133	. . . . . . 7 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → (𝑧 ∩ 𝑢) ∈ 𝐿)
57	56	adantlr 725	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → (𝑧 ∩ 𝑢) ∈ 𝐿)
58		elrestr 17457	. . . . . 6 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑧 ∩ 𝑢) ∈ 𝐿) → ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
59	53, 54, 57, 58	syl3anc 1390	. . . . 5 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
60	59	ralrimivva 3205	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ∀𝑧 ∈ 𝐿 ∀𝑢 ∈ 𝐿 ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
61		vex 3458	. . . . . . 7 ⊢ 𝑧 ∈ V
62	61	inex1 5273	. . . . . 6 ⊢ (𝑧 ∩ 𝐴) ∈ V
63	62	a1i 11	. . . . 5 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑧 ∈ 𝐿) → (𝑧 ∩ 𝐴) ∈ V)
64		elrest 17456	. . . . . 6 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑥 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑧 ∈ 𝐿 𝑥 = (𝑧 ∩ 𝐴)))
65	8, 64	syldan 600	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑥 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑧 ∈ 𝐿 𝑥 = (𝑧 ∩ 𝐴)))
66	15	a1i 11	. . . . . 6 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) ∧ 𝑢 ∈ 𝐿) → (𝑢 ∩ 𝐴) ∈ V)
67	18	adantr 484	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
68		ineq12 4167	. . . . . . . . 9 ⊢ ((𝑥 = (𝑧 ∩ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑥 ∩ 𝑦) = ((𝑧 ∩ 𝐴) ∩ (𝑢 ∩ 𝐴)))
69		inindir 4187	. . . . . . . . 9 ⊢ ((𝑧 ∩ 𝑢) ∩ 𝐴) = ((𝑧 ∩ 𝐴) ∩ (𝑢 ∩ 𝐴))
70	68, 69	eqtr4di 2815	. . . . . . . 8 ⊢ ((𝑥 = (𝑧 ∩ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑥 ∩ 𝑦) = ((𝑧 ∩ 𝑢) ∩ 𝐴))
71	70	adantll 724	. . . . . . 7 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑥 ∩ 𝑦) = ((𝑧 ∩ 𝑢) ∩ 𝐴))
72	71	eleq1d 2847	. . . . . 6 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → ((𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴) ↔ ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴)))
73	66, 67, 72	ralxfr2d 5367	. . . . 5 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) → (∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴) ↔ ∀𝑢 ∈ 𝐿 ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴)))
74	63, 65, 73	ralxfr2d 5367	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴) ↔ ∀𝑧 ∈ 𝐿 ∀𝑢 ∈ 𝐿 ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴)))
75	60, 74	mpbird 259	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))
76		isfil2 23916	. . . . . 6 ⊢ ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ (((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))
77		restsspw 17460	. . . . . . . 8 ⊢ (𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴
78		3anass 1106	. . . . . . . 8 ⊢ (((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ↔ ((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ (¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴))))
79	77, 78	mpbiran 719	. . . . . . 7 ⊢ (((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ↔ (¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)))
80	79	3anbi1i 1170	. . . . . 6 ⊢ ((((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))
81		3anass 1106	. . . . . 6 ⊢ (((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))))
82	76, 80, 81	3bitri 299	. . . . 5 ⊢ ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))))
83		anass 472	. . . . 5 ⊢ (((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) ↔ (¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ (𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))))
84		ancom 464	. . . . 5 ⊢ ((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ (𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))) ↔ ((𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
85	82, 83, 84	3bitri 299	. . . 4 ⊢ ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ((𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
86	85	baib 543	. . 3 ⊢ ((𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
87	12, 52, 75, 86	syl12anc 847	. 2 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
88		nesym 3013	. . . 4 ⊢ ((𝑣 ∩ 𝐴) ≠ ∅ ↔ ¬ ∅ = (𝑣 ∩ 𝐴))
89	88	ralbii 3108	. . 3 ⊢ (∀𝑣 ∈ 𝐿 (𝑣 ∩ 𝐴) ≠ ∅ ↔ ∀𝑣 ∈ 𝐿 ¬ ∅ = (𝑣 ∩ 𝐴))
90		elrest 17456	. . . . . 6 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (∅ ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑣 ∈ 𝐿 ∅ = (𝑣 ∩ 𝐴)))
91	8, 90	syldan 600	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∅ ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑣 ∈ 𝐿 ∅ = (𝑣 ∩ 𝐴)))
92		dfrex2 3089	. . . . 5 ⊢ (∃𝑣 ∈ 𝐿 ∅ = (𝑣 ∩ 𝐴) ↔ ¬ ∀𝑣 ∈ 𝐿 ¬ ∅ = (𝑣 ∩ 𝐴))
93	91, 92	bitrdi 289	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∅ ∈ (𝐿 ↾t 𝐴) ↔ ¬ ∀𝑣 ∈ 𝐿 ¬ ∅ = (𝑣 ∩ 𝐴)))
94	93	con2bid 356	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∀𝑣 ∈ 𝐿 ¬ ∅ = (𝑣 ∩ 𝐴) ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
95	89, 94	bitrid 285	. 2 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∀𝑣 ∈ 𝐿 (𝑣 ∩ 𝐴) ≠ ∅ ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
96	87, 95	bitr4d 284	1 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ∀𝑣 ∈ 𝐿 (𝑣 ∩ 𝐴) ≠ ∅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1098   = wceq 1560   ∈ wcel 2142   ≠ wne 2957  ∀wral 3076  ∃wrex 3086  Vcvv 3454   ∪ cun 3902   ∩ cin 3903   ⊆ wss 3904  ∅c0 4285  𝒫 cpw 4555  ‘cfv 6521  (class class class)co 7396   ↾_t crest 17449  Filcfil 23905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-1st 7970  df-2nd 7971  df-rest 17451  df-fbas 21421  df-fil 23906

This theorem is referenced by:  trfil3  23948  trnei  23952