Theorem trfil2 24097

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 490	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐴 ⊆ 𝑌)
2		sseqin2 4176	. . . . 5 ⊢ (𝐴 ⊆ 𝑌 ↔ (𝑌 ∩ 𝐴) = 𝐴)
3	1, 2	sylib 221	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑌 ∩ 𝐴) = 𝐴)
4		simpl 488	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐿 ∈ (Fil‘𝑌))
5		id 23	. . . . . 6 ⊢ (𝐴 ⊆ 𝑌 → 𝐴 ⊆ 𝑌)
6		filtop 24065	. . . . . 6 ⊢ (𝐿 ∈ (Fil‘𝑌) → 𝑌 ∈ 𝐿)
7		ssexg 5292	. . . . . 6 ⊢ ((𝐴 ⊆ 𝑌 ∧ 𝑌 ∈ 𝐿) → 𝐴 ∈ V)
8	5, 6, 7	syl2anr 609	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐴 ∈ V)
9	6	adantr 486	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝑌 ∈ 𝐿)
10		elrestr 17505	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ 𝑌 ∈ 𝐿) → (𝑌 ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
11	4, 8, 9, 10	syl3anc 1398	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑌 ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
12	3, 11	eqeltrrd 2866	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐴 ∈ (𝐿 ↾t 𝐴))
13		elpwi 4571	. . . . 5 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴)
14		vex 3461	. . . . . . . . . 10 ⊢ 𝑢 ∈ V
15	14	inex1 5288	. . . . . . . . 9 ⊢ (𝑢 ∩ 𝐴) ∈ V
16	15	a1i 11	. . . . . . . 8 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑢 ∈ 𝐿) → (𝑢 ∩ 𝐴) ∈ V)
17		elrest 17504	. . . . . . . . . 10 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
18	8, 17	syldan 603	. . . . . . . . 9 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
19	18	adantr 486	. . . . . . . 8 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
20		simpr 490	. . . . . . . . 9 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → 𝑦 = (𝑢 ∩ 𝐴))
21	20	sseq1d 3969	. . . . . . . 8 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑦 ⊆ 𝑥 ↔ (𝑢 ∩ 𝐴) ⊆ 𝑥))
22	16, 19, 21	rexxfr2d 5384	. . . . . . 7 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 ↔ ∃𝑢 ∈ 𝐿 (𝑢 ∩ 𝐴) ⊆ 𝑥))
23		indir 4239	. . . . . . . . . 10 ⊢ ((𝑢 ∪ 𝑥) ∩ 𝐴) = ((𝑢 ∩ 𝐴) ∪ (𝑥 ∩ 𝐴))
24		simplr 781	. . . . . . . . . . . . 13 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑥 ⊆ 𝐴)
25		dfss2 3924	. . . . . . . . . . . . 13 ⊢ (𝑥 ⊆ 𝐴 ↔ (𝑥 ∩ 𝐴) = 𝑥)
26	24, 25	sylib 221	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑥 ∩ 𝐴) = 𝑥)
27	26	uneq2d 4122	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∩ 𝐴) ∪ (𝑥 ∩ 𝐴)) = ((𝑢 ∩ 𝐴) ∪ 𝑥))
28		simprr 785	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑢 ∩ 𝐴) ⊆ 𝑥)
29		ssequn1 4139	. . . . . . . . . . . 12 ⊢ ((𝑢 ∩ 𝐴) ⊆ 𝑥 ↔ ((𝑢 ∩ 𝐴) ∪ 𝑥) = 𝑥)
30	28, 29	sylib 221	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∩ 𝐴) ∪ 𝑥) = 𝑥)
31	27, 30	eqtrd 2800	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∩ 𝐴) ∪ (𝑥 ∩ 𝐴)) = 𝑥)
32	23, 31	eqtrid 2812	. . . . . . . . 9 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∪ 𝑥) ∩ 𝐴) = 𝑥)
33		simplll 787	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝐿 ∈ (Fil‘𝑌))
34		simpllr 788	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝐴 ⊆ 𝑌)
35	33, 34, 8	syl2anc 596	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝐴 ∈ V)
36		simprl 783	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑢 ∈ 𝐿)
37		filelss 24062	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑢 ∈ 𝐿) → 𝑢 ⊆ 𝑌)
38	33, 36, 37	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑢 ⊆ 𝑌)
39	24, 34	sstrd 3948	. . . . . . . . . . . 12 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑥 ⊆ 𝑌)
40	38, 39	unssd 4145	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑢 ∪ 𝑥) ⊆ 𝑌)
41		ssun1 4131	. . . . . . . . . . . 12 ⊢ 𝑢 ⊆ (𝑢 ∪ 𝑥)
42	41	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑢 ⊆ (𝑢 ∪ 𝑥))
43		filss 24063	. . . . . . . . . . 11 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∪ 𝑥) ⊆ 𝑌 ∧ 𝑢 ⊆ (𝑢 ∪ 𝑥))) → (𝑢 ∪ 𝑥) ∈ 𝐿)
44	33, 36, 40, 42, 43	syl13anc 1399	. . . . . . . . . 10 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → (𝑢 ∪ 𝑥) ∈ 𝐿)
45		elrestr 17505	. . . . . . . . . 10 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑢 ∪ 𝑥) ∈ 𝐿) → ((𝑢 ∪ 𝑥) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
46	33, 35, 44, 45	syl3anc 1398	. . . . . . . . 9 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → ((𝑢 ∪ 𝑥) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
47	32, 46	eqeltrrd 2866	. . . . . . . 8 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) ∧ (𝑢 ∈ 𝐿 ∧ (𝑢 ∩ 𝐴) ⊆ 𝑥)) → 𝑥 ∈ (𝐿 ↾t 𝐴))
48	47	rexlimdvaa 3169	. . . . . . 7 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (∃𝑢 ∈ 𝐿 (𝑢 ∩ 𝐴) ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)))
49	22, 48	sylbid 243	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)))
50	49	ex 418	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑥 ⊆ 𝐴 → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴))))
51	13, 50	syl5 35	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑥 ∈ 𝒫 𝐴 → (∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴))))
52	51	ralrimiv 3158	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)))
53		simpll 779	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → 𝐿 ∈ (Fil‘𝑌))
54	8	adantr 486	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → 𝐴 ∈ V)
55		filin 24064	. . . . . . . 8 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿) → (𝑧 ∩ 𝑢) ∈ 𝐿)
56	55	3expb 1138	. . . . . . 7 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → (𝑧 ∩ 𝑢) ∈ 𝐿)
57	56	adantlr 728	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → (𝑧 ∩ 𝑢) ∈ 𝐿)
58		elrestr 17505	. . . . . 6 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V ∧ (𝑧 ∩ 𝑢) ∈ 𝐿) → ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
59	53, 54, 57, 58	syl3anc 1398	. . . . 5 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ (𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿)) → ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
60	59	ralrimivva 3210	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ∀𝑧 ∈ 𝐿 ∀𝑢 ∈ 𝐿 ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴))
61		vex 3461	. . . . . . 7 ⊢ 𝑧 ∈ V
62	61	inex1 5288	. . . . . 6 ⊢ (𝑧 ∩ 𝐴) ∈ V
63	62	a1i 11	. . . . 5 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑧 ∈ 𝐿) → (𝑧 ∩ 𝐴) ∈ V)
64		elrest 17504	. . . . . 6 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (𝑥 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑧 ∈ 𝐿 𝑥 = (𝑧 ∩ 𝐴)))
65	8, 64	syldan 603	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (𝑥 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑧 ∈ 𝐿 𝑥 = (𝑧 ∩ 𝐴)))
66	15	a1i 11	. . . . . 6 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) ∧ 𝑢 ∈ 𝐿) → (𝑢 ∩ 𝐴) ∈ V)
67	18	adantr 486	. . . . . 6 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) → (𝑦 ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑢 ∈ 𝐿 𝑦 = (𝑢 ∩ 𝐴)))
68		ineq12 4168	. . . . . . . . 9 ⊢ ((𝑥 = (𝑧 ∩ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑥 ∩ 𝑦) = ((𝑧 ∩ 𝐴) ∩ (𝑢 ∩ 𝐴)))
69		inindir 4188	. . . . . . . . 9 ⊢ ((𝑧 ∩ 𝑢) ∩ 𝐴) = ((𝑧 ∩ 𝐴) ∩ (𝑢 ∩ 𝐴))
70	68, 69	eqtr4di 2818	. . . . . . . 8 ⊢ ((𝑥 = (𝑧 ∩ 𝐴) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑥 ∩ 𝑦) = ((𝑧 ∩ 𝑢) ∩ 𝐴))
71	70	adantll 727	. . . . . . 7 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → (𝑥 ∩ 𝑦) = ((𝑧 ∩ 𝑢) ∩ 𝐴))
72	71	eleq1d 2850	. . . . . 6 ⊢ ((((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) ∧ 𝑦 = (𝑢 ∩ 𝐴)) → ((𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴) ↔ ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴)))
73	66, 67, 72	ralxfr2d 5383	. . . . 5 ⊢ (((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) ∧ 𝑥 = (𝑧 ∩ 𝐴)) → (∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴) ↔ ∀𝑢 ∈ 𝐿 ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴)))
74	63, 65, 73	ralxfr2d 5383	. . . 4 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴) ↔ ∀𝑧 ∈ 𝐿 ∀𝑢 ∈ 𝐿 ((𝑧 ∩ 𝑢) ∩ 𝐴) ∈ (𝐿 ↾t 𝐴)))
75	60, 74	mpbird 260	. . 3 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))
76		isfil2 24066	. . . . . 6 ⊢ ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ (((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))
77		restsspw 17508	. . . . . . . 8 ⊢ (𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴
78		3anass 1111	. . . . . . . 8 ⊢ (((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ↔ ((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ (¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴))))
79	77, 78	mpbiran 722	. . . . . . 7 ⊢ (((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ↔ (¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)))
80	79	3anbi1i 1175	. . . . . 6 ⊢ ((((𝐿 ↾t 𝐴) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)) ↔ ((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))
81		3anass 1111	. . . . . 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 474	. . . . 5 ⊢ (((¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ 𝐴 ∈ (𝐿 ↾t 𝐴)) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) ↔ (¬ ∅ ∈ (𝐿 ↾t 𝐴) ∧ (𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴)))))
84		ancom 466	. . . . 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 545	. . 3 ⊢ ((𝐴 ∈ (𝐿 ↾t 𝐴) ∧ (∀𝑥 ∈ 𝒫 𝐴(∃𝑦 ∈ (𝐿 ↾t 𝐴)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝐿 ↾t 𝐴)) ∧ ∀𝑥 ∈ (𝐿 ↾t 𝐴)∀𝑦 ∈ (𝐿 ↾t 𝐴)(𝑥 ∩ 𝑦) ∈ (𝐿 ↾t 𝐴))) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
87	12, 52, 75, 86	syl12anc 850	. 2 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ ∅ ∈ (𝐿 ↾t 𝐴)))
88		nesym 3016	. . . 4 ⊢ ((𝑣 ∩ 𝐴) ≠ ∅ ↔ ¬ ∅ = (𝑣 ∩ 𝐴))
89	88	ralbii 3113	. . 3 ⊢ (∀𝑣 ∈ 𝐿 (𝑣 ∩ 𝐴) ≠ ∅ ↔ ∀𝑣 ∈ 𝐿 ¬ ∅ = (𝑣 ∩ 𝐴))
90		elrest 17504	. . . . . 6 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ∈ V) → (∅ ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑣 ∈ 𝐿 ∅ = (𝑣 ∩ 𝐴)))
91	8, 90	syldan 603	. . . . 5 ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → (∅ ∈ (𝐿 ↾t 𝐴) ↔ ∃𝑣 ∈ 𝐿 ∅ = (𝑣 ∩ 𝐴)))
92		dfrex2 3094	. . . . 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‘𝐴) ↔ ∀𝑣 ∈ 𝐿 (𝑣 ∩ 𝐴) ≠ ∅))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  ∀wral 3081  ∃wrex 3091  Vcvv 3457   ∪ cun 3904   ∩ cin 3905   ⊆ wss 3906  ∅c0 4286  𝒫 cpw 4564  ‘cfv 6540  (class class class)co 7419   ↾_t crest 17497  Filcfil 24055

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7422  df-oprab 7423  df-mpo 7424  df-1st 7992  df-2nd 7993  df-rest 17499  df-fbas 21571  df-fil 24056

This theorem is used by:  trfil3  24098  trnei  24102