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 
|- ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( ( L |`t A ) e. ( Fil ` A ) <-> A. v e. L ( v i^i A ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> A C_ Y )
2 sseqin2 
 |-  ( A C_ Y <-> ( Y i^i A ) = A )
3 1 2 sylib 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( Y i^i A ) = A )
4 simpl 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> L e. ( Fil ` Y ) )
5 id 
 |-  ( A C_ Y -> A C_ Y )
6 filtop 
 |-  ( L e. ( Fil ` Y ) -> Y e. L )
7 ssexg 
 |-  ( ( A C_ Y /\ Y e. L ) -> A e. _V )
8 5 6 7 syl2anr 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> A e. _V )
9 6 adantr 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> Y e. L )
10 elrestr 
 |-  ( ( L e. ( Fil ` Y ) /\ A e. _V /\ Y e. L ) -> ( Y i^i A ) e. ( L |`t A ) )
11 4 8 9 10 syl3anc 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( Y i^i A ) e. ( L |`t A ) )
12 3 11 eqeltrrd 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> A e. ( L |`t A ) )
13 elpwi 
 |-  ( x e. ~P A -> x C_ A )
14 vex 
 |-  u e. _V
15 14 inex1 
 |-  ( u i^i A ) e. _V
16 15 a1i 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ u e. L ) -> ( u i^i A ) e. _V )
17 elrest 
 |-  ( ( L e. ( Fil ` Y ) /\ A e. _V ) -> ( y e. ( L |`t A ) <-> E. u e. L y = ( u i^i A ) ) )
18 8 17 syldan 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( y e. ( L |`t A ) <-> E. u e. L y = ( u i^i A ) ) )
19 18 adantr 
 |-  ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( y e. ( L |`t A ) <-> E. u e. L y = ( u i^i A ) ) )
20 simpr 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ y = ( u i^i A ) ) -> y = ( u i^i A ) )
21 20 sseq1d 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ y = ( u i^i A ) ) -> ( y C_ x <-> ( u i^i A ) C_ x ) )
22 16 19 21 rexxfr2d 
 |-  ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( E. y e. ( L |`t A ) y C_ x <-> E. u e. L ( u i^i A ) C_ x ) )
23 indir 
 |-  ( ( u u. x ) i^i A ) = ( ( u i^i A ) u. ( x i^i A ) )
24 simplr 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> x C_ A )
25 df-ss 
 |-  ( x C_ A <-> ( x i^i A ) = x )
26 24 25 sylib 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> ( x i^i A ) = x )
27 26 uneq2d 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> ( ( u i^i A ) u. ( x i^i A ) ) = ( ( u i^i A ) u. x ) )
28 simprr 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> ( u i^i A ) C_ x )
29 ssequn1 
 |-  ( ( u i^i A ) C_ x <-> ( ( u i^i A ) u. x ) = x )
30 28 29 sylib 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> ( ( u i^i A ) u. x ) = x )
31 27 30 eqtrd 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> ( ( u i^i A ) u. ( x i^i A ) ) = x )
32 23 31 syl5eq 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> ( ( u u. x ) i^i A ) = x )
33 simplll 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> L e. ( Fil ` Y ) )
34 simpllr 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> A C_ Y )
35 33 34 8 syl2anc 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> A e. _V )
36 simprl 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> u e. L )
37 filelss 
 |-  ( ( L e. ( Fil ` Y ) /\ u e. L ) -> u C_ Y )
38 33 36 37 syl2anc 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> u C_ Y )
39 24 34 sstrd 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> x C_ Y )
40 38 39 unssd 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> ( u u. x ) C_ Y )
41 ssun1 
 |-  u C_ ( u u. x )
42 41 a1i 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> u C_ ( u u. x ) )
43 filss 
 |-  ( ( L e. ( Fil ` Y ) /\ ( u e. L /\ ( u u. x ) C_ Y /\ u C_ ( u u. x ) ) ) -> ( u u. x ) e. L )
44 33 36 40 42 43 syl13anc 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> ( u u. x ) e. L )
45 elrestr 
 |-  ( ( L e. ( Fil ` Y ) /\ A e. _V /\ ( u u. x ) e. L ) -> ( ( u u. x ) i^i A ) e. ( L |`t A ) )
46 33 35 44 45 syl3anc 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> ( ( u u. x ) i^i A ) e. ( L |`t A ) )
47 32 46 eqeltrrd 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) /\ ( u e. L /\ ( u i^i A ) C_ x ) ) -> x e. ( L |`t A ) )
48 47 rexlimdvaa 
 |-  ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( E. u e. L ( u i^i A ) C_ x -> x e. ( L |`t A ) ) )
49 22 48 sylbid 
 |-  ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x C_ A ) -> ( E. y e. ( L |`t A ) y C_ x -> x e. ( L |`t A ) ) )
50 49 ex 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( x C_ A -> ( E. y e. ( L |`t A ) y C_ x -> x e. ( L |`t A ) ) ) )
51 13 50 syl5 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( x e. ~P A -> ( E. y e. ( L |`t A ) y C_ x -> x e. ( L |`t A ) ) ) )
52 51 ralrimiv 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> A. x e. ~P A ( E. y e. ( L |`t A ) y C_ x -> x e. ( L |`t A ) ) )
53 simpll 
 |-  ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ ( z e. L /\ u e. L ) ) -> L e. ( Fil ` Y ) )
54 8 adantr 
 |-  ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ ( z e. L /\ u e. L ) ) -> A e. _V )
55 filin 
 |-  ( ( L e. ( Fil ` Y ) /\ z e. L /\ u e. L ) -> ( z i^i u ) e. L )
56 55 3expb 
 |-  ( ( L e. ( Fil ` Y ) /\ ( z e. L /\ u e. L ) ) -> ( z i^i u ) e. L )
57 56 adantlr 
 |-  ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ ( z e. L /\ u e. L ) ) -> ( z i^i u ) e. L )
58 elrestr 
 |-  ( ( L e. ( Fil ` Y ) /\ A e. _V /\ ( z i^i u ) e. L ) -> ( ( z i^i u ) i^i A ) e. ( L |`t A ) )
59 53 54 57 58 syl3anc 
 |-  ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ ( z e. L /\ u e. L ) ) -> ( ( z i^i u ) i^i A ) e. ( L |`t A ) )
60 59 ralrimivva 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> A. z e. L A. u e. L ( ( z i^i u ) i^i A ) e. ( L |`t A ) )
61 vex 
 |-  z e. _V
62 61 inex1 
 |-  ( z i^i A ) e. _V
63 62 a1i 
 |-  ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ z e. L ) -> ( z i^i A ) e. _V )
64 elrest 
 |-  ( ( L e. ( Fil ` Y ) /\ A e. _V ) -> ( x e. ( L |`t A ) <-> E. z e. L x = ( z i^i A ) ) )
65 8 64 syldan 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( x e. ( L |`t A ) <-> E. z e. L x = ( z i^i A ) ) )
66 15 a1i 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x = ( z i^i A ) ) /\ u e. L ) -> ( u i^i A ) e. _V )
67 18 adantr 
 |-  ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x = ( z i^i A ) ) -> ( y e. ( L |`t A ) <-> E. u e. L y = ( u i^i A ) ) )
68 ineq12 
 |-  ( ( x = ( z i^i A ) /\ y = ( u i^i A ) ) -> ( x i^i y ) = ( ( z i^i A ) i^i ( u i^i A ) ) )
69 inindir 
 |-  ( ( z i^i u ) i^i A ) = ( ( z i^i A ) i^i ( u i^i A ) )
70 68 69 eqtr4di 
 |-  ( ( x = ( z i^i A ) /\ y = ( u i^i A ) ) -> ( x i^i y ) = ( ( z i^i u ) i^i A ) )
71 70 adantll 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x = ( z i^i A ) ) /\ y = ( u i^i A ) ) -> ( x i^i y ) = ( ( z i^i u ) i^i A ) )
72 71 eleq1d 
 |-  ( ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x = ( z i^i A ) ) /\ y = ( u i^i A ) ) -> ( ( x i^i y ) e. ( L |`t A ) <-> ( ( z i^i u ) i^i A ) e. ( L |`t A ) ) )
73 66 67 72 ralxfr2d 
 |-  ( ( ( L e. ( Fil ` Y ) /\ A C_ Y ) /\ x = ( z i^i A ) ) -> ( A. y e. ( L |`t A ) ( x i^i y ) e. ( L |`t A ) <-> A. u e. L ( ( z i^i u ) i^i A ) e. ( L |`t A ) ) )
74 63 65 73 ralxfr2d 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( A. x e. ( L |`t A ) A. y e. ( L |`t A ) ( x i^i y ) e. ( L |`t A ) <-> A. z e. L A. u e. L ( ( z i^i u ) i^i A ) e. ( L |`t A ) ) )
75 60 74 mpbird 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> A. x e. ( L |`t A ) A. y e. ( L |`t A ) ( x i^i y ) e. ( L |`t A ) )
76 isfil2 
 |-  ( ( L |`t A ) e. ( Fil ` A ) <-> ( ( ( L |`t A ) C_ ~P A /\ -. (/) e. ( L |`t A ) /\ A e. ( L |`t A ) ) /\ A. x e. ~P A ( E. y e. ( L |`t A ) y C_ x -> x e. ( L |`t A ) ) /\ A. x e. ( L |`t A ) A. y e. ( L |`t A ) ( x i^i y ) e. ( L |`t A ) ) )
77 restsspw 
 |-  ( L |`t A ) C_ ~P A
78 3anass 
 |-  ( ( ( L |`t A ) C_ ~P A /\ -. (/) e. ( L |`t A ) /\ A e. ( L |`t A ) ) <-> ( ( L |`t A ) C_ ~P A /\ ( -. (/) e. ( L |`t A ) /\ A e. ( L |`t A ) ) ) )
79 77 78 mpbiran 
 |-  ( ( ( L |`t A ) C_ ~P A /\ -. (/) e. ( L |`t A ) /\ A e. ( L |`t A ) ) <-> ( -. (/) e. ( L |`t A ) /\ A e. ( L |`t A ) ) )
80 79 3anbi1i 
 |-  ( ( ( ( L |`t A ) C_ ~P A /\ -. (/) e. ( L |`t A ) /\ A e. ( L |`t A ) ) /\ A. x e. ~P A ( E. y e. ( L |`t A ) y C_ x -> x e. ( L |`t A ) ) /\ A. x e. ( L |`t A ) A. y e. ( L |`t A ) ( x i^i y ) e. ( L |`t A ) ) <-> ( ( -. (/) e. ( L |`t A ) /\ A e. ( L |`t A ) ) /\ A. x e. ~P A ( E. y e. ( L |`t A ) y C_ x -> x e. ( L |`t A ) ) /\ A. x e. ( L |`t A ) A. y e. ( L |`t A ) ( x i^i y ) e. ( L |`t A ) ) )
81 3anass 
 |-  ( ( ( -. (/) e. ( L |`t A ) /\ A e. ( L |`t A ) ) /\ A. x e. ~P A ( E. y e. ( L |`t A ) y C_ x -> x e. ( L |`t A ) ) /\ A. x e. ( L |`t A ) A. y e. ( L |`t A ) ( x i^i y ) e. ( L |`t A ) ) <-> ( ( -. (/) e. ( L |`t A ) /\ A e. ( L |`t A ) ) /\ ( A. x e. ~P A ( E. y e. ( L |`t A ) y C_ x -> x e. ( L |`t A ) ) /\ A. x e. ( L |`t A ) A. y e. ( L |`t A ) ( x i^i y ) e. ( L |`t A ) ) ) )
82 76 80 81 3bitri 
 |-  ( ( L |`t A ) e. ( Fil ` A ) <-> ( ( -. (/) e. ( L |`t A ) /\ A e. ( L |`t A ) ) /\ ( A. x e. ~P A ( E. y e. ( L |`t A ) y C_ x -> x e. ( L |`t A ) ) /\ A. x e. ( L |`t A ) A. y e. ( L |`t A ) ( x i^i y ) e. ( L |`t A ) ) ) )
83 anass 
 |-  ( ( ( -. (/) e. ( L |`t A ) /\ A e. ( L |`t A ) ) /\ ( A. x e. ~P A ( E. y e. ( L |`t A ) y C_ x -> x e. ( L |`t A ) ) /\ A. x e. ( L |`t A ) A. y e. ( L |`t A ) ( x i^i y ) e. ( L |`t A ) ) ) <-> ( -. (/) e. ( L |`t A ) /\ ( A e. ( L |`t A ) /\ ( A. x e. ~P A ( E. y e. ( L |`t A ) y C_ x -> x e. ( L |`t A ) ) /\ A. x e. ( L |`t A ) A. y e. ( L |`t A ) ( x i^i y ) e. ( L |`t A ) ) ) ) )
84 ancom 
 |-  ( ( -. (/) e. ( L |`t A ) /\ ( A e. ( L |`t A ) /\ ( A. x e. ~P A ( E. y e. ( L |`t A ) y C_ x -> x e. ( L |`t A ) ) /\ A. x e. ( L |`t A ) A. y e. ( L |`t A ) ( x i^i y ) e. ( L |`t A ) ) ) ) <-> ( ( A e. ( L |`t A ) /\ ( A. x e. ~P A ( E. y e. ( L |`t A ) y C_ x -> x e. ( L |`t A ) ) /\ A. x e. ( L |`t A ) A. y e. ( L |`t A ) ( x i^i y ) e. ( L |`t A ) ) ) /\ -. (/) e. ( L |`t A ) ) )
85 82 83 84 3bitri 
 |-  ( ( L |`t A ) e. ( Fil ` A ) <-> ( ( A e. ( L |`t A ) /\ ( A. x e. ~P A ( E. y e. ( L |`t A ) y C_ x -> x e. ( L |`t A ) ) /\ A. x e. ( L |`t A ) A. y e. ( L |`t A ) ( x i^i y ) e. ( L |`t A ) ) ) /\ -. (/) e. ( L |`t A ) ) )
86 85 baib 
 |-  ( ( A e. ( L |`t A ) /\ ( A. x e. ~P A ( E. y e. ( L |`t A ) y C_ x -> x e. ( L |`t A ) ) /\ A. x e. ( L |`t A ) A. y e. ( L |`t A ) ( x i^i y ) e. ( L |`t A ) ) ) -> ( ( L |`t A ) e. ( Fil ` A ) <-> -. (/) e. ( L |`t A ) ) )
87 12 52 75 86 syl12anc 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( ( L |`t A ) e. ( Fil ` A ) <-> -. (/) e. ( L |`t A ) ) )
88 nesym 
 |-  ( ( v i^i A ) =/= (/) <-> -. (/) = ( v i^i A ) )
89 88 ralbii 
 |-  ( A. v e. L ( v i^i A ) =/= (/) <-> A. v e. L -. (/) = ( v i^i A ) )
90 elrest 
 |-  ( ( L e. ( Fil ` Y ) /\ A e. _V ) -> ( (/) e. ( L |`t A ) <-> E. v e. L (/) = ( v i^i A ) ) )
91 8 90 syldan 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( (/) e. ( L |`t A ) <-> E. v e. L (/) = ( v i^i A ) ) )
92 dfrex2 
 |-  ( E. v e. L (/) = ( v i^i A ) <-> -. A. v e. L -. (/) = ( v i^i A ) )
93 91 92 bitrdi 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( (/) e. ( L |`t A ) <-> -. A. v e. L -. (/) = ( v i^i A ) ) )
94 93 con2bid 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( A. v e. L -. (/) = ( v i^i A ) <-> -. (/) e. ( L |`t A ) ) )
95 89 94 syl5bb 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( A. v e. L ( v i^i A ) =/= (/) <-> -. (/) e. ( L |`t A ) ) )
96 87 95 bitr4d 
 |-  ( ( L e. ( Fil ` Y ) /\ A C_ Y ) -> ( ( L |`t A ) e. ( Fil ` A ) <-> A. v e. L ( v i^i A ) =/= (/) ) )