Metamath Proof Explorer

Theorem trfil2

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

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

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ⊆ 𝑌 )
2 sseqin2 ⊢ ( 𝐴 ⊆ 𝑌 ↔ ( 𝑌 ∩ 𝐴 ) = 𝐴 )
3 1 2 sylib ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝑌 ∩ 𝐴 ) = 𝐴 )
4 simpl ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
5 id ⊢ ( 𝐴 ⊆ 𝑌 → 𝐴 ⊆ 𝑌 )
6 filtop ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → 𝑌 ∈ 𝐿 )
7 ssexg ⊢ ( ( 𝐴 ⊆ 𝑌 ∧ 𝑌 ∈ 𝐿 ) → 𝐴 ∈ V )
8 5 6 7 syl2anr ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ∈ V )
9 6 adantr ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝑌 ∈ 𝐿 )
10 elrestr ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ∈ V ∧ 𝑌 ∈ 𝐿 ) → ( 𝑌 ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) )
11 4 8 9 10 syl3anc ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝑌 ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) )
12 3 11 eqeltrrd ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) )
13 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
14 vex ⊢ 𝑢 ∈ V
15 14 inex1 ⊢ ( 𝑢 ∩ 𝐴 ) ∈ V
16 15 a1i ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑢 ∈ 𝐿 ) → ( 𝑢 ∩ 𝐴 ) ∈ V )
17 elrest ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ∈ V ) → ( 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ↔ ∃ 𝑢 ∈ 𝐿 𝑦 = ( 𝑢 ∩ 𝐴 ) ) )
18 8 17 syldan ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ↔ ∃ 𝑢 ∈ 𝐿 𝑦 = ( 𝑢 ∩ 𝐴 ) ) )
19 18 adantr ⊢ ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ↔ ∃ 𝑢 ∈ 𝐿 𝑦 = ( 𝑢 ∩ 𝐴 ) ) )
20 simpr ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑦 = ( 𝑢 ∩ 𝐴 ) ) → 𝑦 = ( 𝑢 ∩ 𝐴 ) )
21 20 sseq1d ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ 𝑦 = ( 𝑢 ∩ 𝐴 ) ) → ( 𝑦 ⊆ 𝑥 ↔ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) )
22 16 19 21 rexxfr2d ⊢ ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) → ( ∃ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 ↔ ∃ 𝑢 ∈ 𝐿 ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) )
23 indir ⊢ ( ( 𝑢 ∪ 𝑥 ) ∩ 𝐴 ) = ( ( 𝑢 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐴 ) )
24 simplr ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → 𝑥 ⊆ 𝐴 )
25 df-ss ⊢ ( 𝑥 ⊆ 𝐴 ↔ ( 𝑥 ∩ 𝐴 ) = 𝑥 )
26 24 25 sylib ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → ( 𝑥 ∩ 𝐴 ) = 𝑥 )
27 26 uneq2d ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → ( ( 𝑢 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐴 ) ) = ( ( 𝑢 ∩ 𝐴 ) ∪ 𝑥 ) )
28 simprr ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 )
29 ssequn1 ⊢ ( ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ↔ ( ( 𝑢 ∩ 𝐴 ) ∪ 𝑥 ) = 𝑥 )
30 28 29 sylib ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → ( ( 𝑢 ∩ 𝐴 ) ∪ 𝑥 ) = 𝑥 )
31 27 30 eqtrd ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → ( ( 𝑢 ∩ 𝐴 ) ∪ ( 𝑥 ∩ 𝐴 ) ) = 𝑥 )
32 23 31 syl5eq ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → ( ( 𝑢 ∪ 𝑥 ) ∩ 𝐴 ) = 𝑥 )
33 simplll ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
34 simpllr ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → 𝐴 ⊆ 𝑌 )
35 33 34 8 syl2anc ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → 𝐴 ∈ V )
36 simprl ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → 𝑢 ∈ 𝐿 )
37 filelss ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝑢 ∈ 𝐿 ) → 𝑢 ⊆ 𝑌 )
38 33 36 37 syl2anc ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → 𝑢 ⊆ 𝑌 )
39 24 34 sstrd ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → 𝑥 ⊆ 𝑌 )
40 38 39 unssd ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → ( 𝑢 ∪ 𝑥 ) ⊆ 𝑌 )
41 ssun1 ⊢ 𝑢 ⊆ ( 𝑢 ∪ 𝑥 )
42 41 a1i ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → 𝑢 ⊆ ( 𝑢 ∪ 𝑥 ) )
43 filss ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∪ 𝑥 ) ⊆ 𝑌 ∧ 𝑢 ⊆ ( 𝑢 ∪ 𝑥 ) ) ) → ( 𝑢 ∪ 𝑥 ) ∈ 𝐿 )
44 33 36 40 42 43 syl13anc ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → ( 𝑢 ∪ 𝑥 ) ∈ 𝐿 )
45 elrestr ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ∈ V ∧ ( 𝑢 ∪ 𝑥 ) ∈ 𝐿 ) → ( ( 𝑢 ∪ 𝑥 ) ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) )
46 33 35 44 45 syl3anc ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → ( ( 𝑢 ∪ 𝑥 ) ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) )
47 32 46 eqeltrrd ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) ∧ ( 𝑢 ∈ 𝐿 ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 ) ) → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) )
48 47 rexlimdvaa ⊢ ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) → ( ∃ 𝑢 ∈ 𝐿 ( 𝑢 ∩ 𝐴 ) ⊆ 𝑥 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) )
49 22 48 sylbid ⊢ ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 ⊆ 𝐴 ) → ( ∃ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) )
50 49 ex ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝑥 ⊆ 𝐴 → ( ∃ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) ) )
51 13 50 syl5 ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝑥 ∈ 𝒫 𝐴 → ( ∃ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) ) )
52 51 ralrimiv ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ∀ 𝑥 ∈ 𝒫 𝐴 ( ∃ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) )
53 simpll ⊢ ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿 ) ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
54 8 adantr ⊢ ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿 ) ) → 𝐴 ∈ V )
55 filin ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿 ) → ( 𝑧 ∩ 𝑢 ) ∈ 𝐿 )
56 55 3expb ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ ( 𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿 ) ) → ( 𝑧 ∩ 𝑢 ) ∈ 𝐿 )
57 56 adantlr ⊢ ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿 ) ) → ( 𝑧 ∩ 𝑢 ) ∈ 𝐿 )
58 elrestr ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ∈ V ∧ ( 𝑧 ∩ 𝑢 ) ∈ 𝐿 ) → ( ( 𝑧 ∩ 𝑢 ) ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) )
59 53 54 57 58 syl3anc ⊢ ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ ( 𝑧 ∈ 𝐿 ∧ 𝑢 ∈ 𝐿 ) ) → ( ( 𝑧 ∩ 𝑢 ) ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) )
60 59 ralrimivva ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ∀ 𝑧 ∈ 𝐿 ∀ 𝑢 ∈ 𝐿 ( ( 𝑧 ∩ 𝑢 ) ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) )
61 vex ⊢ 𝑧 ∈ V
62 61 inex1 ⊢ ( 𝑧 ∩ 𝐴 ) ∈ V
63 62 a1i ⊢ ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑧 ∈ 𝐿 ) → ( 𝑧 ∩ 𝐴 ) ∈ V )
64 elrest ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ∈ V ) → ( 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ↔ ∃ 𝑧 ∈ 𝐿 𝑥 = ( 𝑧 ∩ 𝐴 ) ) )
65 8 64 syldan ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ↔ ∃ 𝑧 ∈ 𝐿 𝑥 = ( 𝑧 ∩ 𝐴 ) ) )
66 15 a1i ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 = ( 𝑧 ∩ 𝐴 ) ) ∧ 𝑢 ∈ 𝐿 ) → ( 𝑢 ∩ 𝐴 ) ∈ V )
67 18 adantr ⊢ ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 = ( 𝑧 ∩ 𝐴 ) ) → ( 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ↔ ∃ 𝑢 ∈ 𝐿 𝑦 = ( 𝑢 ∩ 𝐴 ) ) )
68 ineq12 ⊢ ( ( 𝑥 = ( 𝑧 ∩ 𝐴 ) ∧ 𝑦 = ( 𝑢 ∩ 𝐴 ) ) → ( 𝑥 ∩ 𝑦 ) = ( ( 𝑧 ∩ 𝐴 ) ∩ ( 𝑢 ∩ 𝐴 ) ) )
69 inindir ⊢ ( ( 𝑧 ∩ 𝑢 ) ∩ 𝐴 ) = ( ( 𝑧 ∩ 𝐴 ) ∩ ( 𝑢 ∩ 𝐴 ) )
70 68 69 eqtr4di ⊢ ( ( 𝑥 = ( 𝑧 ∩ 𝐴 ) ∧ 𝑦 = ( 𝑢 ∩ 𝐴 ) ) → ( 𝑥 ∩ 𝑦 ) = ( ( 𝑧 ∩ 𝑢 ) ∩ 𝐴 ) )
71 70 adantll ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 = ( 𝑧 ∩ 𝐴 ) ) ∧ 𝑦 = ( 𝑢 ∩ 𝐴 ) ) → ( 𝑥 ∩ 𝑦 ) = ( ( 𝑧 ∩ 𝑢 ) ∩ 𝐴 ) )
72 71 eleq1d ⊢ ( ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 = ( 𝑧 ∩ 𝐴 ) ) ∧ 𝑦 = ( 𝑢 ∩ 𝐴 ) ) → ( ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐿 ↾t 𝐴 ) ↔ ( ( 𝑧 ∩ 𝑢 ) ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) ) )
73 66 67 72 ralxfr2d ⊢ ( ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) ∧ 𝑥 = ( 𝑧 ∩ 𝐴 ) ) → ( ∀ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐿 ↾t 𝐴 ) ↔ ∀ 𝑢 ∈ 𝐿 ( ( 𝑧 ∩ 𝑢 ) ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) ) )
74 63 65 73 ralxfr2d ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ∀ 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐿 ↾t 𝐴 ) ↔ ∀ 𝑧 ∈ 𝐿 ∀ 𝑢 ∈ 𝐿 ( ( 𝑧 ∩ 𝑢 ) ∩ 𝐴 ) ∈ ( 𝐿 ↾t 𝐴 ) ) )
75 60 74 mpbird ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ∀ 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐿 ↾t 𝐴 ) )
76 isfil2 ⊢ ( ( 𝐿 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ↔ ( ( ( 𝐿 ↾t 𝐴 ) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ∧ 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( ∃ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ∀ 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐿 ↾t 𝐴 ) ) )
77 restsspw ⊢ ( 𝐿 ↾t 𝐴 ) ⊆ 𝒫 𝐴
78 3anass ⊢ ( ( ( 𝐿 ↾t 𝐴 ) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ∧ 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) ) ↔ ( ( 𝐿 ↾t 𝐴 ) ⊆ 𝒫 𝐴 ∧ ( ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ∧ 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) ) ) )
79 77 78 mpbiran ⊢ ( ( ( 𝐿 ↾t 𝐴 ) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ∧ 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) ) ↔ ( ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ∧ 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) ) )
80 79 3anbi1i ⊢ ( ( ( ( 𝐿 ↾t 𝐴 ) ⊆ 𝒫 𝐴 ∧ ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ∧ 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( ∃ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ∀ 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐿 ↾t 𝐴 ) ) ↔ ( ( ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ∧ 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( ∃ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ∀ 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐿 ↾t 𝐴 ) ) )
81 3anass ⊢ ( ( ( ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ∧ 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ∀ 𝑥 ∈ 𝒫 𝐴 ( ∃ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ∀ 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐿 ↾t 𝐴 ) ) ↔ ( ( ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ∧ 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝒫 𝐴 ( ∃ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ∀ 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐿 ↾t 𝐴 ) ) ) )
82 76 80 81 3bitri ⊢ ( ( 𝐿 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ↔ ( ( ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ∧ 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝒫 𝐴 ( ∃ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ∀ 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐿 ↾t 𝐴 ) ) ) )
83 anass ⊢ ( ( ( ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ∧ 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ( ∀ 𝑥 ∈ 𝒫 𝐴 ( ∃ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ∀ 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐿 ↾t 𝐴 ) ) ) ↔ ( ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ∧ ( 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) ∧ ( ∀ 𝑥 ∈ 𝒫 𝐴 ( ∃ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ∀ 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐿 ↾t 𝐴 ) ) ) ) )
84 ancom ⊢ ( ( ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ∧ ( 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) ∧ ( ∀ 𝑥 ∈ 𝒫 𝐴 ( ∃ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ∀ 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐿 ↾t 𝐴 ) ) ) ) ↔ ( ( 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) ∧ ( ∀ 𝑥 ∈ 𝒫 𝐴 ( ∃ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ∀ 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐿 ↾t 𝐴 ) ) ) ∧ ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ) )
85 82 83 84 3bitri ⊢ ( ( 𝐿 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ↔ ( ( 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) ∧ ( ∀ 𝑥 ∈ 𝒫 𝐴 ( ∃ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ∀ 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐿 ↾t 𝐴 ) ) ) ∧ ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ) )
86 85 baib ⊢ ( ( 𝐴 ∈ ( 𝐿 ↾t 𝐴 ) ∧ ( ∀ 𝑥 ∈ 𝒫 𝐴 ( ∃ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) 𝑦 ⊆ 𝑥 → 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ) ∧ ∀ 𝑥 ∈ ( 𝐿 ↾t 𝐴 ) ∀ 𝑦 ∈ ( 𝐿 ↾t 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐿 ↾t 𝐴 ) ) ) → ( ( 𝐿 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ↔ ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ) )
87 12 52 75 86 syl12anc ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐿 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ↔ ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ) )
88 nesym ⊢ ( ( 𝑣 ∩ 𝐴 ) ≠ ∅ ↔ ¬ ∅ = ( 𝑣 ∩ 𝐴 ) )
89 88 ralbii ⊢ ( ∀ 𝑣 ∈ 𝐿 ( 𝑣 ∩ 𝐴 ) ≠ ∅ ↔ ∀ 𝑣 ∈ 𝐿 ¬ ∅ = ( 𝑣 ∩ 𝐴 ) )
90 elrest ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ∈ V ) → ( ∅ ∈ ( 𝐿 ↾t 𝐴 ) ↔ ∃ 𝑣 ∈ 𝐿 ∅ = ( 𝑣 ∩ 𝐴 ) ) )
91 8 90 syldan ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ∅ ∈ ( 𝐿 ↾t 𝐴 ) ↔ ∃ 𝑣 ∈ 𝐿 ∅ = ( 𝑣 ∩ 𝐴 ) ) )
92 dfrex2 ⊢ ( ∃ 𝑣 ∈ 𝐿 ∅ = ( 𝑣 ∩ 𝐴 ) ↔ ¬ ∀ 𝑣 ∈ 𝐿 ¬ ∅ = ( 𝑣 ∩ 𝐴 ) )
93 91 92 syl6bb ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ∅ ∈ ( 𝐿 ↾t 𝐴 ) ↔ ¬ ∀ 𝑣 ∈ 𝐿 ¬ ∅ = ( 𝑣 ∩ 𝐴 ) ) )
94 93 con2bid ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ∀ 𝑣 ∈ 𝐿 ¬ ∅ = ( 𝑣 ∩ 𝐴 ) ↔ ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ) )
95 89 94 syl5bb ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ∀ 𝑣 ∈ 𝐿 ( 𝑣 ∩ 𝐴 ) ≠ ∅ ↔ ¬ ∅ ∈ ( 𝐿 ↾t 𝐴 ) ) )
96 87 95 bitr4d ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴 ⊆ 𝑌 ) → ( ( 𝐿 ↾t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ↔ ∀ 𝑣 ∈ 𝐿 ( 𝑣 ∩ 𝐴 ) ≠ ∅ ) )