Theorem opnin 7866

Description: The intersection of two open sets of a metric space is open.

Hypothesis

Ref	Expression
opni.1	|- J = (Open` D)

Assertion

Ref	Expression
opnin	|- ((D e. Met /\ A e. J /\ B e. J) -> (A i^i B) e. J)

Proof of Theorem opnin

Step	Hyp	Ref	Expression
1		pm3.27 323	. . . . . . . . . . 11 |- ((D e. Met /\ (A i^i B) (_ dom dom D) -> (A i^i B) (_ dom dom D)
2	1	a1i 8	. . . . . . . . . 10 |- ((A.z e. A E.v e. ran ( ball ` D)(z e. v /\ v (_ A) /\ A.w e. B E.u e. ran ( ball ` D)(w e. u /\ u (_ B)) -> ((D e. Met /\ (A i^i B) (_ dom dom D) -> (A i^i B) (_ dom dom D))
3		reeanv 1781	. . . . . . . . . . . . . . . . . . 19 |- (E.v e. ran ( ball ` D)E.u e. ran ( ball ` D)((x e. v /\ v (_ A) /\ (x e. u /\ u (_ B)) <-> (E.v e. ran ( ball ` D)(x e. v /\ v (_ A) /\ E.u e. ran ( ball ` D)(x e. u /\ u (_ B)))
4		blss 7850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((D e. Met /\ v e. ran ( ball ` D) /\ x e. v) -> E.f e. RR (0 < f /\ (x( ball ` D)f) (_ v))
5	4	3expib 838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (D e. Met -> ((v e. ran ( ball ` D) /\ x e. v) -> E.f e. RR (0 < f /\ (x( ball ` D)f) (_ v)))
6		blss 7850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((D e. Met /\ u e. ran ( ball ` D) /\ x e. u) -> E.g e. RR (0 < g /\ (x( ball ` D)g) (_ u))
7	6	3expib 838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (D e. Met -> ((u e. ran ( ball ` D) /\ x e. u) -> E.g e. RR (0 < g /\ (x( ball ` D)g) (_ u)))
8	5, 7	anim12d 560	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (D e. Met -> (((v e. ran ( ball ` D) /\ x e. v) /\ (u e. ran ( ball ` D) /\ x e. u)) -> (E.f e. RR (0 < f /\ (x( ball ` D)f) (_ v) /\ E.g e. RR (0 < g /\ (x( ball ` D)g) (_ u))))
9	8	adantr 391	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((D e. Met /\ x e. dom dom D) -> (((v e. ran ( ball ` D) /\ x e. v) /\ (u e. ran ( ball ` D) /\ x e. u)) -> (E.f e. RR (0 < f /\ (x( ball ` D)f) (_ v) /\ E.g e. RR (0 < g /\ (x( ball ` D)g) (_ u))))
10		eqid 1478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- dom dom D = dom dom D
11	10	blin 7849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (((D e. Met /\ x e. dom dom D) /\ (f e. RR /\ 0 < f) /\ (g e. RR /\ 0 < g)) -> ((x( ball ` D)f) i^i (x( ball ` D)g)) = (x( ball ` D)if(f <_ g, f, g)))
12	11	3expb 836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (((D e. Met /\ x e. dom dom D) /\ ((f e. RR /\ 0 < f) /\ (g e. RR /\ 0 < g))) -> ((x( ball ` D)f) i^i (x( ball ` D)g)) = (x( ball ` D)if(f <_ g, f, g)))
13	12	sseq1d 2091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((D e. Met /\ x e. dom dom D) /\ ((f e. RR /\ 0 < f) /\ (g e. RR /\ 0 < g))) -> (((x( ball ` D)f) i^i (x( ball ` D)g)) (_ (A i^i B) <-> (x( ball ` D)if(f <_ g, f, g)) (_ (A i^i B)))
14		eleq2 1538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (y = (x( ball ` D)if(f <_ g, f, g)) -> (x e. y <-> x e. (x( ball ` D)if(f <_ g, f, g))))
15		sseq1 2085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (y = (x( ball ` D)if(f <_ g, f, g)) -> (y (_ (A i^i B) <-> (x( ball ` D)if(f <_ g, f, g)) (_ (A i^i B)))
16	14, 15	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (y = (x( ball ` D)if(f <_ g, f, g)) -> ((x e. y /\ y (_ (A i^i B)) <-> (x e. (x( ball ` D)if(f <_ g, f, g)) /\ (x( ball ` D)if(f <_ g, f, g)) (_ (A i^i B))))
17	16	rcla4ev 1880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (((x( ball ` D)if(f <_ g, f, g)) e. ran ( ball ` D) /\ (x e. (x( ball ` D)if(f <_ g, f, g)) /\ (x( ball ` D)if(f <_ g, f, g)) (_ (A i^i B))) -> E.y e. ran ( ball ` D)(x e. y /\ y (_ (A i^i B)))
18	10	blelrn 7845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (((D e. Met /\ x e. dom dom D) /\ (if(f <_ g, f, g) e. RR /\ 0 < if(f <_ g, f, g))) -> (x( ball ` D)if(f <_ g, f, g)) e. ran ( ball ` D))
19		eleq1 1537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (f = if(f <_ g, f, g) -> (f e. RR <-> if(f <_ g, f, g) e. RR))
20		breq2 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (f = if(f <_ g, f, g) -> (0 < f <-> 0 < if(f <_ g, f, g)))
21	19, 20	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (f = if(f <_ g, f, g) -> ((f e. RR /\ 0 < f) <-> (if(f <_ g, f, g) e. RR /\ 0 < if(f <_ g, f, g))))
22		eleq1 1537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (g = if(f <_ g, f, g) -> (g e. RR <-> if(f <_ g, f, g) e. RR))
23		breq2 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (g = if(f <_ g, f, g) -> (0 < g <-> 0 < if(f <_ g, f, g)))
24	22, 23	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (g = if(f <_ g, f, g) -> ((g e. RR /\ 0 < g) <-> (if(f <_ g, f, g) e. RR /\ 0 < if(f <_ g, f, g))))
25	21, 24	ifboth 2379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (((f e. RR /\ 0 < f) /\ (g e. RR /\ 0 < g)) -> (if(f <_ g, f, g) e. RR /\ 0 < if(f <_ g, f, g)))
26	18, 25	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (((D e. Met /\ x e. dom dom D) /\ ((f e. RR /\ 0 < f) /\ (g e. RR /\ 0 < g))) -> (x( ball ` D)if(f <_ g, f, g)) e. ran ( ball ` D))
27	26	adantr 391	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((((D e. Met /\ x e. dom dom D) /\ ((f e. RR /\ 0 < f) /\ (g e. RR /\ 0 < g))) /\ (x( ball ` D)if(f <_ g, f, g)) (_ (A i^i B)) -> (x( ball ` D)if(f <_ g, f, g)) e. ran ( ball ` D))
28	10	blcntr 7842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (((D e. Met /\ x e. dom dom D) /\ (if(f <_ g, f, g) e. RR /\ 0 < if(f <_ g, f, g))) -> x e. (x( ball ` D)if(f <_ g, f, g)))
29	28, 25	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (((D e. Met /\ x e. dom dom D) /\ ((f e. RR /\ 0 < f) /\ (g e. RR /\ 0 < g))) -> x e. (x( ball ` D)if(f <_ g, f, g)))
30	29	anim1i 334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ((((D e. Met /\ x e. dom dom D) /\ ((f e. RR /\ 0 < f) /\ (g e. RR /\ 0 < g))) /\ (x( ball ` D)if(f <_ g, f, g)) (_ (A i^i B)) -> (x e. (x( ball ` D)if(f <_ g, f, g)) /\ (x( ball ` D)if(f <_ g, f, g)) (_ (A i^i B)))
31	17, 27, 30	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((((D e. Met /\ x e. dom dom D) /\ ((f e. RR /\ 0 < f) /\ (g e. RR /\ 0 < g))) /\ (x( ball ` D)if(f <_ g, f, g)) (_ (A i^i B)) -> E.y e. ran ( ball ` D)(x e. y /\ y (_ (A i^i B)))
32	31	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((D e. Met /\ x e. dom dom D) /\ ((f e. RR /\ 0 < f) /\ (g e. RR /\ 0 < g))) -> ((x( ball ` D)if(f <_ g, f, g)) (_ (A i^i B) -> E.y e. ran ( ball ` D)(x e. y /\ y (_ (A i^i B))))
33	13, 32	sylbid 203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((D e. Met /\ x e. dom dom D) /\ ((f e. RR /\ 0 < f) /\ (g e. RR /\ 0 < g))) -> (((x( ball ` D)f) i^i (x( ball ` D)g)) (_ (A i^i B) -> E.y e. ran ( ball ` D)(x e. y /\ y (_ (A i^i B))))
34	33	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((D e. Met /\ x e. dom dom