Metamath Proof Explorer

Theorem trfbas2

Description: Conditions for the trace of a filter base F to be a filter base. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion trfbas2 
|- ( ( F e. ( fBas ` Y ) /\ A C_ Y ) -> ( ( F |`t A ) e. ( fBas ` A ) <-> -. (/) e. ( F |`t A ) ) )

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( F e. ( fBas ` Y ) -> Y e. dom fBas )
2 ssexg 
 |-  ( ( A C_ Y /\ Y e. dom fBas ) -> A e. _V )
3 2 ancoms 
 |-  ( ( Y e. dom fBas /\ A C_ Y ) -> A e. _V )
4 1 3 sylan 
 |-  ( ( F e. ( fBas ` Y ) /\ A C_ Y ) -> A e. _V )
5 restsspw 
 |-  ( F |`t A ) C_ ~P A
6 5 a1i 
 |-  ( ( F e. ( fBas ` Y ) /\ A C_ Y ) -> ( F |`t A ) C_ ~P A )
7 fbasne0 
 |-  ( F e. ( fBas ` Y ) -> F =/= (/) )
8 7 adantr 
 |-  ( ( F e. ( fBas ` Y ) /\ A C_ Y ) -> F =/= (/) )
9 n0 
 |-  ( F =/= (/) <-> E. x x e. F )
10 8 9 sylib 
 |-  ( ( F e. ( fBas ` Y ) /\ A C_ Y ) -> E. x x e. F )
11 elrestr 
 |-  ( ( F e. ( fBas ` Y ) /\ A e. _V /\ x e. F ) -> ( x i^i A ) e. ( F |`t A ) )
12 11 3expia 
 |-  ( ( F e. ( fBas ` Y ) /\ A e. _V ) -> ( x e. F -> ( x i^i A ) e. ( F |`t A ) ) )
13 4 12 syldan 
 |-  ( ( F e. ( fBas ` Y ) /\ A C_ Y ) -> ( x e. F -> ( x i^i A ) e. ( F |`t A ) ) )
14 ne0i 
 |-  ( ( x i^i A ) e. ( F |`t A ) -> ( F |`t A ) =/= (/) )
15 13 14 syl6 
 |-  ( ( F e. ( fBas ` Y ) /\ A C_ Y ) -> ( x e. F -> ( F |`t A ) =/= (/) ) )
16 15 exlimdv 
 |-  ( ( F e. ( fBas ` Y ) /\ A C_ Y ) -> ( E. x x e. F -> ( F |`t A ) =/= (/) ) )
17 10 16 mpd 
 |-  ( ( F e. ( fBas ` Y ) /\ A C_ Y ) -> ( F |`t A ) =/= (/) )
18 fbasssin 
 |-  ( ( F e. ( fBas ` Y ) /\ z e. F /\ w e. F ) -> E. x e. F x C_ ( z i^i w ) )
19 18 3expb 
 |-  ( ( F e. ( fBas ` Y ) /\ ( z e. F /\ w e. F ) ) -> E. x e. F x C_ ( z i^i w ) )
20 19 adantlr 
 |-  ( ( ( F e. ( fBas ` Y ) /\ A C_ Y ) /\ ( z e. F /\ w e. F ) ) -> E. x e. F x C_ ( z i^i w ) )
21 simplll 
 |-  ( ( ( ( F e. ( fBas ` Y ) /\ A C_ Y ) /\ ( z e. F /\ w e. F ) ) /\ ( x e. F /\ x C_ ( z i^i w ) ) ) -> F e. ( fBas ` Y ) )
22 4 ad2antrr 
 |-  ( ( ( ( F e. ( fBas ` Y ) /\ A C_ Y ) /\ ( z e. F /\ w e. F ) ) /\ ( x e. F /\ x C_ ( z i^i w ) ) ) -> A e. _V )
23 simprl 
 |-  ( ( ( ( F e. ( fBas ` Y ) /\ A C_ Y ) /\ ( z e. F /\ w e. F ) ) /\ ( x e. F /\ x C_ ( z i^i w ) ) ) -> x e. F )
24 21 22 23 11 syl3anc 
 |-  ( ( ( ( F e. ( fBas ` Y ) /\ A C_ Y ) /\ ( z e. F /\ w e. F ) ) /\ ( x e. F /\ x C_ ( z i^i w ) ) ) -> ( x i^i A ) e. ( F |`t A ) )
25 ssrin 
 |-  ( x C_ ( z i^i w ) -> ( x i^i A ) C_ ( ( z i^i w ) i^i A ) )
26 25 ad2antll 
 |-  ( ( ( ( F e. ( fBas ` Y ) /\ A C_ Y ) /\ ( z e. F /\ w e. F ) ) /\ ( x e. F /\ x C_ ( z i^i w ) ) ) -> ( x i^i A ) C_ ( ( z i^i w ) i^i A ) )
27 vex 
 |-  x e. _V
28 27 inex1 
 |-  ( x i^i A ) e. _V
29 28 elpw 
 |-  ( ( x i^i A ) e. ~P ( ( z i^i w ) i^i A ) <-> ( x i^i A ) C_ ( ( z i^i w ) i^i A ) )
30 26 29 sylibr 
 |-  ( ( ( ( F e. ( fBas ` Y ) /\ A C_ Y ) /\ ( z e. F /\ w e. F ) ) /\ ( x e. F /\ x C_ ( z i^i w ) ) ) -> ( x i^i A ) e. ~P ( ( z i^i w ) i^i A ) )
31 inelcm 
 |-  ( ( ( x i^i A ) e. ( F |`t A ) /\ ( x i^i A ) e. ~P ( ( z i^i w ) i^i A ) ) -> ( ( F |`t A ) i^i ~P ( ( z i^i w ) i^i A ) ) =/= (/) )
32 24 30 31 syl2anc 
 |-  ( ( ( ( F e. ( fBas ` Y ) /\ A C_ Y ) /\ ( z e. F /\ w e. F ) ) /\ ( x e. F /\ x C_ ( z i^i w ) ) ) -> ( ( F |`t A ) i^i ~P ( ( z i^i w ) i^i A ) ) =/= (/) )
33 20 32 rexlimddv 
 |-  ( ( ( F e. ( fBas ` Y ) /\ A C_ Y ) /\ ( z e. F /\ w e. F ) ) -> ( ( F |`t A ) i^i ~P ( ( z i^i w ) i^i A ) ) =/= (/) )
34 33 ralrimivva 
 |-  ( ( F e. ( fBas ` Y ) /\ A C_ Y ) -> A. z e. F A. w e. F ( ( F |`t A ) i^i ~P ( ( z i^i w ) i^i A ) ) =/= (/) )
35 vex 
 |-  z e. _V
36 35 inex1 
 |-  ( z i^i A ) e. _V
37 36 a1i 
 |-  ( ( ( F e. ( fBas ` Y ) /\ A C_ Y ) /\ z e. F ) -> ( z i^i A ) e. _V )
38 elrest 
 |-  ( ( F e. ( fBas ` Y ) /\ A e. _V ) -> ( x e. ( F |`t A ) <-> E. z e. F x = ( z i^i A ) ) )
39 4 38 syldan 
 |-  ( ( F e. ( fBas ` Y ) /\ A C_ Y ) -> ( x e. ( F |`t A ) <-> E. z e. F x = ( z i^i A ) ) )
40 vex 
 |-  w e. _V
41 40 inex1 
 |-  ( w i^i A ) e. _V
42 41 a1i 
 |-  ( ( ( ( F e. ( fBas ` Y ) /\ A C_ Y ) /\ x = ( z i^i A ) ) /\ w e. F ) -> ( w i^i A ) e. _V )
43 elrest 
 |-  ( ( F e. ( fBas ` Y ) /\ A e. _V ) -> ( y e. ( F |`t A ) <-> E. w e. F y = ( w i^i A ) ) )
44 4 43 syldan 
 |-  ( ( F e. ( fBas ` Y ) /\ A C_ Y ) -> ( y e. ( F |`t A ) <-> E. w e. F y = ( w i^i A ) ) )
45 44 adantr 
 |-  ( ( ( F e. ( fBas ` Y ) /\ A C_ Y ) /\ x = ( z i^i A ) ) -> ( y e. ( F |`t A ) <-> E. w e. F y = ( w i^i A ) ) )
46 ineq12 
 |-  ( ( x = ( z i^i A ) /\ y = ( w i^i A ) ) -> ( x i^i y ) = ( ( z i^i A ) i^i ( w i^i A ) ) )
47 inindir 
 |-  ( ( z i^i w ) i^i A ) = ( ( z i^i A ) i^i ( w i^i A ) )
48 46 47 eqtr4di 
 |-  ( ( x = ( z i^i A ) /\ y = ( w i^i A ) ) -> ( x i^i y ) = ( ( z i^i w ) i^i A ) )
49 48 pweqd 
 |-  ( ( x = ( z i^i A ) /\ y = ( w i^i A ) ) -> ~P ( x i^i y ) = ~P ( ( z i^i w ) i^i A ) )
50 49 ineq2d 
 |-  ( ( x = ( z i^i A ) /\ y = ( w i^i A ) ) -> ( ( F |`t A ) i^i ~P ( x i^i y ) ) = ( ( F |`t A ) i^i ~P ( ( z i^i w ) i^i A ) ) )
51 50 neeq1d 
 |-  ( ( x = ( z i^i A ) /\ y = ( w i^i A ) ) -> ( ( ( F |`t A ) i^i ~P ( x i^i y ) ) =/= (/) <-> ( ( F |`t A ) i^i ~P ( ( z i^i w ) i^i A ) ) =/= (/) ) )
52 51 adantll 
 |-  ( ( ( ( F e. ( fBas ` Y ) /\ A C_ Y ) /\ x = ( z i^i A ) ) /\ y = ( w i^i A ) ) -> ( ( ( F |`t A ) i^i ~P ( x i^i y ) ) =/= (/) <-> ( ( F |`t A ) i^i ~P ( ( z i^i w ) i^i A ) ) =/= (/) ) )
53 42 45 52 ralxfr2d 
 |-  ( ( ( F e. ( fBas ` Y ) /\ A C_ Y ) /\ x = ( z i^i A ) ) -> ( A. y e. ( F |`t A ) ( ( F |`t A ) i^i ~P ( x i^i y ) ) =/= (/) <-> A. w e. F ( ( F |`t A ) i^i ~P ( ( z i^i w ) i^i A ) ) =/= (/) ) )
54 37 39 53 ralxfr2d 
 |-  ( ( F e. ( fBas ` Y ) /\ A C_ Y ) -> ( A. x e. ( F |`t A ) A. y e. ( F |`t A ) ( ( F |`t A ) i^i ~P ( x i^i y ) ) =/= (/) <-> A. z e. F A. w e. F ( ( F |`t A ) i^i ~P ( ( z i^i w ) i^i A ) ) =/= (/) ) )
55 34 54 mpbird 
 |-  ( ( F e. ( fBas ` Y ) /\ A C_ Y ) -> A. x e. ( F |`t A ) A. y e. ( F |`t A ) ( ( F |`t A ) i^i ~P ( x i^i y ) ) =/= (/) )
56 isfbas 
 |-  ( A e. _V -> ( ( F |`t A ) e. ( fBas ` A ) <-> ( ( F |`t A ) C_ ~P A /\ ( ( F |`t A ) =/= (/) /\ (/) e/ ( F |`t A ) /\ A. x e. ( F |`t A ) A. y e. ( F |`t A ) ( ( F |`t A ) i^i ~P ( x i^i y ) ) =/= (/) ) ) ) )
57 56 baibd 
 |-  ( ( A e. _V /\ ( F |`t A ) C_ ~P A ) -> ( ( F |`t A ) e. ( fBas ` A ) <-> ( ( F |`t A ) =/= (/) /\ (/) e/ ( F |`t A ) /\ A. x e. ( F |`t A ) A. y e. ( F |`t A ) ( ( F |`t A ) i^i ~P ( x i^i y ) ) =/= (/) ) ) )
58 3anan32 
 |-  ( ( ( F |`t A ) =/= (/) /\ (/) e/ ( F |`t A ) /\ A. x e. ( F |`t A ) A. y e. ( F |`t A ) ( ( F |`t A ) i^i ~P ( x i^i y ) ) =/= (/) ) <-> ( ( ( F |`t A ) =/= (/) /\ A. x e. ( F |`t A ) A. y e. ( F |`t A ) ( ( F |`t A ) i^i ~P ( x i^i y ) ) =/= (/) ) /\ (/) e/ ( F |`t A ) ) )
59 57 58 bitrdi 
 |-  ( ( A e. _V /\ ( F |`t A ) C_ ~P A ) -> ( ( F |`t A ) e. ( fBas ` A ) <-> ( ( ( F |`t A ) =/= (/) /\ A. x e. ( F |`t A ) A. y e. ( F |`t A ) ( ( F |`t A ) i^i ~P ( x i^i y ) ) =/= (/) ) /\ (/) e/ ( F |`t A ) ) ) )
60 59 baibd 
 |-  ( ( ( A e. _V /\ ( F |`t A ) C_ ~P A ) /\ ( ( F |`t A ) =/= (/) /\ A. x e. ( F |`t A ) A. y e. ( F |`t A ) ( ( F |`t A ) i^i ~P ( x i^i y ) ) =/= (/) ) ) -> ( ( F |`t A ) e. ( fBas ` A ) <-> (/) e/ ( F |`t A ) ) )
61 4 6 17 55 60 syl22anc 
 |-  ( ( F e. ( fBas ` Y ) /\ A C_ Y ) -> ( ( F |`t A ) e. ( fBas ` A ) <-> (/) e/ ( F |`t A ) ) )
62 df-nel 
 |-  ( (/) e/ ( F |`t A ) <-> -. (/) e. ( F |`t A ) )
63 61 62 bitrdi 
 |-  ( ( F e. ( fBas ` Y ) /\ A C_ Y ) -> ( ( F |`t A ) e. ( fBas ` A ) <-> -. (/) e. ( F |`t A ) ) )