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 ) =/= (/) ) )