Theorem fsubbas 10281

Description: A condition for a set to generate a filter base. (Contributed by Jeff Hankins, 2-Sep-2009.)

Assertion

Ref	Expression
fsubbas	|- (A e. B -> (( fi ` A) e. fBas <-> (A =/= (/) /\ (/) e/ ( fi ` A))))

Proof of Theorem fsubbas

Step	Hyp	Ref	Expression
1		fveq2 4681	. . . . . . . . 9 |- (A = (/) -> ( fi ` A) = ( fi ` (/)))
2		eq0 2889	. . . . . . . . . 10 |- (( fi ` (/)) = (/) <-> A.t -. t e. ( fi ` (/)))
3		ss0 2902	. . . . . . . . . . . . . . 15 |- (y C_ (/) -> y = (/))
4		vprc 3449	. . . . . . . . . . . . . . . . . . 19 |- -. _V e. _V
5		int0 3230	. . . . . . . . . . . . . . . . . . . 20 |- |^|(/) = _V
6	5	eleq1i 1960	. . . . . . . . . . . . . . . . . . 19 |- (|^|(/) e. _V <-> _V e. _V)
7	4, 6	mtbir 209	. . . . . . . . . . . . . . . . . 18 |- -. |^|(/) e. _V
8		isset 2296	. . . . . . . . . . . . . . . . . 18 |- (|^|(/) e. _V <-> E.t t = |^|(/))
9	7, 8	mtbi 208	. . . . . . . . . . . . . . . . 17 |- -. E.t t = |^|(/)
10	9	nexr 1455	. . . . . . . . . . . . . . . 16 |- -. t = |^|(/)
11		inteq 3217	. . . . . . . . . . . . . . . . 17 |- (y = (/) -> |^|y = |^|(/))
12	11	eqeq2d 1895	. . . . . . . . . . . . . . . 16 |- (y = (/) -> (t = |^|y <-> t = |^|(/)))
13	10, 12	mtbiri 785	. . . . . . . . . . . . . . 15 |- (y = (/) -> -. t = |^|y)
14	3, 13	syl 12	. . . . . . . . . . . . . 14 |- (y C_ (/) -> -. t = |^|y)
15		imnan 261	. . . . . . . . . . . . . 14 |- ((y C_ (/) -> -. t = |^|y) <-> -. (y C_ (/) /\ t = |^|y))
16	14, 15	mpbi 206	. . . . . . . . . . . . 13 |- -. (y C_ (/) /\ t = |^|y)
17		3simpb 873	. . . . . . . . . . . . 13 |- ((y C_ (/) /\ y e. Fin /\ t = |^|y) -> (y C_ (/) /\ t = |^|y))
18	16, 17	mto 121	. . . . . . . . . . . 12 |- -. (y C_ (/) /\ y e. Fin /\ t = |^|y)
19	18	nex 1456	. . . . . . . . . . 11 |- -. E.y(y C_ (/) /\ y e. Fin /\ t = |^|y)
20		visset 2295	. . . . . . . . . . . 12 |- t e. _V
21		eqeq1 1890	. . . . . . . . . . . . . 14 |- (x = t -> (x = |^|y <-> t = |^|y))
22	21	3anbi3d 1174	. . . . . . . . . . . . 13 |- (x = t -> ((y C_ (/) /\ y e. Fin /\ x = |^|y) <-> (y C_ (/) /\ y e. Fin /\ t = |^|y)))
23	22	exbidv 1657	. . . . . . . . . . . 12 |- (x = t -> (E.y(y C_ (/) /\ y e. Fin /\ x = |^|y) <-> E.y(y C_ (/) /\ y e. Fin /\ t = |^|y)))
24		0ex 3446	. . . . . . . . . . . . 13 |- (/) e. _V
25		fiv 10212	. . . . . . . . . . . . 13 |- ((/) e. _V -> ( fi ` (/)) = {x | E.y(y C_ (/) /\ y e. Fin /\ x = |^|y)})
26	24, 25	ax-mp 7	. . . . . . . . . . . 12 |- ( fi ` (/)) = {x | E.y(y C_ (/) /\ y e. Fin /\ x = |^|y)}
27	20, 23, 26	elab2 2407	. . . . . . . . . . 11 |- (t e. ( fi ` (/)) <-> E.y(y C_ (/) /\ y e. Fin /\ t = |^|y))
28	19, 27	mtbir 209	. . . . . . . . . 10 |- -. t e. ( fi ` (/))
29	2, 28	mpgbir 1334	. . . . . . . . 9 |- ( fi ` (/)) = (/)
30	1, 29	syl6eq 1944	. . . . . . . 8 |- (A = (/) -> ( fi ` A) = (/))
31	30	a1i 8	. . . . . . 7 |- (A e. B -> (A = (/) -> ( fi ` A) = (/)))
32	31	necon3d 2041	. . . . . 6 |- (A e. B -> (( fi ` A) =/= (/) -> A =/= (/)))
33	32	imp 377	. . . . 5 |- ((A e. B /\ ( fi ` A) =/= (/)) -> A =/= (/))
34		fbasne0 10262	. . . . 5 |- (( fi ` A) e. fBas -> ( fi ` A) =/= (/))
35	33, 34	sylan2 500	. . . 4 |- ((A e. B /\ ( fi ` A) e. fBas) -> A =/= (/))
36		0nelfb 10277	. . . . 5 |- (( fi ` A) e. fBas -> (/) e/ ( fi ` A))
37	36	adantl 424	. . . 4 |- ((A e. B /\ ( fi ` A) e. fBas) -> (/) e/ ( fi ` A))
38	35, 37	jca 310	. . 3 |- ((A e. B /\ ( fi ` A) e. fBas) -> (A =/= (/) /\ (/) e/ ( fi ` A)))
39	38	ex 402	. 2 |- (A e. B -> (( fi ` A) e. fBas -> (A =/= (/) /\ (/) e/ ( fi ` A))))
40		fine2 10214	. . . . . . 7 |- (A e. B -> (A =/= (/) -> ( fi ` A) =/= (/)))
41	40	imp 377	. . . . . 6 |- ((A e. B /\ A =/= (/)) -> ( fi ` A) =/= (/))
42	41	3adant3 896	. . . . 5 |- ((A e. B /\ A =/= (/) /\ (/) e/ ( fi ` A)) -> ( fi ` A) =/= (/))
43		simp3 878	. . . . 5 |- ((A e. B /\ A =/= (/) /\ (/) e/ ( fi ` A)) -> (/) e/ ( fi ` A))
44		infi 10280	. . . . . . . 8 |- (A e. B -> ((x e. ( fi ` A) /\ y e. ( fi ` A)) -> (x i^i y) e. ( fi ` A)))
45		ssid 2634	. . . . . . . . 9 |- (x i^i y) C_ (x i^i y)
46		sseq1 2637	. . . . . . . . . 10 |- (z = (x i^i y) -> (z C_ (x i^i y) <-> (x i^i y) C_ (x i^i y)))
47	46	rcla4ev 2381	. . . . . . . . 9 |- (((x i^i y) e. ( fi ` A) /\ (x i^i y) C_ (x i^i y)) -> E.z e. ( fi ` A)z C_ (x i^i y))
48	45, 47	mpan2 760	. . . . . . . 8 |- ((x i^i y) e. ( fi ` A) -> E.z e. ( fi ` A)z C_ (x i^i y))
49	44, 48	syl6 25	. . . . . . 7 |- (A e. B -> ((x e. ( fi ` A) /\ y e. ( fi ` A)) -> E.z e. ( fi ` A)z C_ (x i^i y)))
50	49	r19.21aivv 2183	. . . . . 6 |- (A e. B -> A.x e. ( fi ` A)A.y e. ( fi ` A)E.z e. ( fi ` A)z C_ (x i^i y))
51	50	3ad2ant1 897	. . . . 5 |- ((A e. B /\ A =/= (/) /\ (/) e/ ( fi ` A)) -> A.x e. ( fi ` A)A.y e. ( fi ` A)E.z e. ( fi ` A)z C_ (x i^i y))
52	42, 43, 51	3jca 1050	. . . 4 |- ((A e. B /\ A =/= (/) /\ (/) e/ ( fi ` A)) -> (( fi ` A) =/= (/) /\ (/) e/ ( fi ` A) /\ A.x e. ( fi ` A)A.y e. ( fi ` A)E.z e. ( fi ` A)z C_ (x i^i y)))
53		fvex 4689	. . . . 5 |- ( fi ` A) e. _V
54		isfbas2 10263	. . . . 5 |- (( fi ` A) e. _V -> (( fi ` A) e. fBas <-> (( fi ` A) =/= (/) /\ (/) e/ ( fi ` A) /\ A.x e. ( fi ` A)A.y e. ( fi ` A)E.z e. ( fi ` A)z C_ (x i^i y))))
55	53, 54	ax-mp 7	. . . 4 |- (( fi ` A) e. fBas <-> (( fi ` A) =/= (/) /\ (/) e/ ( fi ` A) /\ A.x e. ( fi ` A)A.y e. ( fi ` A)E.z e. ( fi ` A)z C_ (x i^i y)))
56	52, 55	sylibr 217	. . 3 |- ((A e. B /\ A =/= (/) /\ (/) e/ ( fi ` A)) -> ( fi ` A) e. fBas)
57	56	3expib 1070	. 2 |- (A e. B -> ((A =/= (/) /\ (/) e/ ( fi ` A)) -> ( fi ` A) e. fBas))
58	39, 57	impbid 574	1 |- (A e. B -> (( fi ` A) e. fBas <-> (A =/= (/) /\ (/) e/ ( fi ` A))))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871   =/= wne 2017   e/ wnel 2018  A.wral 2105  E.wrex 2106  _Vcvv 2292   i^i cin 2592   C_ wss 2593  (/)c0 2875  |^|cint 3214  ` cfv 3998  Fincfn 5426   fi cfi 10210  fBascfbas 10257

This theorem is referenced by:  hausfillim 10303  isufil2 15565  ufileulem 15572  ufileu 15573  filufint 15574  flimcls 15588  fmfnfm 15598  fclsfnflim 15614  flimfnfcls 15615  fcluscomp 15621

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-fin 5430  df-fi 10211  df-fbas 10259

Copyright terms: Public domain