isfil2 - Metamath Proof Explorer

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

Theorem isfil2 20871

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 20866	. . . 4
2		0nelfil 20864	. . . 4
3		filtop 20870	. . . 4
4	1, 2, 3	3jca 1188	. . 3 $/\$ $/\$
5		elpwi 3960	. . . . 5
6		filss 20868	. . . . . . . . 9 $/\$ $/\$ $/\$
7	6	3exp2 1227	. . . . . . . 8
8	7	com23 81	. . . . . . 7
9	8	imp 431	. . . . . 6 $/\$
10	9	rexlimdv 2877	. . . . 5 $/\$
11	5, 10	sylan2 477	. . . 4 $/\$
12	11	ralrimiva 2802	. . 3
13		filin 20869	. . . . 5 $/\$ $/\$
14	13	3expb 1209	. . . 4 $/\$ $/\$
15	14	ralrimivva 2809	. . 3
16	4, 12, 15	3jca 1188	. 2 $/\$ $/\$ $/\$ $/\$
17		simp11 1038	. . . 4 $/\$ $/\$ $/\$ $/\$
18		simp13 1040	. . . . . 6 $/\$ $/\$ $/\$ $/\$
19		ne0i 3737	. . . . . 6
20	18, 19	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$
21		simp12 1039	. . . . . 6 $/\$ $/\$ $/\$ $/\$
22		df-nel 2625	. . . . . 6
23	21, 22	sylibr 216	. . . . 5 $/\$ $/\$ $/\$ $/\$
24		ssid 3451	. . . . . . . . 9
25		sseq1 3453	. . . . . . . . . 10
26	25	rspcev 3150	. . . . . . . . 9 $/\$
27	24, 26	mpan2 677	. . . . . . . 8
28	27	ralimi 2781	. . . . . . 7
29	28	ralimi 2781	. . . . . 6
30	29	3ad2ant3 1031	. . . . 5 $/\$ $/\$ $/\$ $/\$
31	20, 23, 30	3jca 1188	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		isfbas2 20850	. . . . 5 $/\$ $/\$ $/\$
33	18, 32	syl 17	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	17, 31, 33	mpbir2and 933	. . 3 $/\$ $/\$ $/\$ $/\$
35		n0 3741	. . . . . . . 8
36		elin 3617	. . . . . . . . . 10 $/\$
37		elpwi 3960	. . . . . . . . . . 11
38	37	anim2i 573	. . . . . . . . . 10 $/\$ $/\$
39	36, 38	sylbi 199	. . . . . . . . 9 $/\$
40	39	eximi 1707	. . . . . . . 8 $/\$
41	35, 40	sylbi 199	. . . . . . 7 $/\$
42		df-rex 2743	. . . . . . 7 $/\$
43	41, 42	sylibr 216	. . . . . 6
44	43	imim1i 60	. . . . 5
45	44	ralimi 2781	. . . 4
46	45	3ad2ant2 1030	. . 3 $/\$ $/\$ $/\$ $/\$
47		isfil 20862	. . 3 $/\$
48	34, 46, 47	sylanbrc 670	. 2 $/\$ $/\$ $/\$ $/\$
49	16, 48	impbii 191	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 985

wex 1663

wcel 1887

wne 2622

wnel 2623

wral 2737

wrex 2738

cin 3403

wss 3404

c0 3731

cpw 3951

cfv 5582

cfbas 18958

cfil 20860

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-op 3975 df-uni 4199 df-br 4403 df-opab 4462 df-mpt 4463 df-id 4749 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-iota 5546 df-fun 5584 df-fv 5590 df-fbas 18967 df-fil 20861

This theorem is referenced by: isfild 20873 infil 20878 neifil 20895 trfil2 20902

W3C validator