isfil2 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > isfil2		Structured version Unicode version

Theorem isfil2 20120

Description: Derive the standard axioms of a filter. (Contributed by Mario Carneiro, 27-Nov-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)

**Assertion**
Ref	Expression
isfil2	$/\$ $/\$ $/\$ $/\$

Distinct variable groups:

Proof of Theorem isfil2 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		filsspw 20115	. . . 4
2		0nelfil 20113	. . . 4
3		filtop 20119	. . . 4
4	1, 2, 3	3jca 1176	. . 3 $/\$ $/\$
5		elpwi 4019	. . . . 5
6		filss 20117	. . . . . . . . 9 $/\$ $/\$ $/\$
7	6	3exp2 1214	. . . . . . . 8
8	7	com23 78	. . . . . . 7
9	8	imp 429	. . . . . 6 $/\$
10	9	rexlimdv 2953	. . . . 5 $/\$
11	5, 10	sylan2 474	. . . 4 $/\$
12	11	ralrimiva 2878	. . 3
13		filin 20118	. . . . 5 $/\$ $/\$
14	13	3expb 1197	. . . 4 $/\$ $/\$
15	14	ralrimivva 2885	. . 3
16	4, 12, 15	3jca 1176	. 2 $/\$ $/\$ $/\$ $/\$
17		simp11 1026	. . . 4 $/\$ $/\$ $/\$ $/\$
18		simp13 1028	. . . . . 6 $/\$ $/\$ $/\$ $/\$
19		ne0i 3791	. . . . . 6
20	18, 19	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$
21		simp12 1027	. . . . . 6 $/\$ $/\$ $/\$ $/\$
22		df-nel 2665	. . . . . 6
23	21, 22	sylibr 212	. . . . 5 $/\$ $/\$ $/\$ $/\$
24		ssid 3523	. . . . . . . . 9
25		sseq1 3525	. . . . . . . . . 10
26	25	rspcev 3214	. . . . . . . . 9 $/\$
27	24, 26	mpan2 671	. . . . . . . 8
28	27	ralimi 2857	. . . . . . 7
29	28	ralimi 2857	. . . . . 6
30	29	3ad2ant3 1019	. . . . 5 $/\$ $/\$ $/\$ $/\$
31	20, 23, 30	3jca 1176	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		isfbas2 20099	. . . . 5 $/\$ $/\$ $/\$
33	18, 32	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	17, 31, 33	mpbir2and 920	. . 3 $/\$ $/\$ $/\$ $/\$
35		n0 3794	. . . . . . . 8
36		elin 3687	. . . . . . . . . 10 $/\$
37		elpwi 4019	. . . . . . . . . . 11
38	37	anim2i 569	. . . . . . . . . 10 $/\$ $/\$
39	36, 38	sylbi 195	. . . . . . . . 9 $/\$
40	39	eximi 1635	. . . . . . . 8 $/\$
41	35, 40	sylbi 195	. . . . . . 7 $/\$
42		df-rex 2820	. . . . . . 7 $/\$
43	41, 42	sylibr 212	. . . . . 6
44	43	imim1i 58	. . . . 5
45	44	ralimi 2857	. . . 4
46	45	3ad2ant2 1018	. . 3 $/\$ $/\$ $/\$ $/\$
47		isfil 20111	. . 3 $/\$
48	34, 46, 47	sylanbrc 664	. 2 $/\$ $/\$ $/\$ $/\$
49	16, 48	impbii 188	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 973

wex 1596

wcel 1767

wne 2662

wnel 2663

wral 2814

wrex 2815

cin 3475

wss 3476

c0 3785

cpw 4010

cfv 5588

cfbas 18205

cfil 20109

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-op 4034 df-uni 4246 df-br 4448 df-opab 4506 df-mpt 4507 df-id 4795 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fv 5596 df-fbas 18215 df-fil 20110

This theorem is referenced by: isfild 20122 infil 20127 neifil 20144 trfil2 20151

W3C validator