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 bitrdi ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴𝑌 ) → ( ∅ ∈ ( 𝐿t 𝐴 ) ↔ ¬ ∀ 𝑣𝐿 ¬ ∅ = ( 𝑣𝐴 ) ) )
94 93 con2bid ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴𝑌 ) → ( ∀ 𝑣𝐿 ¬ ∅ = ( 𝑣𝐴 ) ↔ ¬ ∅ ∈ ( 𝐿t 𝐴 ) ) )
95 89 94 syl5bb ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴𝑌 ) → ( ∀ 𝑣𝐿 ( 𝑣𝐴 ) ≠ ∅ ↔ ¬ ∅ ∈ ( 𝐿t 𝐴 ) ) )
96 87 95 bitr4d ( ( 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐴𝑌 ) → ( ( 𝐿t 𝐴 ) ∈ ( Fil ‘ 𝐴 ) ↔ ∀ 𝑣𝐿 ( 𝑣𝐴 ) ≠ ∅ ) )