Theorem topfneec 15501

Description: A cover is equivalent to a topology iff it is a base for that topology.

Hypothesis

Ref	Expression
topfneec.1	|- R = (Fne i^i `'Fne)

Assertion

Ref	Expression
topfneec	|- (J e. Top -> (A e. [J]R <-> (A e. Bases /\ (topGen` A) = J)))

Proof of Theorem topfneec

Step	Hyp	Ref	Expression
1		elisset 2299	. . 3 |- (A e. [J]R -> A e. _V)
2	1	anim2i 362	. 2 |- ((J e. Top /\ A e. [J]R) -> (J e. Top /\ A e. _V))
3		elisset 2299	. . . 4 |- (A e. Bases -> A e. _V)
4	3	adantr 425	. . 3 |- ((A e. Bases /\ (topGen` A) = J) -> A e. _V)
5	4	anim2i 362	. 2 |- ((J e. Top /\ (A e. Bases /\ (topGen` A) = J)) -> (J e. Top /\ A e. _V))
6		eceq2 5336	. . . . . . 7 |- (j = J -> [j]R = [J]R)
7		breq1 3341	. . . . . . . 8 |- (j = J -> (jRc <-> JRc))
8	7	abbidv 2008	. . . . . . 7 |- (j = J -> {c | jRc} = {c | JRc})
9	6, 8	eqeq12d 1899	. . . . . 6 |- (j = J -> ([j]R = {c | jRc} <-> [J]R = {c | JRc}))
10		visset 2295	. . . . . . 7 |- j e. _V
11	10	dfec2 5321	. . . . . 6 |- [j]R = {c | jRc}
12	9, 11	vtoclg 2346	. . . . 5 |- (J e. Top -> [J]R = {c | JRc})
13	12	eleq2d 1964	. . . 4 |- (J e. Top -> (A e. [J]R <-> A e. {c | JRc}))
14	13	adantr 425	. . 3 |- ((J e. Top /\ A e. _V) -> (A e. [J]R <-> A e. {c | JRc}))
15		breq2 3342	. . . . 5 |- (c = A -> (JRc <-> JRA))
16	15	elabg 2405	. . . 4 |- (A e. _V -> (A e. {c | JRc} <-> JRA))
17	16	adantl 424	. . 3 |- ((J e. Top /\ A e. _V) -> (A e. {c | JRc} <-> JRA))
18		brcnvg 4142	. . . . . 6 |- ((J e. Top /\ A e. _V) -> (J`'FneA <-> AFneJ))
19	18	anbi2d 678	. . . . 5 |- ((J e. Top /\ A e. _V) -> ((JFneA /\ J`'FneA) <-> (JFneA /\ AFneJ)))
20		simpll 448	. . . . . . 7 |- (((J e. Top /\ A e. _V) /\ (JFneA /\ AFneJ)) -> J e. Top)
21		elssuni 3206	. . . . . . . . . . . . . . 15 |- (s e. A -> s C_ U.A)
22	21	ad2antll 443	. . . . . . . . . . . . . 14 |- (((J e. Top /\ A e. _V) /\ (AFneJ /\ s e. A)) -> s C_ U.A)
23		eqid 1884	. . . . . . . . . . . . . . . 16 |- U.A = U.A
24		eqid 1884	. . . . . . . . . . . . . . . 16 |- U.J = U.J
25	23, 24	fnebas 15483	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ AFneJ) -> U.A = U.J)
26	25	ad2ant2r 445	. . . . . . . . . . . . . 14 |- (((J e. Top /\ A e. _V) /\ (AFneJ /\ s e. A)) -> U.A = U.J)
27	22, 26	sseqtrd 2653	. . . . . . . . . . . . 13 |- (((J e. Top /\ A e. _V) /\ (AFneJ /\ s e. A)) -> s C_ U.J)
28		fnessex 15484	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ AFneJ /\ s e. A) /\ x e. s) -> E.o e. J (x e. o /\ o C_ s))
29	28	r19.21aiva 2176	. . . . . . . . . . . . . . 15 |- ((J e. Top /\ AFneJ /\ s e. A) -> A.x e. s E.o e. J (x e. o /\ o C_ s))
30	29	3expb 1068	. . . . . . . . . . . . . 14 |- ((J e. Top /\ (AFneJ /\ s e. A)) -> A.x e. s E.o e. J (x e. o /\ o C_ s))
31	30	adantlr 429	. . . . . . . . . . . . 13 |- (((J e. Top /\ A e. _V) /\ (AFneJ /\ s e. A)) -> A.x e. s E.o e. J (x e. o /\ o C_ s))
32	27, 31	jca 310	. . . . . . . . . . . 12 |- (((J e. Top /\ A e. _V) /\ (AFneJ /\ s e. A)) -> (s C_ U.J /\ A.x e. s E.o e. J (x e. o /\ o C_ s)))
33	32	anassrs 489	. . . . . . . . . . 11 |- ((((J e. Top /\ A e. _V) /\ AFneJ) /\ s e. A) -> (s C_ U.J /\ A.x e. s E.o e. J (x e. o /\ o C_ s)))
34	33	adantlrl 434	. . . . . . . . . 10 |- ((((J e. Top /\ A e. _V) /\ (JFneA /\ AFneJ)) /\ s e. A) -> (s C_ U.J /\ A.x e. s E.o e. J (x e. o /\ o C_ s)))
35		eltop2 8900	. . . . . . . . . . . 12 |- (J e. Top -> (s e. J <-> (s C_ U.J /\ A.x e. s E.o e. J (x e. o /\ o C_ s))))
36	35	adantr 425	. . . . . . . . . . 11 |- ((J e. Top /\ A e. _V) -> (s e. J <-> (s C_ U.J /\ A.x e. s E.o e. J (x e. o /\ o C_ s))))
37	36	ad2antrr 440	. . . . . . . . . 10 |- ((((J e. Top /\ A e. _V) /\ (JFneA /\ AFneJ)) /\ s e. A) -> (s e. J <-> (s C_ U.J /\ A.x e. s E.o e. J (x e. o /\ o C_ s))))
38	34, 37	mpbird 213	. . . . . . . . 9 |- ((((J e. Top /\ A e. _V) /\ (JFneA /\ AFneJ)) /\ s e. A) -> s e. J)
39	38	ex 402	. . . . . . . 8 |- (((J e. Top /\ A e. _V) /\ (JFneA /\ AFneJ)) -> (s e. A -> s e. J))
40	39	ssrdv 2622	. . . . . . 7 |- (((J e. Top /\ A e. _V) /\ (JFneA /\ AFneJ)) -> A C_ J)
41		fnessex 15484	. . . . . . . . . . 11 |- (((A e. _V /\ JFneA /\ o e. J) /\ x e. o) -> E.s e. A (x e. s /\ s C_ o))
42	41	r19.21aiva 2176	. . . . . . . . . 10 |- ((A e. _V /\ JFneA /\ o e. J) -> A.x e. o E.s e. A (x e. s /\ s C_ o))
43	42	3expia 1069	. . . . . . . . 9 |- ((A e. _V /\ JFneA) -> (o e. J -> A.x e. o E.s e. A (x e. s /\ s C_ o)))
44	43	r19.21aiv 2175	. . . . . . . 8 |- ((A e. _V /\ JFneA) -> A.o e. J A.x e. o E.s e. A (x e. s /\ s C_ o))
45	44	ad2ant2lr 446	. . . . . . 7 |- (((J e. Top /\ A e. _V) /\ (JFneA /\ AFneJ)) -> A.o e. J A.x e. o E.s e. A (x e. s /\ s C_ o))
46		basgen2 8909	. . . . . . 7 |- ((J e. Top /\ A C_ J /\ A.o e. J A.x e. o E.s e. A (x e. s /\ s C_ o)) -> (A e. Bases /\ (topGen` A) = J))
47	20, 40, 45, 46	syl111anc 1100	. . . . . 6 |- (((J e. Top /\ A e. _V) /\ (JFneA /\ AFneJ)) -> (A e. Bases /\ (topGen` A) = J))
48		tgtop 8898	. . . . . . . . . . . 12 |- (J e. Top -> (topGen` J) = J)
49	48	adantr 425	. . . . . . . . . . 11 |- ((J e. Top /\ A e. _V) -> (topGen` J) = J)
50	49	eqeq2d 1895	. . . . . . . . . 10 |- ((J e. Top /\ A e. _V) -> ((topGen` A) = (topGen` J) <-> (topGen` A) = J))
51	50	biimprd 171	. . . . . . . . 9 |- ((J e. Top /\ A e. _V) -> ((topGen` A) = J -> (topGen` A) = (topGen` J)))
52	51	anim2d 620	. . . . . . . 8 |- ((J e. Top /\ A e. _V) -> ((A e. Bases /\ (topGen` A) = J) -> (A e. Bases /\ (topGen` A) = (topGen` J))))
53	52	imp 377	. . . . . . 7 |- (((J e. Top /\ A e. _V) /\ (A e. Bases /\ (topGen` A) = J)) -> (A e. Bases /\ (topGen` A) = (topGen` J)))
54		unieq 3185	. . . . . . . . . . 11 |- ((topGen` A) = (topGen` J) -> U.(topGen` A) = U.(topGen` J))
55	54	ad2antll 443	. . . . . . . . . 10 |- ((J e. Top /\ (A e. Bases /\ (topGen` A) = (topGen` J))) -> U.(topGen` A) = U.(topGen` J))
56		unitg 8893	. . . . . . . . . . 11 |- (A e. Bases -> U.(topGen` A) = U.A)
57	56	ad2antrl 442	. . . . . . . . . 10 |- ((J e. Top /\ (A e. Bases /\ (topGen` A) = (topGen` J))) -> U.(topGen` A) = U.A)
58		topbas 8897	. . . . . . . . . . . 12 |- (J e. Top -> J e. Bases)
59		unitg 8893	. . . . . . . . . . . 12 |- (J e. Bases -> U.(topGen` J) = U.J)
60	58, 59	syl 12	. . . . . . . . . . 11 |- (J e. Top -> U.(topGen` J) = U.J)
61	60	adantr 425	. . . . . . . . . 10 |- ((J e. Top /\ (A e. Bases /\ (topGen` A) = (topGen` J))) -> U.(topGen` J) = U.J)
62	55, 57, 61	3eqtr3d 1934	. . . . . . . . 9 |- ((J e. Top /\ (A e. Bases /\ (topGen` A) = (topGen` J))) -> U.A = U.J)
63		eqimss2 2667	. . . . . . . . . . . . . 14 |- ((topGen` A) = (topGen` J) -> (topGen` J) C_ (topGen` A))
64	63	ad2antrl 442	. . . . . . . . . . . . 13 |- (((J e. Top /\ A e. Bases) /\ ((topGen` A) = (topGen` J) /\ U.A = U.J)) -> (topGen` J) C_ (topGen` A))
65	58	ad2antrr 440	. . . . . . . . . . . . . 14 |- (((J e. Top /\ A e. Bases) /\ ((topGen` A) = (topGen` J) /\ U.A = U.J)) -> J e. Bases)
66		simplr 449	. . . . . . . . . . . . . 14 |- (((J e. Top /\ A e. Bases) /\ ((topGen` A) = (topGen` J) /\ U.A = U.J)) -> A e. Bases)
67		eqcom 1886	. . . . . . . . . . . . . . . 16 |- (U.A = U.J <-> U.J = U.A)
68	67	biimpi 168	. . . . . . . . . . . . . . 15 |- (U.A = U.J -> U.J = U.A)
69	68	ad2antll 443	. . . . . . . . . . . . . 14 |- (((J e. Top /\ A e. Bases) /\ ((topGen` A) = (topGen` J) /\ U.A = U.J)) -> U.J = U.A)
70	24, 23	topbasfne 15499	. . . . . . . . . . . . . 14 |- ((J e. Bases /\ A e. Bases /\ U.J = U.A) -> ((topGen` J) C_ (topGen` A) <-> JFneA))
71	65, 66, 69, 70	syl111anc 1100	. . . . . . . . . . . . 13 |- (((J e. Top /\ A e. Bases) /\ ((topGen` A) = (topGen` J) /\ U.A = U.J)) -> ((topGen` J) C_ (topGen` A) <-> JFneA))
72	64, 71	mpbid 212	. . . . . . . . . . . 12 |- (((J e. Top /\ A e. Bases) /\ ((topGen` A) = (topGen` J) /\ U.A = U.J)) -> JFneA)
73		eqimss 2665	. . . . . . . . . . . . . 14 |- ((topGen` A) = (topGen` J) -> (topGen` A) C_ (topGen` J))
74	73	ad2antrl 442	. . . . . . . . . . . . 13 |- (((J e. Top /\ A e. Bases) /\ ((topGen` A) = (topGen` J) /\ U.A = U.J)) -> (topGen` A) C_ (topGen` J))
75		simprr 451	. . . . . . . . . . . . . 14 |- (((J e. Top /\ A e. Bases) /\ ((topGen` A) = (topGen` J) /\ U.A = U.J)) -> U.A = U.J)
76	23, 24	topbasfne 15499	. . . . . . . . . . . . . 14 |- ((A e. Bases /\ J e. Bases /\ U.A = U.J) -> ((topGen` A) C_ (topGen` J) <-> AFneJ))
77	66, 65, 75, 76	syl111anc 1100	. . . . . . . . . . . . 13 |- (((J e. Top /\ A e. Bases) /\ ((topGen` A) = (topGen` J) /\ U.A = U.J)) -> ((topGen` A) C_ (topGen` J) <-> AFneJ))
78	74, 77	mpbid 212	. . . . . . . . . . . 12 |- (((J e. Top /\ A e. Bases) /\ ((topGen` A) = (topGen` J) /\ U.A = U.J)) -> AFneJ)
79	72, 78	jca 310	. . . . . . . . . . 11 |- (((J e. Top /\ A e. Bases) /\ ((topGen` A) = (topGen` J) /\ U.A = U.J)) -> (JFneA /\ AFneJ))
80	79	expr 418	. . . . . . . . . 10 |- (((J e. Top /\ A e. Bases) /\ (topGen` A) = (topGen` J)) -> (U.A = U.J -> (JFneA /\ AFneJ)))
81	80	anasss 488	. . . . . . . . 9 |- ((J e. Top /\ (A e. Bases /\ (topGen` A) = (topGen` J))) -> (U.A = U.J -> (JFneA /\ AFneJ)))
82	62, 81	mpd 29	. . . . . . . 8 |- ((J e. Top /\ (A e. Bases /\ (topGen` A) = (topGen` J))) -> (JFneA /\ AFneJ))
83	82	adantlr 429	. . . . . . 7 |- (((J e. Top /\ A e. _V) /\ (A e. Bases /\ (topGen` A) = (topGen` J))) -> (JFneA /\ AFneJ))
84	53, 83	syldan 516	. . . . . 6 |- (((J e. Top /\ A e. _V) /\ (A e. Bases /\ (topGen` A) = J)) -> (JFneA /\ AFneJ))
85	47, 84	impbida 577	. . . . 5 |- ((J e. Top /\ A e. _V) -> ((JFneA /\ AFneJ) <-> (A e. Bases /\ (topGen` A) = J)))
86	19, 85	bitrd 587	. . . 4 |- ((J e. Top /\ A e. _V) -> ((JFneA /\ J`'FneA) <-> (A e. Bases /\ (topGen` A) = J)))
87		topfneec.1	. . . . . 6 |- R = (Fne i^i `'Fne)
88	87	breqi 3344	. . . . 5 |- (JRA <-> J(Fne i^i `'Fne)A)
89		brin 3388	. . . . 5 |- (J(Fne i^i `'Fne)A <-> (JFneA /\ J`'FneA))
90	88, 89	bitri 190	. . . 4 |- (JRA <-> (JFneA /\ J`'FneA))
91	86, 90	syl5bb 591	. . 3 |- ((J e. Top /\ A e. _V) -> (JRA <-> (A e. Bases /\ (topGen` A) = J)))
92	14, 17, 91	3bitrd 603	. 2 |- ((J e. Top /\ A e. _V) -> (A e. [J]R <-> (A e. Bases /\ (topGen` A) = J)))
93	2, 5, 92	pm5.21nd 744	1 |- (J e. Top -> (A e. [J]R <-> (A e. Bases /\ (topGen` A) = J)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  {cab 1871  A.wral 2105  E.wrex 2106  _Vcvv 2292   i^i cin 2592   C_ wss 2593  U.cuni 3177   class class class wbr 3338  `'ccnv 3985  ` cfv 3998  [cec 5316  Topctop 8857  Basesctb 8859  topGenctg 8860  Fnecfne 15457

This theorem is referenced by:  topfneec2 15502

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-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-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-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  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-fv 4014  df-ec 5320  df-top 8861  df-bases 8863  df-topgen 8864  df-fne 15463

Copyright terms: Public domain