Theorem trfil2 23870

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 485	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐴 ⊆ 𝑌)
2		sseqin2 4152	. . . . 5 ⊢ (𝐴 ⊆ 𝑌 ↔ (𝑌 ∩ 𝐴) = 𝐴)
3	1, 2	sylib 219	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑌 ∩ 𝐴) = 𝐴)
4		simpl 483	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐿 ∈ (Fil‘𝑌))
5		id 22	. . . . . 6 ⊢ (𝐴 ⊆ 𝑌 → 𝐴 ⊆ 𝑌)
6		filtop 23838	. . . . . 6 ⊢ (𝐿 ∈ (Fil‘𝑌) → 𝑌 ∈ 𝐿)
7		ssexg 5251	. . . . . 6 ⊢ ((𝐴 ⊆ 𝑌 ∧ 𝑌 ∈ 𝐿) → 𝐴 ∈ V)
8	5, 6, 7	syl2anr 603	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐴 ∈ V)
9	6	adantr 481	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝑌 ∈ 𝐿)
10		elrestr 17382	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ 𝑌 ∈ 𝐿) → (𝑌 ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
11	4, 8, 9, 10	syl3anc 1379	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑌 ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
12	3, 11	eqeltrrd 2840	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐴 ∈ (𝐿 ↾t 𝐴))
13		elpwi 4536	. . . . 5 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴)
14		vex 3435	. . . . . . . . . 10 ⊢ 𝑢 ∈ V
15	14	inex1 5245	. . . . . . . . 9 ⊢ (𝑢 ∩ 𝐴) ∈ V
16	15	a1i 11	. . . . . . . 8 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑢 ∈ 𝐿) → (𝑢 ∩ 𝐴) ∈ V)
17		elrest 17381	. . . . . . . . . 10 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
18	8, 17	syldan 597	. . . . . . . . 9 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
19	18	adantr 481	. . . . . . . 8 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
20		simpr 485	. . . . . . . . 9 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → 𝑦 = (𝑢 ∩ 𝐴))
21	20	sseq1d 3946	. . . . . . . 8 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑦 ⊆ 𝑥 ↔ (𝑢 ∩ 𝐴) ⊆ 𝑥))
22	16, 19, 21	rexxfr2d 5340	. . . . . . 7 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 ↔ ∃𝑢 ∈ 𝐿 (𝑢 ∩ 𝐴) ⊆ 𝑥))
23		indir 4214	. . . . . . . . . 10 ⊢ ((𝑢 ∪ 𝑥) ∩ 𝐴) = ((𝑢 ∩ 𝐴) ∪ (𝑥 ∩ 𝐴))
24		simplr 774	. . . . . . . . . . . . 13 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑥 ⊆ 𝐴)
25		dfss2 3901	. . . . . . . . . . . . 13 ⊢ (𝑥 ⊆ 𝐴 ↔ (𝑥 ∩ 𝐴) = 𝑥)
26	24, 25	sylib 219	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑥 ∩ 𝐴) = 𝑥)
27	26	uneq2d 4098	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∩ 𝐴) ∪ (𝑥 ∩ 𝐴)) = ((𝑢 ∩ 𝐴) ∪ 𝑥))
28		simprr 778	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑢 ∩ 𝐴) ⊆ 𝑥)
29		ssequn1 4115	. . . . . . . . . . . 12 ⊢ ((𝑢 ∩ 𝐴) ⊆ 𝑥 ↔ ((𝑢 ∩ 𝐴) ∪ 𝑥) = 𝑥)
30	28, 29	sylib 219	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∩ 𝐴) ∪ 𝑥) = 𝑥)
31	27, 30	eqtrd 2774	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∩ 𝐴) ∪ (𝑥 ∩ 𝐴)) = 𝑥)
32	23, 31	eqtrid 2786	. . . . . . . . 9 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∪ 𝑥) ∩ 𝐴) = 𝑥)
33		simplll 780	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝐿 ∈ (Fil‘𝑌))
34		simpllr 781	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝐴 ⊆ 𝑌)
35	33, 34, 8	syl2anc 590	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝐴 ∈ V)
36		simprl 776	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑢 ∈ 𝐿)
37		filelss 23835	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑢 ∈ 𝐿) → 𝑢 ⊆ 𝑌)
38	33, 36, 37	syl2anc 590	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑢 ⊆ 𝑌)
39	24, 34	sstrd 3925	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑥 ⊆ 𝑌)
40	38, 39	unssd 4121	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑢 ∪ 𝑥) ⊆ 𝑌)
41		ssun1 4107	. . . . . . . . . . . 12 ⊢ 𝑢 ⊆ (𝑢 ∪ 𝑥)
42	41	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑢 ⊆ (𝑢 ∪ 𝑥))
43		filss 23836	. . . . . . . . . . 11 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∪ 𝑥) ⊆ 𝑌 ∧ 𝑢 ⊆ (𝑢 ∪ 𝑥))) → (𝑢 ∪ 𝑥) ∈ 𝐿)
44	33, 36, 40, 42, 43	syl13anc 1380	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑢 ∪ 𝑥) ∈ 𝐿)
45		elrestr 17382	. . . . . . . . . 10 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑢 ∪ 𝑥) ∈ 𝐿) → ((𝑢 ∪ 𝑥) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
46	33, 35, 44, 45	syl3anc 1379	. . . . . . . . 9 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∪ 𝑥) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
47	32, 46	eqeltrrd 2840	. . . . . . . 8 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑥 ∈ (𝐿 ↾t 𝐴))
48	47	rexlimdvaa 3141	. . . . . . 7 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (∃𝑢 ∈ 𝐿 (𝑢 ∩ 𝐴) ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)))
49	22, 48	sylbid 241	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)))
50	49	ex 413	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑥 ⊆ 𝐴 → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴))))
51	13, 50	syl5 34	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑥 ∈ 𝒫 𝐴 → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴))))
52	51	ralrimiv 3130	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)))
53		simpll 772	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → 𝐿 ∈ (Fil‘𝑌))
54	8	adantr 481	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → 𝐴 ∈ V)
55		filin 23837	. . . . . . . 8 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿) → (𝑧 ∩ 𝑢) ∈ 𝐿)
56	55	3expb 1126	. . . . . . 7 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → (𝑧 ∩ 𝑢) ∈ 𝐿)
57	56	adantlr 721	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → (𝑧 ∩ 𝑢) ∈ 𝐿)
58		elrestr 17382	. . . . . 6 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑧 ∩ 𝑢) ∈ 𝐿) → ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
59	53, 54, 57, 58	syl3anc 1379	. . . . 5 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
60	59	ralrimivva 3182	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ∀𝑧 ∈ 𝐿 ∀𝑢 ∈ 𝐿 ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
61		vex 3435	. . . . . . 7 ⊢ 𝑧 ∈ V
62	61	inex1 5245	. . . . . 6 ⊢ (𝑧 ∩ 𝐴) ∈ V
63	62	a1i 11	. . . . 5 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑧 ∈ 𝐿) → (𝑧 ∩ 𝐴) ∈ V)
64		elrest 17381	. . . . . 6 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑥 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑧 ∈ 𝐿 𝑥 = (𝑧 ∩ 𝐴)))
65	8, 64	syldan 597	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑥 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑧 ∈ 𝐿 𝑥 = (𝑧 ∩ 𝐴)))
66	15	a1i 11	. . . . . 6 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) ∧ 𝑢 ∈ 𝐿) → (𝑢 ∩ 𝐴) ∈ V)
67	18	adantr 481	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
68		ineq12 4144	. . . . . . . . 9 ⊢ ((𝑥 = (𝑧 ∩ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑥 ∩ 𝑦) = ((𝑧 ∩ 𝐴) ∩ (𝑢 ∩ 𝐴)))
69		inindir 4164	. . . . . . . . 9 ⊢ ((𝑧 ∩ 𝑢) ∩ 𝐴) = ((𝑧 ∩ 𝐴) ∩ (𝑢 ∩ 𝐴))
70	68, 69	eqtr4di 2792	. . . . . . . 8 ⊢ ((𝑥 = (𝑧 ∩ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑥 ∩ 𝑦) = ((𝑧 ∩ 𝑢) ∩ 𝐴))
71	70	adantll 720	. . . . . . 7 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑥 ∩ 𝑦) = ((𝑧 ∩ 𝑢) ∩ 𝐴))
72	71	eleq1d 2824	. . . . . 6 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → ((𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴) ↔ ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴)))
73	66, 67, 72	ralxfr2d 5339	. . . . 5 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) → (∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴) ↔ ∀𝑢 ∈ 𝐿 ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴)))
74	63, 65, 73	ralxfr2d 5339	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴) ↔ ∀𝑧 ∈ 𝐿 ∀𝑢 ∈ 𝐿 ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴)))
75	60, 74	mpbird 258	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))
76		isfil2 23839	. . . . . 6 ⊢ ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ (((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))
77		restsspw 17385	. . . . . . . 8 ⊢ (𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴
78		3anass 1100	. . . . . . . 8 ⊢ (((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ↔ ((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ (¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴))))
79	77, 78	mpbiran 715	. . . . . . 7 ⊢ (((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ↔ (¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)))
80	79	3anbi1i 1163	. . . . . 6 ⊢ ((((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))
81		3anass 1100	. . . . . 6 ⊢ (((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))))
82	76, 80, 81	3bitri 298	. . . . 5 ⊢ ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))))
83		anass 469	. . . . 5 ⊢ (((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) ↔ (¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ (𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))))
84		ancom 461	. . . . 5 ⊢ ((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ (𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))) ↔ ((𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
85	82, 83, 84	3bitri 298	. . . 4 ⊢ ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ((𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
86	85	baib 540	. . 3 ⊢ ((𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
87	12, 52, 75, 86	syl12anc 842	. 2 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
88		nesym 2990	. . . 4 ⊢ ((𝑣 ∩ 𝐴) ≠ ∅ ↔ ¬ ∅ = (𝑣 ∩ 𝐴))
89	88	ralbii 3085	. . 3 ⊢ (∀𝑣 ∈ 𝐿 (𝑣 ∩ 𝐴) ≠ ∅ ↔ ∀𝑣 ∈ 𝐿 ¬ ∅ = (𝑣 ∩ 𝐴))
90		elrest 17381	. . . . . 6 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (∅ ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑣 ∈ 𝐿 ∅ = (𝑣 ∩ 𝐴)))
91	8, 90	syldan 597	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∅ ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑣 ∈ 𝐿 ∅ = (𝑣 ∩ 𝐴)))
92		dfrex2 3066	. . . . 5 ⊢ (∃𝑣 ∈ 𝐿 ∅ = (𝑣 ∩ 𝐴) ↔ ¬ ∀𝑣 ∈ 𝐿 ¬ ∅ = (𝑣 ∩ 𝐴))
93	91, 92	bitrdi 288	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∅ ∈ (𝐿 ↾t 𝐴) ↔ ¬ ∀𝑣 ∈ 𝐿 ¬ ∅ = (𝑣 ∩ 𝐴)))
94	93	con2bid 355	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∀𝑣 ∈ 𝐿 ¬ ∅ = (𝑣 ∩ 𝐴) ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
95	89, 94	bitrid 284	. 2 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∀𝑣 ∈ 𝐿 (𝑣 ∩ 𝐴) ≠ ∅ ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
96	87, 95	bitr4d 283	1 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ∀𝑣 ∈ 𝐿 (𝑣 ∩ 𝐴) ≠ ∅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119   ≠ wne 2934  ∀wral 3053  ∃wrex 3063  Vcvv 3431   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  ∅c0 4261  𝒫 cpw 4529  ‘cfv 6485  (class class class)co 7356   ↾_t crest 17374  Filcfil 23828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-rest 17376  df-fbas 21344  df-fil 23829

This theorem is referenced by:  trfil3  23871  trnei  23875