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