isfil2 - Metamath Proof Explorer

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

Theorem isfil2 20483

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 20478	. . . 4
2		0nelfil 20476	. . . 4
3		filtop 20482	. . . 4
4	1, 2, 3	3jca 1176	. . 3 $/\$ $/\$
5		elpwi 4024	. . . . 5
6		filss 20480	. . . . . . . . 9 $/\$ $/\$ $/\$
7	6	3exp2 1214	. . . . . . . 8
8	7	com23 78	. . . . . . 7
9	8	imp 429	. . . . . 6 $/\$
10	9	rexlimdv 2947	. . . . 5 $/\$
11	5, 10	sylan2 474	. . . 4 $/\$
12	11	ralrimiva 2871	. . 3
13		filin 20481	. . . . 5 $/\$ $/\$
14	13	3expb 1197	. . . 4 $/\$ $/\$
15	14	ralrimivva 2878	. . 3
16	4, 12, 15	3jca 1176	. 2 $/\$ $/\$ $/\$ $/\$
17		simp11 1026	. . . 4 $/\$ $/\$ $/\$ $/\$
18		simp13 1028	. . . . . 6 $/\$ $/\$ $/\$ $/\$
19		ne0i 3799	. . . . . 6
20	18, 19	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$
21		simp12 1027	. . . . . 6 $/\$ $/\$ $/\$ $/\$
22		df-nel 2655	. . . . . 6
23	21, 22	sylibr 212	. . . . 5 $/\$ $/\$ $/\$ $/\$
24		ssid 3518	. . . . . . . . 9
25		sseq1 3520	. . . . . . . . . 10
26	25	rspcev 3210	. . . . . . . . 9 $/\$
27	24, 26	mpan2 671	. . . . . . . 8
28	27	ralimi 2850	. . . . . . 7
29	28	ralimi 2850	. . . . . 6
30	29	3ad2ant3 1019	. . . . 5 $/\$ $/\$ $/\$ $/\$
31	20, 23, 30	3jca 1176	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		isfbas2 20462	. . . . 5 $/\$ $/\$ $/\$
33	18, 32	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	17, 31, 33	mpbir2and 922	. . 3 $/\$ $/\$ $/\$ $/\$
35		n0 3803	. . . . . . . 8
36		elin 3683	. . . . . . . . . 10 $/\$
37		elpwi 4024	. . . . . . . . . . 11
38	37	anim2i 569	. . . . . . . . . 10 $/\$ $/\$
39	36, 38	sylbi 195	. . . . . . . . 9 $/\$
40	39	eximi 1657	. . . . . . . 8 $/\$
41	35, 40	sylbi 195	. . . . . . 7 $/\$
42		df-rex 2813	. . . . . . 7 $/\$
43	41, 42	sylibr 212	. . . . . 6
44	43	imim1i 58	. . . . 5
45	44	ralimi 2850	. . . 4
46	45	3ad2ant2 1018	. . 3 $/\$ $/\$ $/\$ $/\$
47		isfil 20474	. . 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 1613

wcel 1819

wne 2652

wnel 2653

wral 2807

wrex 2808

cin 3470

wss 3471

c0 3793

cpw 4015

cfv 5594

cfbas 18533

cfil 20472

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-op 4039 df-uni 4252 df-br 4457 df-opab 4516 df-mpt 4517 df-id 4804 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fv 5602 df-fbas 18543 df-fil 20473

This theorem is referenced by: isfild 20485 infil 20490 neifil 20507 trfil2 20514

W3C validator