Theorem isfild 21662

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
isfild	|- ( ph -> F e. ( Fil ` A ) )

Distinct variable groups:   x, y, A   z, A   x, F, y   y, z, F   ph, x, y   ph, z   ps, y

Allowed substitution hints:   ps( x, z)

Proof of Theorem isfild

Step	Hyp	Ref	Expression
1		isfild.1	. . . . 5 |- ( ph -> ( x e. F <-> ( x C_ A /\ ps ) ) )
2		selpw 4165	. . . . . . 7 |- ( x e. ~P A <-> x C_ A )
3	2	biimpri 218	. . . . . 6 |- ( x C_ A -> x e. ~P A )
4	3	adantr 481	. . . . 5 |- ( ( x C_ A /\ ps ) -> x e. ~P A )
5	1, 4	syl6bi 243	. . . 4 |- ( ph -> ( x e. F -> x e. ~P A ) )
6	5	ssrdv 3609	. . 3 |- ( ph -> F C_ ~P A )
7		isfild.4	. . . 4 |- ( ph -> -. [. (/) / x ]. ps )
8		isfild.2	. . . . . 6 |- ( ph -> A e. _V )
9	1, 8	isfildlem 21661	. . . . 5 |- ( ph -> ( (/) e. F <-> ( (/) C_ A /\ [. (/) / x ]. ps ) ) )
10		simpr 477	. . . . 5 |- ( ( (/) C_ A /\ [. (/) / x ]. ps ) -> [. (/) / x ]. ps )
11	9, 10	syl6bi 243	. . . 4 |- ( ph -> ( (/) e. F -> [. (/) / x ]. ps ) )
12	7, 11	mtod 189	. . 3 |- ( ph -> -. (/) e. F )
13		isfild.3	. . . . 5 |- ( ph -> [. A / x ]. ps )
14		ssid 3624	. . . . 5 |- A C_ A
15	13, 14	jctil 560	. . . 4 |- ( ph -> ( A C_ A /\ [. A / x ]. ps ) )
16	1, 8	isfildlem 21661	. . . 4 |- ( ph -> ( A e. F <-> ( A C_ A /\ [. A / x ]. ps ) ) )
17	15, 16	mpbird 247	. . 3 |- ( ph -> A e. F )
18	6, 12, 17	3jca 1242	. 2 |- ( ph -> ( F C_ ~P A /\ -. (/) e. F /\ A e. F ) )
19		elpwi 4168	. . . 4 |- ( y e. ~P A -> y C_ A )
20		isfild.5	. . . . . . . . . . 11 |- ( ( ph /\ y C_ A /\ z C_ y ) -> ( [. z / x ]. ps -> [. y / x ]. ps ) )
21		simp2 1062	. . . . . . . . . . 11 |- ( ( ph /\ y C_ A /\ z C_ y ) -> y C_ A )
22	20, 21	jctild 566	. . . . . . . . . 10 |- ( ( ph /\ y C_ A /\ z C_ y ) -> ( [. z / x ]. ps -> ( y C_ A /\ [. y / x ]. ps ) ) )
23	22	adantld 483	. . . . . . . . 9 |- ( ( ph /\ y C_ A /\ z C_ y ) -> ( ( z C_ A /\ [. z / x ]. ps ) -> ( y C_ A /\ [. y / x ]. ps ) ) )
24	1, 8	isfildlem 21661	. . . . . . . . . 10 |- ( ph -> ( z e. F <-> ( z C_ A /\ [. z / x ]. ps ) ) )
25	24	3ad2ant1 1082	. . . . . . . . 9 |- ( ( ph /\ y C_ A /\ z C_ y ) -> ( z e. F <-> ( z C_ A /\ [. z / x ]. ps ) ) )
26	1, 8	isfildlem 21661	. . . . . . . . . 10 |- ( ph -> ( y e. F <-> ( y C_ A /\ [. y / x ]. ps ) ) )
27	26	3ad2ant1 1082	. . . . . . . . 9 |- ( ( ph /\ y C_ A /\ z C_ y ) -> ( y e. F <-> ( y C_ A /\ [. y / x ]. ps ) ) )
28	23, 25, 27	3imtr4d 283	. . . . . . . 8 |- ( ( ph /\ y C_ A /\ z C_ y ) -> ( z e. F -> y e. F ) )
29	28	3expa 1265	. . . . . . 7 |- ( ( ( ph /\ y C_ A ) /\ z C_ y ) -> ( z e. F -> y e. F ) )
30	29	impancom 456	. . . . . 6 |- ( ( ( ph /\ y C_ A ) /\ z e. F ) -> ( z C_ y -> y e. F ) )
31	30	rexlimdva 3031	. . . . 5 |- ( ( ph /\ y C_ A ) -> ( E. z e. F z C_ y -> y e. F ) )
32	31	ex 450	. . . 4 |- ( ph -> ( y C_ A -> ( E. z e. F z C_ y -> y e. F ) ) )
33	19, 32	syl5 34	. . 3 |- ( ph -> ( y e. ~P A -> ( E. z e. F z C_ y -> y e. F ) ) )
34	33	ralrimiv 2965	. 2 |- ( ph -> A. y e. ~P A ( E. z e. F z C_ y -> y e. F ) )
35		ssinss1 3841	. . . . . . 7 |- ( y C_ A -> ( y i^i z ) C_ A )
36	35	ad2antrr 762	. . . . . 6 |- ( ( ( y C_ A /\ [. y / x ]. ps ) /\ ( z C_ A /\ [. z / x ]. ps ) ) -> ( y i^i z ) C_ A )
37	36	a1i 11	. . . . 5 |- ( ph -> ( ( ( y C_ A /\ [. y / x ]. ps ) /\ ( z C_ A /\ [. z / x ]. ps ) ) -> ( y i^i z ) C_ A ) )
38		an4 865	. . . . . 6 |- ( ( ( 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		isfild.6	. . . . . . . 8 |- ( ( ph /\ y C_ A /\ z C_ A ) -> ( ( [. y / x ]. ps /\ [. z / x ]. ps ) -> [. ( y i^i z ) / x ]. ps ) )
40	39	3expb 1266	. . . . . . 7 |- ( ( ph /\ ( y C_ A /\ z C_ A ) ) -> ( ( [. y / x ]. ps /\ [. z / x ]. ps ) -> [. ( y i^i z ) / x ]. ps ) )
41	40	expimpd 629	. . . . . 6 |- ( ph -> ( ( ( y C_ A /\ z C_ A ) /\ ( [. y / x ]. ps /\ [. z / x ]. ps ) ) -> [. ( y i^i z ) / x ]. ps ) )
42	38, 41	syl5bi 232	. . . . 5 |- ( ph -> ( ( ( y C_ A /\ [. y / x ]. ps ) /\ ( z C_ A /\ [. z / x ]. ps ) ) -> [. ( y i^i z ) / x ]. ps ) )
43	37, 42	jcad 555	. . . 4 |- ( 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	26, 24	anbi12d 747	. . . 4 |- ( ph -> ( ( y e. F /\ z e. F ) <-> ( ( y C_ A /\ [. y / x ]. ps ) /\ ( z C_ A /\ [. z / x ]. ps ) ) ) )
45	1, 8	isfildlem 21661	. . . 4 |- ( ph -> ( ( y i^i z ) e. F <-> ( ( y i^i z ) C_ A /\ [. ( y i^i z ) / x ]. ps ) ) )
46	43, 44, 45	3imtr4d 283	. . 3 |- ( ph -> ( ( y e. F /\ z e. F ) -> ( y i^i z ) e. F ) )
47	46	ralrimivv 2970	. 2 |- ( ph -> A. y e. F A. z e. F ( y i^i z ) e. F )
48		isfil2 21660	. 2 |- ( 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	18, 34, 47, 48	syl3anbrc 1246	1 |- ( ph -> F e. ( Fil ` A ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   [.wsbc 3435   i^i cin 3573   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   ` cfv 5888   Filcfil 21649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fv 5896  df-fbas 19743  df-fil 21650

This theorem is referenced by:  snfil  21668  fgcl  21682  filuni  21689  cfinfil  21697  csdfil  21698  supfil  21699  fin1aufil  21736