Metamath Proof Explorer

Theorem isfild

Description: Sufficient condition for a set of the form { x e. ~P A | ph } to be a filter. (Contributed by Mario Carneiro, 1-Dec-2013) (Revised by Stefan O'Rear, 2-Aug-2015) (Revised by AV, 10-Apr-2024)

Ref Expression
Hypotheses isfild.1 
|- ( ph -> ( x e. F <-> ( x C_ A /\ ps ) ) )
isfild.2 
|- ( ph -> A e. V )
isfild.3 
|- ( ph -> [. A / x ]. ps )
isfild.4 
|- ( ph -> -. [. (/) / x ]. ps )
isfild.5 
|- ( ( ph /\ y C_ A /\ z C_ y ) -> ( [. z / x ]. ps -> [. y / x ]. ps ) )
isfild.6 
|- ( ( ph /\ y C_ A /\ z C_ A ) -> ( ( [. y / x ]. ps /\ [. z / x ]. ps ) -> [. ( y i^i z ) / x ]. ps ) )
Assertion isfild 
|- ( ph -> F e. ( Fil ` A ) )

Proof

Step Hyp Ref Expression
1 isfild.1 
 |-  ( ph -> ( x e. F <-> ( x C_ A /\ ps ) ) )
2 isfild.2 
 |-  ( ph -> A e. V )
3 isfild.3 
 |-  ( ph -> [. A / x ]. ps )
4 isfild.4 
 |-  ( ph -> -. [. (/) / x ]. ps )
5 isfild.5 
 |-  ( ( ph /\ y C_ A /\ z C_ y ) -> ( [. z / x ]. ps -> [. y / x ]. ps ) )
6 isfild.6 
 |-  ( ( ph /\ y C_ A /\ z C_ A ) -> ( ( [. y / x ]. ps /\ [. z / x ]. ps ) -> [. ( y i^i z ) / x ]. ps ) )
7 velpw 
 |-  ( x e. ~P A <-> x C_ A )
8 7 biranri 
 |-  ( ( x C_ A /\ ps ) -> x e. ~P A )
9 1 8 biimtrdi 
 |-  ( ph -> ( x e. F -> x e. ~P A ) )
10 9 ssrdv 
 |-  ( ph -> F C_ ~P A )
11 1 2 isfildlem 
 |-  ( ph -> ( (/) e. F <-> ( (/) C_ A /\ [. (/) / x ]. ps ) ) )
12 simpr 
 |-  ( ( (/) C_ A /\ [. (/) / x ]. ps ) -> [. (/) / x ]. ps )
13 11 12 biimtrdi 
 |-  ( ph -> ( (/) e. F -> [. (/) / x ]. ps ) )
14 4 13 mtod 
 |-  ( ph -> -. (/) e. F )
15 ssid 
 |-  A C_ A
16 3 15 jctil 
 |-  ( ph -> ( A C_ A /\ [. A / x ]. ps ) )
17 1 2 isfildlem 
 |-  ( ph -> ( A e. F <-> ( A C_ A /\ [. A / x ]. ps ) ) )
18 16 17 mpbird 
 |-  ( ph -> A e. F )
19 10 14 18 3jca 
 |-  ( ph -> ( F C_ ~P A /\ -. (/) e. F /\ A e. F ) )
20 elpwi 
 |-  ( y e. ~P A -> y C_ A )
21 simp2 
 |-  ( ( ph /\ y C_ A /\ z C_ y ) -> y C_ A )
22 5 21 jctild 
 |-  ( ( ph /\ y C_ A /\ z C_ y ) -> ( [. z / x ]. ps -> ( y C_ A /\ [. y / x ]. ps ) ) )
23 22 adantld 
 |-  ( ( ph /\ y C_ A /\ z C_ y ) -> ( ( z C_ A /\ [. z / x ]. ps ) -> ( y C_ A /\ [. y / x ]. ps ) ) )
24 1 2 isfildlem 
 |-  ( ph -> ( z e. F <-> ( z C_ A /\ [. z / x ]. ps ) ) )
25 24 3ad2ant1 
 |-  ( ( ph /\ y C_ A /\ z C_ y ) -> ( z e. F <-> ( z C_ A /\ [. z / x ]. ps ) ) )
26 1 2 isfildlem 
 |-  ( ph -> ( y e. F <-> ( y C_ A /\ [. y / x ]. ps ) ) )
27 26 3ad2ant1 
 |-  ( ( ph /\ y C_ A /\ z C_ y ) -> ( y e. F <-> ( y C_ A /\ [. y / x ]. ps ) ) )
28 23 25 27 3imtr4d 
 |-  ( ( ph /\ y C_ A /\ z C_ y ) -> ( z e. F -> y e. F ) )
29 28 3expa 
 |-  ( ( ( ph /\ y C_ A ) /\ z C_ y ) -> ( z e. F -> y e. F ) )
30 29 impancom 
 |-  ( ( ( ph /\ y C_ A ) /\ z e. F ) -> ( z C_ y -> y e. F ) )
31 30 rexlimdva 
 |-  ( ( ph /\ y C_ A ) -> ( E. z e. F z C_ y -> y e. F ) )
32 31 ex 
 |-  ( ph -> ( y C_ A -> ( E. z e. F z C_ y -> y e. F ) ) )
33 20 32 syl5 
 |-  ( ph -> ( y e. ~P A -> ( E. z e. F z C_ y -> y e. F ) ) )
34 33 ralrimiv 
 |-  ( ph -> A. y e. ~P A ( E. z e. F z C_ y -> y e. F ) )
35 ssinss1 
 |-  ( y C_ A -> ( y i^i z ) C_ A )
36 35 ad2antrr 
 |-  ( ( ( y C_ A /\ [. y / x ]. ps ) /\ ( z C_ A /\ [. z / x ]. ps ) ) -> ( y i^i z ) C_ A )
37 36 a1i 
 |-  ( ph -> ( ( ( y C_ A /\ [. y / x ]. ps ) /\ ( z C_ A /\ [. z / x ]. ps ) ) -> ( y i^i z ) C_ A ) )
38 an4 
 |-  ( ( ( y C_ A /\ [. y / x ]. ps ) /\ ( z C_ A /\ [. z / x ]. ps ) ) <-> ( ( y C_ A /\ z C_ A ) /\ ( [. y / x ]. ps /\ [. z / x ]. ps ) ) )
39 6 3expb 
 |-  ( ( ph /\ ( y C_ A /\ z C_ A ) ) -> ( ( [. y / x ]. ps /\ [. z / x ]. ps ) -> [. ( y i^i z ) / x ]. ps ) )
40 39 expimpd 
 |-  ( ph -> ( ( ( y C_ A /\ z C_ A ) /\ ( [. y / x ]. ps /\ [. z / x ]. ps ) ) -> [. ( y i^i z ) / x ]. ps ) )
41 38 40 biimtrid 
 |-  ( ph -> ( ( ( y C_ A /\ [. y / x ]. ps ) /\ ( z C_ A /\ [. z / x ]. ps ) ) -> [. ( y i^i z ) / x ]. ps ) )
42 37 41 jcad 
 |-  ( ph -> ( ( ( y C_ A /\ [. y / x ]. ps ) /\ ( z C_ A /\ [. z / x ]. ps ) ) -> ( ( y i^i z ) C_ A /\ [. ( y i^i z ) / x ]. ps ) ) )
43 26 24 anbi12d 
 |-  ( ph -> ( ( y e. F /\ z e. F ) <-> ( ( y C_ A /\ [. y / x ]. ps ) /\ ( z C_ A /\ [. z / x ]. ps ) ) ) )
44 1 2 isfildlem 
 |-  ( ph -> ( ( y i^i z ) e. F <-> ( ( y i^i z ) C_ A /\ [. ( y i^i z ) / x ]. ps ) ) )
45 42 43 44 3imtr4d 
 |-  ( ph -> ( ( y e. F /\ z e. F ) -> ( y i^i z ) e. F ) )
46 45 ralrimivv 
 |-  ( ph -> A. y e. F A. z e. F ( y i^i z ) e. F )
47 isfil2 
 |-  ( F e. ( Fil ` A ) <-> ( ( F C_ ~P A /\ -. (/) e. F /\ A e. F ) /\ A. y e. ~P A ( E. z e. F z C_ y -> y e. F ) /\ A. y e. F A. z e. F ( y i^i z ) e. F ) )
48 19 34 46 47 syl3anbrc 
 |-  ( ph -> F e. ( Fil ` A ) )