Theorem ismtyhmeolem 15950

Description: Lemma for ismtyhmeo 15951.

Hypotheses

Ref	Expression
ismtyhmeo.1	|- J = (Open` M)
ismtyhmeo.2	|- K = (Open` N)

Assertion

Ref	Expression
ismtyhmeolem	|- (((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) -> A.u e. J (F"u) e. K)

Distinct variable groups:   u,M,x,y   u,N,x,y   u,J,x,y   u,K,x,y   u,F,x,y

Proof of Theorem ismtyhmeolem

Step	Hyp	Ref	Expression
1		f1ofun 4637	. . . . . . . . . 10 |- (F:dom dom M-1-1-onto->dom dom N -> Fun F)
2		fvelima 4723	. . . . . . . . . . 11 |- ((Fun F /\ w e. (F"u)) -> E.z e. u (F` z) = w)
3	2	ex 402	. . . . . . . . . 10 |- (Fun F -> (w e. (F"u) -> E.z e. u (F` z) = w))
4	1, 3	syl 12	. . . . . . . . 9 |- (F:dom dom M-1-1-onto->dom dom N -> (w e. (F"u) -> E.z e. u (F` z) = w))
5	4	adantr 425	. . . . . . . 8 |- ((F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y))) -> (w e. (F"u) -> E.z e. u (F` z) = w))
6	5	ad2antlr 441	. . . . . . 7 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ (u C_ dom dom M /\ A.v e. u E.s e. ran ( ball ` M)(v e. s /\ s C_ u))) -> (w e. (F"u) -> E.z e. u (F` z) = w))
7		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((F:dom dom M-->dom dom N /\ v e. dom dom M) -> (F` v) e. dom dom N)
8		f1of 4635	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (F:dom dom M-1-1-onto->dom dom N -> F:dom dom M-->dom dom N)
9	7, 8	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F:dom dom M-1-1-onto->dom dom N /\ v e. dom dom M) -> (F` v) e. dom dom N)
10	9	ad2ant2r 445	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y))) /\ (v e. dom dom M /\ q e. RR)) -> (F` v) e. dom dom N)
11	10	ad2ant2lr 446	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> (F` v) e. dom dom N)
12		simprlr 457	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> q e. RR)
13		simprrl 458	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> 0 < q)
14		simpll 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((M e. Met /\ F:dom dom M-1-1-onto->dom dom N) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> M e. Met)
15		simprll 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((M e. Met /\ F:dom dom M-1-1-onto->dom dom N) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> v e. dom dom M)
16		simprlr 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((M e. Met /\ F:dom dom M-1-1-onto->dom dom N) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> q e. RR)
17		simprr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((M e. Met /\ F:dom dom M-1-1-onto->dom dom N) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> 0 < q)
18		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- dom dom M = dom dom M
19	18	blssm 9127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((M e. Met /\ v e. dom dom M) /\ (q e. RR /\ 0 < q)) -> (v( ball ` M)q) C_ dom dom M)
20	14, 15, 16, 17, 19	syl22anc 1101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((M e. Met /\ F:dom dom M-1-1-onto->dom dom N) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> (v( ball ` M)q) C_ dom dom M)
21	20	adantlrr 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((M e. Met /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> (v( ball ` M)q) C_ dom dom M)
22	21	adantllr 433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> (v( ball ` M)q) C_ dom dom M)
23	22	adantrrr 439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> (v( ball ` M)q) C_ dom dom M)
24	23	sseld 2619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> (w e. (v( ball ` M)q) -> w e. dom dom M))
25	24	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ w e. (v( ball ` M)q)) -> w e. dom dom M)
26	25	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ (w e. (v( ball ` M)q) /\ (F` w) = z)) -> w e. dom dom M)
27		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((F` w) = z -> ((F` w) e. dom dom N <-> z e. dom dom N))
28		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((F:dom dom M-->dom dom N /\ w e. dom dom M) -> (F` w) e. dom dom N)
29	28, 8	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((F:dom dom M-1-1-onto->dom dom N /\ w e. dom dom M) -> (F` w) e. dom dom N)
30	27, 29	syl5cbi 226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((F:dom dom M-1-1-onto->dom dom N /\ w e. dom dom M) -> ((F` w) = z -> z e. dom dom N))
31	30	expimpd 404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (F:dom dom M-1-1-onto->dom dom N -> ((w e. dom dom M /\ (F` w) = z) -> z e. dom dom N))
32	31	ancomsd 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (F:dom dom M-1-1-onto->dom dom N -> (((F` w) = z /\ w e. dom dom M) -> z e. dom dom N))
33	32	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) -> (((F` w) = z /\ w e. dom dom M) -> z e. dom dom N))
34	33	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ w e. (v( ball ` M)q)) -> (((F` w) = z /\ w e. dom dom M) -> z e. dom dom N))
35	34	expdimp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ w e. (v( ball ` M)q)) /\ (F` w) = z) -> (w e. dom dom M -> z e. dom dom N))
36	35	anasss 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ (w e. (v( ball ` M)q) /\ (F` w) = z)) -> (w e. dom dom M -> z e. dom dom N))
37	26, 36	mpd 29	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ (w e. (v( ball ` M)q) /\ (F` w) = z)) -> z e. dom dom N)
38		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((F` w) = z -> ((F` v)N(F` w)) = ((F` v)Nz))
39	38	breq1d 3348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((F` w) = z -> (((F` v)N(F` w)) < q <-> ((F` v)Nz) < q))
40		simpll 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q))) -> v e. dom dom M)
41	40	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ w e. (v( ball ` M)q)) -> v e. dom dom M)
42		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (x = v -> (xMy) = (vMy))
43		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (x = v -> (F` x) = (F` v))
44	43	opreq1d 4897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (x = v -> ((F` x)N(F` y)) = ((F` v)N(F` y)))
45	42, 44	eqeq12d 1899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (x = v -> ((xMy) = ((F` x)N(F` y)) <-> (vMy) = ((F` v)N(F` y))))
46		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (y = w -> (vMy) = (vMw))
47		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (y = w -> (F` y) = (F` w))
48	47	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (y = w -> ((F` v)N(F` y)) = ((F` v)N(F` w)))
49	46, 48	eqeq12d 1899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (y = w -> ((vMy) = ((F` v)N(F` y)) <-> (vMw) = ((F` v)N(F` w))))
50	45, 49	rcla42v 2384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((v e. dom dom M /\ w e. dom dom M) -> (A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)) -> (vMw) = ((F` v)N(F` w))))
51	50	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)) -> ((v e. dom dom M /\ w e. dom dom M) -> (vMw) = ((F` v)N(F` w))))
52	51	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) -> ((v e. dom dom M /\ w e. dom dom M) -> (vMw) = ((F` v)N(F` w))))
53	52	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ w e. (v( ball ` M)q)) -> ((v e. dom dom M /\ w e. dom dom M) -> (vMw) = ((F` v)N(F` w))))
54	41, 25, 53	mp2and 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ w e. (v( ball ` M)q)) -> (vMw) = ((F` v)N(F` w)))
55		simpl 346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((M e. Met /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> M e. Met)
56		simprll 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((M e. Met /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> v e. dom dom M)
57		simprlr 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((M e. Met /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> q e. RR)
58		simprr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((M e. Met /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> 0 < q)
59	18	elbl 9115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (((M e. Met /\ v e. dom dom M) /\ (q e. RR /\ 0 < q)) -> (w e. (v( ball ` M)q) <-> (w e. dom dom M /\ (vMw) < q)))
60	55, 56, 57, 58, 59	syl22anc 1101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((M e. Met /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> (w e. (v( ball ` M)q) <-> (w e. dom dom M /\ (vMw) < q)))
61	60	simplbda 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((M e. Met /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) /\ w e. (v( ball ` M)q)) -> (vMw) < q)
62	61	an1rs 547	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((M e. Met /\ w e. (v( ball ` M)q)) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> (vMw) < q)
63	62	adantrrr 439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((M e. Met /\ w e. (v( ball ` M)q)) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> (vMw) < q)
64	63	an1rs 547	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((M e. Met /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ w e. (v( ball ` M)q)) -> (vMw) < q)
65	64	adantllr 433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((M e. Met /\ N e. Met) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ w e. (v( ball ` M)q)) -> (vMw) < q)
66	65	adantllr 433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ w e. (v( ball ` M)q)) -> (vMw) < q)
67	54, 66	eqbrtrrd 3359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ w e. (v( ball ` M)q)) -> ((F` v)N(F` w)) < q)
68	39, 67	syl5cbi 226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ w e. (v( ball ` M)q)) -> ((F` w) = z -> ((F` v)Nz) < q))
69	68	impr 422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ (w e. (v( ball ` M)q) /\ (F` w) = z)) -> ((F` v)Nz) < q)
70	37, 69	jca 310	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ (w e. (v( ball ` M)q) /\ (F` w) = z)) -> (z e. dom dom N /\ ((F` v)Nz) < q))
71	70	expr 418	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ w e. (v( ball ` M)q)) -> ((F` w) = z -> (z e. dom dom N /\ ((F` v)Nz) < q)))
72	71	r19.23adva 2216	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> (E.w e. (v( ball ` M)q)(F` w) = z -> (z e. dom dom N /\ ((F` v)Nz) < q)))
73		simpll 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) -> M e. Met)
74	73	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ (z e. dom dom N /\ ((F` v)Nz) < q)) -> M e. Met)
75	40	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ (z e. dom dom N /\ ((F` v)Nz) < q)) -> v e. dom dom M)
76		simplr 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q))) -> q e. RR)
77	76	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ (z e. dom dom N /\ ((F` v)Nz) < q)) -> q e. RR)
78		simprl 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q))) -> 0 < q)
79	78	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ (z e. dom dom N /\ ((F` v)Nz) < q)) -> 0 < q)
80	18	elbl 9115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((M e. Met /\ v e. dom dom M) /\ (q e. RR /\ 0 < q)) -> ((`'F` z) e. (v( ball ` M)q) <-> ((`'F` z) e. dom dom M /\ (vM(`'F` z)) < q)))
81	74, 75, 77, 79, 80	syl22anc 1101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ (z e. dom dom N /\ ((F` v)Nz) < q)) -> ((`'F` z) e. (v( ball ` M)q) <-> ((`'F` z) e. dom dom M /\ (vM(`'F` z)) < q)))
82		f1ocnvdm 4860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((F:dom dom M-1-1-onto->dom dom N /\ z e. dom dom N) -> (`'F` z) e. dom dom M)
83	82	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((M e. Met /\ N e. Met) /\ F:dom dom M-1-1-onto->dom dom N) /\ z e. dom dom N) -> (`'F` z) e. dom dom M)
84	83	adantlrr 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ z e. dom dom N) -> (`'F` z) e. dom dom M)
85	84	ad2ant2r 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ (z e. dom dom N /\ ((F` v)Nz) < q)) -> (`'F` z) e. dom dom M)
86	40	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ z e. dom dom N) -> v e. dom dom M)
87	84	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ z e. dom dom N) -> (`'F` z) e. dom dom M)
88		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (y = (`'F` z) -> (vMy) = (vM(`'F` z)))
89		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (y = (`'F` z) -> (F` y) = (F` (`'F` z)))
90	89	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (y = (`'F` z) -> ((F` v)N(F` y)) = ((F` v)N(F` (`'F` z))))
91	88, 90	eqeq12d 1899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (y = (`'F` z) -> ((vMy) = ((F` v)N(F` y)) <-> (vM(`'F` z)) = ((F` v)N(F` (`'F` z)))))
92	45, 91	rcla42v 2384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((v e. dom dom M /\ (`'F` z) e. dom dom M) -> (A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)) -> (vM(`'F` z)) = ((F` v)N(F` (`'F` z)))))
93	92	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)) -> ((v e. dom dom M /\ (`'F` z) e. dom dom M) -> (vM(`'F` z)) = ((F` v)N(F` (`'F` z)))))
94	93	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) -> ((v e. dom dom M /\ (`'F` z) e. dom dom M) -> (vM(`'F` z)) = ((F` v)N(F` (`'F` z)))))
95	94	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ z e. dom dom N) -> ((v e. dom dom M /\ (`'F` z) e. dom dom M) -> (vM(`'F` z)) = ((F` v)N(F` (`'F` z)))))
96	86, 87, 95	mp2and 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ z e. dom dom N) -> (vM(`'F` z)) = ((F` v)N(F` (`'F` z))))
97		f1ocnvfv2 4855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((F:dom dom M-1-1-onto->dom dom N /\ z e. dom dom N) -> (F` (`'F` z)) = z)
98	97	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((M e. Met /\ N e. Met) /\ F:dom dom M-1-1-onto->dom dom N) /\ z e. dom dom N) -> (F` (`'F` z)) = z)
99	98	adantlrr 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ z e. dom dom N) -> (F` (`'F` z)) = z)
100	99	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ z e. dom dom N) -> (F` (`'F` z)) = z)
101	100	opreq2d 4898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ z e. dom dom N) -> ((F` v)N(F` (`'F` z))) = ((F` v)Nz))
102	96, 101	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ z e. dom dom N) -> (vM(`'F` z)) = ((F` v)Nz))
103	102	breq1d 3348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ z e. dom dom N) -> ((vM(`'F` z)) < q <-> ((F` v)Nz) < q))
104	103	biimpar 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ z e. dom dom N) /\ ((F` v)Nz) < q) -> (vM(`'F` z)) < q)
105	104	anasss 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ (z e. dom dom N /\ ((F` v)Nz) < q)) -> (vM(`'F` z)) < q)
106	81, 85, 105	mpbir2and 802	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ (z e. dom dom N /\ ((F` v)Nz) < q)) -> (`'F` z) e. (v( ball ` M)q))
107	99	ad2ant2r 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ (z e. dom dom N /\ ((F` v)Nz) < q)) -> (F` (`'F` z)) = z)
108		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (w = (`'F` z) -> (F` w) = (F` (`'F` z)))
109	108	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = (`'F` z) -> ((F` w) = z <-> (F` (`'F` z)) = z))
110	109	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((`'F` z) e. (v( ball ` M)q) /\ (F` (`'F` z)) = z) -> E.w e. (v( ball ` M)q)(F` w) = z)
111	106, 107, 110	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) /\ (z e. dom dom N /\ ((F` v)Nz) < q)) -> E.w e. (v( ball ` M)q)(F` w) = z)
112	111	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> ((z e. dom dom N /\ ((F` v)Nz) < q) -> E.w e. (v( ball ` M)q)(F` w) = z))
113	72, 112	impbid 574	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> (E.w e. (v( ball ` M)q)(F` w) = z <-> (z e. dom dom N /\ ((F` v)Nz) < q)))
114		imaeq2 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (s = (v( ball ` M)q) -> (F"s) = (F"(v( ball ` M)q)))
115	114	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((0 < q /\ s = (v( ball ` M)q)) -> (F"s) = (F"(v( ball ` M)q)))
116	115	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> (F"s) = (F"(v( ball ` M)q)))
117	116	eleq2d 1964	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> (z e. (F"s) <-> z e. (F"(v( ball ` M)q))))
118		f1ofn 4636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (F:dom dom M-1-1-onto->dom dom N -> F Fn dom dom M)
119	118	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((M e. Met /\ F:dom dom M-1-1-onto->dom dom N) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> F Fn dom dom M)
120		fvelimab 4725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((F Fn dom dom M /\ (v( ball ` M)q) C_ dom dom M) -> (z e. (F"(v( ball ` M)q)) <-> E.w e. (v( ball ` M)q)(F` w) = z))
121	119, 20, 120	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((M e. Met /\ F:dom dom M-1-1-onto->dom dom N) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> (z e. (F"(v( ball ` M)q)) <-> E.w e. (v( ball ` M)q)(F` w) = z))
122	121	adantllr 433	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((M e. Met /\ N e. Met) /\ F:dom dom M-1-1-onto->dom dom N) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> (z e. (F"(v( ball ` M)q)) <-> E.w e. (v( ball ` M)q)(F` w) = z))
123	122	adantlrr 435	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> (z e. (F"(v( ball ` M)q)) <-> E.w e. (v( ball ` M)q)(F` w) = z))
124	123	adantrrr 439	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> (z e. (F"(v( ball ` M)q)) <-> E.w e. (v( ball ` M)q)(F` w) = z))
125	117, 124	bitrd 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> (z e. (F"s) <-> E.w e. (v( ball ` M)q)(F` w) = z))
126		simpll 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((N e. Met /\ F:dom dom M-1-1-onto->dom dom N) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> N e. Met)
127	9	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((F:dom dom M-1-1-onto->dom dom N /\ (v e. dom dom M /\ q e. RR)) -> (F` v) e. dom dom N)
128	127	ad2ant2lr 446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((N e. Met /\ F:dom dom M-1-1-onto->dom dom N) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> (F` v) e. dom dom N)
129		simprlr 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((N e. Met /\ F:dom dom M-1-1-onto->dom dom N) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> q e. RR)
130		simprr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((N e. Met /\ F:dom dom M-1-1-onto->dom dom N) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> 0 < q)
131		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- dom dom N = dom dom N
132	131	elbl 9115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((N e. Met /\ (F` v) e. dom dom N) /\ (q e. RR /\ 0 < q)) -> (z e. ((F` v)( ball ` N)q) <-> (z e. dom dom N /\ ((F` v)Nz) < q)))
133	126, 128, 129, 130, 132	syl22anc 1101	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((N e. Met /\ F:dom dom M-1-1-onto->dom dom N) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> (z e. ((F` v)( ball ` N)q) <-> (z e. dom dom N /\ ((F` v)Nz) < q)))
134	133	adantlll 432	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((((M e. Met /\ N e. Met) /\ F:dom dom M-1-1-onto->dom dom N) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> (z e. ((F` v)( ball ` N)q) <-> (z e. dom dom N /\ ((F` v)Nz) < q)))
135	134	adantlrr 435	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ 0 < q)) -> (z e. ((F` v)( ball ` N)q) <-> (z e. dom dom N /\ ((F` v)Nz) < q)))
136	135	adantrrr 439	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> (z e. ((F` v)( ball ` N)q) <-> (z e. dom dom N /\ ((F` v)Nz) < q)))
137	113, 125, 136	3bitr4d 609	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> (z e. (F"s) <-> z e. ((F` v)( ball ` N)q)))
138	137	eqrdv 1882	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> (F"s) = ((F` v)( ball ` N)q))
139		breq2 3342	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (r = q -> (0 < r <-> 0 < q))
140		opreq2 4890	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (r = q -> ((F` v)( ball ` N)r) = ((F` v)( ball ` N)q))
141	140	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (r = q -> ((F"s) = ((F` v)( ball ` N)r) <-> (F"s) = ((F` v)( ball ` N)q)))
142	139, 141	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (r = q -> ((0 < r /\ (F"s) = ((F` v)( ball ` N)r)) <-> (0 < q /\ (F"s) = ((F` v)( ball ` N)q))))
143	142	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((q e. RR /\ (0 < q /\ (F"s) = ((F` v)( ball ` N)q))) -> E.r e. RR (0 < r /\ (F"s) = ((F` v)( ball ` N)r)))
144	12, 13, 138, 143	syl12anc 1098	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> E.r e. RR (0 < r /\ (F"s) = ((F` v)( ball ` N)r)))
145		opreq1 4889	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w = (F` v) -> (w( ball ` N)r) = ((F` v)( ball ` N)r))
146	145	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = (F` v) -> ((F"s) = (w( ball ` N)r) <-> (F"s) = ((F` v)( ball ` N)r)))
147	146	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w = (F` v) -> ((0 < r /\ (F"s) = (w( ball ` N)r)) <-> (0 < r /\ (F"s) = ((F` v)( ball ` N)r))))
148	147	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w = (F` v) -> (E.r e. RR (0 < r /\ (F"s) = (w( ball ` N)r)) <-> E.r e. RR (0 < r /\ (F"s) = ((F` v)( ball ` N)r))))
149	148	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F` v) e. dom dom N /\ E.r e. RR (0 < r /\ (F"s) = ((F` v)( ball ` N)r))) -> E.w e. dom dom NE.r e. RR (0 < r /\ (F"s) = (w( ball ` N)r)))
150	11, 144, 149	syl11anc 524	. . . . . . . . . . . . . . . . . . . . 21 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ ((v e. dom dom M /\ q e. RR) /\ (0 < q /\ s = (v( ball ` M)q)))) -> E.w e. dom dom NE.r e. RR (0 < r /\ (F"s) = (w( ball ` N)r)))
151	150	exp32 408	. . . . . . . . . . . . . . . . . . . 20 |- (((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) -> ((v e. dom dom M /\ q e. RR) -> ((0 < q /\ s = (v( ball ` M)q)) -> E.w e. dom dom NE.r e. RR (0 < r /\ (F"s) = (w( ball ` N)r)))))
152	151	r19.23advv 2218	. . . . . . . . . . . . . . . . . . 19 |- (((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) -> (E.v e. dom dom ME.q e. RR (0 < q /\ s = (v( ball ` M)q)) -> E.w e. dom dom NE.r e. RR (0 < r /\ (F"s) = (w( ball ` N)r))))
153	18	blrn3 9124	. . . . . . . . . . . . . . . . . . . 20 |- (M e. Met -> (s e. ran ( ball ` M) <-> E.v e. dom dom ME.q e. RR (0 < q /\ s = (v( ball ` M)q))))
154	153	ad2antrr 440	. . . . . . . . . . . . . . . . . . 19 |- (((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) -> (s e. ran ( ball ` M) <-> E.v e. dom dom ME.q e. RR (0 < q /\ s = (v( ball ` M)q))))
155	131	blrn3 9124	. . . . . . . . . . . . . . . . . . . 20 |- (N e. Met -> ((F"s) e. ran ( ball ` N) <-> E.w e. dom dom NE.r e. RR (0 < r /\ (F"s) = (w( ball ` N)r))))
156	155	ad2antlr 441	. . . . . . . . . . . . . . . . . . 19 |- (((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) -> ((F"s) e. ran ( ball ` N) <-> E.w e. dom dom NE.r e. RR (0 < r /\ (F"s) = (w( ball ` N)r))))
157	152, 154, 156	3imtr4d 602	. . . . . . . . . . . . . . . . . 18 |- (((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) -> (s e. ran ( ball ` M) -> (F"s) e. ran ( ball ` N)))
158	157	imp 377	. . . . . . . . . . . . . . . . 17 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ s e. ran ( ball ` M)) -> (F"s) e. ran ( ball ` N))
159	158	adantlr 429	. . . . . . . . . . . . . . . 16 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ u C_ dom dom M) /\ s e. ran ( ball ` M)) -> (F"s) e. ran ( ball ` N))
160	159	ad2antrr 440	. . . . . . . . . . . . . . 15 |- (((((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ u C_ dom dom M) /\ s e. ran ( ball ` M)) /\ (z e. s /\ s C_ u)) /\ (F` z) = w) -> (F"s) e. ran ( ball ` N))
161		eleq1 1957	. . . . . . . . . . . . . . . . 17 |- ((F` z) = w -> ((F` z) e. (F"s) <-> w e. (F"s)))
162	1	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((F:dom dom M-1-1-onto->dom dom N /\ s C_ dom dom M) -> Fun F)
163		fdm 4567	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (F:dom dom M-->dom dom N -> dom F = dom dom M)
164	8, 163	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (F:dom dom M-1-1-onto->dom dom N -> dom F = dom dom M)
165	164	sseq2d 2645	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (F:dom dom M-1-1-onto->dom dom N -> (s C_ dom F <-> s C_ dom dom M))
166	165	biimpar 461	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((F:dom dom M-1-1-onto->dom dom N /\ s C_ dom dom M) -> s C_ dom F)
167		funfvima2 4829	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((Fun F /\ s C_ dom F) -> (z e. s -> (F` z) e. (F"s)))
168	162, 166, 167	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F:dom dom M-1-1-onto->dom dom N /\ s C_ dom dom M) -> (z e. s -> (F` z) e. (F"s)))
169	168	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y))) /\ s C_ dom dom M) -> (z e. s -> (F` z) e. (F"s)))
170	169	adantll 428	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ s C_ dom dom M) -> (z e. s -> (F` z) e. (F"s)))
171		sstr 2625	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((s C_ u /\ u C_ dom dom M) -> s C_ dom dom M)
172	171	ancoms 484	. . . . . . . . . . . . . . . . . . . . . 22 |- ((u C_ dom dom M /\ s C_ u) -> s C_ dom dom M)
173	170, 172	sylan2 500	. . . . . . . . . . . . . . . . . . . . 21 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ (u C_ dom dom M /\ s C_ u)) -> (z e. s -> (F` z) e. (F"s)))
174	173	anassrs 489	. . . . . . . . . . . . . . . . . . . 20 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ u C_ dom dom M) /\ s C_ u) -> (z e. s -> (F` z) e. (F"s)))
175	174	adantlr 429	. . . . . . . . . . . . . . . . . . 19 |- ((((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ u C_ dom dom M) /\ s e. ran ( ball ` M)) /\ s C_ u) -> (z e. s -> (F` z) e. (F"s)))
176	175	impr 422	. . . . . . . . . . . . . . . . . 18 |- ((((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ u C_ dom dom M) /\ s e. ran ( ball ` M)) /\ (s C_ u /\ z e. s)) -> (F` z) e. (F"s))
177	176	ancom2s 545	. . . . . . . . . . . . . . . . 17 |- ((((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ u C_ dom dom M) /\ s e. ran ( ball ` M)) /\ (z e. s /\ s C_ u)) -> (F` z) e. (F"s))
178	161, 177	syl5cbi 226	. . . . . . . . . . . . . . . 16 |- ((((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ u C_ dom dom M) /\ s e. ran ( ball ` M)) /\ (z e. s /\ s C_ u)) -> ((F` z) = w -> w e. (F"s)))
179	178	imp 377	. . . . . . . . . . . . . . 15 |- (((((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ u C_ dom dom M) /\ s e. ran ( ball ` M)) /\ (z e. s /\ s C_ u)) /\ (F` z) = w) -> w e. (F"s))
180		imass2 4299	. . . . . . . . . . . . . . . . 17 |- (s C_ u -> (F"s) C_ (F"u))
181	180	adantl 424	. . . . . . . . . . . . . . . 16 |- ((z e. s /\ s C_ u) -> (F"s) C_ (F"u))
182	181	ad2antlr 441	. . . . . . . . . . . . . . 15 |- (((((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ u C_ dom dom M) /\ s e. ran ( ball ` M)) /\ (z e. s /\ s C_ u)) /\ (F` z) = w) -> (F"s) C_ (F"u))
183		eleq2 1958	. . . . . . . . . . . . . . . . 17 |- (t = (F"s) -> (w e. t <-> w e. (F"s)))
184		sseq1 2637	. . . . . . . . . . . . . . . . 17 |- (t = (F"s) -> (t C_ (F"u) <-> (F"s) C_ (F"u)))
185	183, 184	anbi12d 690	. . . . . . . . . . . . . . . 16 |- (t = (F"s) -> ((w e. t /\ t C_ (F"u)) <-> (w e. (F"s) /\ (F"s) C_ (F"u))))
186	185	rcla4ev 2381	. . . . . . . . . . . . . . 15 |- (((F"s) e. ran ( ball ` N) /\ (w e. (F"s) /\ (F"s) C_ (F"u))) -> E.t e. ran ( ball ` N)(w e. t /\ t C_ (F"u)))
187	160, 179, 182, 186	syl12anc 1098	. . . . . . . . . . . . . 14 |- (((((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ u C_ dom dom M) /\ s e. ran ( ball ` M)) /\ (z e. s /\ s C_ u)) /\ (F` z) = w) -> E.t e. ran ( ball ` N)(w e. t /\ t C_ (F"u)))
188	187	exp31 407	. . . . . . . . . . . . 13 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ u C_ dom dom M) /\ s e. ran ( ball ` M)) -> ((z e. s /\ s C_ u) -> ((F` z) = w -> E.t e. ran ( ball ` N)(w e. t /\ t C_ (F"u)))))
189	188	r19.23adva 2216	. . . . . . . . . . . 12 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ u C_ dom dom M) -> (E.s e. ran ( ball ` M)(z e. s /\ s C_ u) -> ((F` z) = w -> E.t e. ran ( ball ` N)(w e. t /\ t C_ (F"u)))))
190	189	imp 377	. . . . . . . . . . 11 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ u C_ dom dom M) /\ E.s e. ran ( ball ` M)(z e. s /\ s C_ u)) -> ((F` z) = w -> E.t e. ran ( ball ` N)(w e. t /\ t C_ (F"u))))
191		elequ1 1496	. . . . . . . . . . . . . 14 |- (v = z -> (v e. s <-> z e. s))
192	191	anbi1d 679	. . . . . . . . . . . . 13 |- (v = z -> ((v e. s /\ s C_ u) <-> (z e. s /\ s C_ u)))
193	192	rexbidv 2124	. . . . . . . . . . . 12 |- (v = z -> (E.s e. ran ( ball ` M)(v e. s /\ s C_ u) <-> E.s e. ran ( ball ` M)(z e. s /\ s C_ u)))
194	193	rcla4cva 2379	. . . . . . . . . . 11 |- ((A.v e. u E.s e. ran ( ball ` M)(v e. s /\ s C_ u) /\ z e. u) -> E.s e. ran ( ball ` M)(z e. s /\ s C_ u))
195	190, 194	sylan2 500	. . . . . . . . . 10 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ u C_ dom dom M) /\ (A.v e. u E.s e. ran ( ball ` M)(v e. s /\ s C_ u) /\ z e. u)) -> ((F` z) = w -> E.t e. ran ( ball ` N)(w e. t /\ t C_ (F"u))))
196	195	anassrs 489	. . . . . . . . 9 |- ((((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ u C_ dom dom M) /\ A.v e. u E.s e. ran ( ball ` M)(v e. s /\ s C_ u)) /\ z e. u) -> ((F` z) = w -> E.t e. ran ( ball ` N)(w e. t /\ t C_ (F"u))))
197	196	r19.23adva 2216	. . . . . . . 8 |- (((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ u C_ dom dom M) /\ A.v e. u E.s e. ran ( ball ` M)(v e. s /\ s C_ u)) -> (E.z e. u (F` z) = w -> E.t e. ran ( ball ` N)(w e. t /\ t C_ (F"u))))
198	197	anasss 488	. . . . . . 7 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ (u C_ dom dom M /\ A.v e. u E.s e. ran ( ball ` M)(v e. s /\ s C_ u))) -> (E.z e. u (F` z) = w -> E.t e. ran ( ball ` N)(w e. t /\ t C_ (F"u))))
199	6, 198	syld 30	. . . . . 6 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ (u C_ dom dom M /\ A.v e. u E.s e. ran ( ball ` M)(v e. s /\ s C_ u))) -> (w e. (F"u) -> E.t e. ran ( ball ` N)(w e. t /\ t C_ (F"u))))
200	199	r19.21aiv 2175	. . . . 5 |- ((((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) /\ (u C_ dom dom M /\ A.v e. u E.s e. ran ( ball ` M)(v e. s /\ s C_ u))) -> A.w e. (F"u)E.t e. ran ( ball ` N)(w e. t /\ t C_ (F"u)))
201	200	ex 402	. . . 4 |- (((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) -> ((u C_ dom dom M /\ A.v e. u E.s e. ran ( ball ` M)(v e. s /\ s C_ u)) -> A.w e. (F"u)E.t e. ran ( ball ` N)(w e. t /\ t C_ (F"u))))
202		f1ofo 4643	. . . . . 6 |- (F:dom dom M-1-1-onto->dom dom N -> F:dom dom M-onto->dom dom N)
203		forn 4620	. . . . . 6 |- (F:dom dom M-onto->dom dom N -> ran F = dom dom N)
204		imassrn 4278	. . . . . . 7 |- (F"u) C_ ran F
205		sseq2 2639	. . . . . . 7 |- (ran F = dom dom N -> ((F"u) C_ ran F <-> (F"u) C_ dom dom N))
206	204, 205	mpbii 210	. . . . . 6 |- (ran F = dom dom N -> (F"u) C_ dom dom N)
207	202, 203, 206	3syl 24	. . . . 5 |- (F:dom dom M-1-1-onto->dom dom N -> (F"u) C_ dom dom N)
208	207	ad2antrl 442	. . . 4 |- (((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) -> (F"u) C_ dom dom N)
209	201, 208	jctild 662	. . 3 |- (((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) -> ((u C_ dom dom M /\ A.v e. u E.s e. ran ( ball ` M)(v e. s /\ s C_ u)) -> ((F"u) C_ dom dom N /\ A.w e. (F"u)E.t e. ran ( ball ` N)(w e. t /\ t C_ (F"u)))))
210		ismtyhmeo.1	. . . . 5 |- J = (Open` M)
211	18, 210	isopn 9136	. . . 4 |- (M e. Met -> (u e. J <-> (u C_ dom dom M /\ A.v e. u E.s e. ran ( ball ` M)(v e. s /\ s C_ u))))
212	211	ad2antrr 440	. . 3 |- (((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) -> (u e. J <-> (u C_ dom dom M /\ A.v e. u E.s e. ran ( ball ` M)(v e. s /\ s C_ u))))
213		ismtyhmeo.2	. . . . 5 |- K = (Open` N)
214	131, 213	isopn 9136	. . . 4 |- (N e. Met -> ((F"u) e. K <-> ((F"u) C_ dom dom N /\ A.w e. (F"u)E.t e. ran ( ball ` N)(w e. t /\ t C_ (F"u)))))
215	214	ad2antlr 441	. . 3 |- (((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) -> ((F"u) e. K <-> ((F"u) C_ dom dom N /\ A.w e. (F"u)E.t e. ran ( ball ` N)(w e. t /\ t C_ (F"u)))))
216	209, 212, 215	3imtr4d 602	. 2 |- (((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) -> (u e. J -> (F"u) e. K))
217	216	r19.21aiv 2175	1 |- (((M e. Met /\ N e. Met) /\ (F:dom dom M-1-1-onto->dom dom N /\ A.x e. dom dom MA.y e. dom dom M(xMy) = ((F` x)N(F` y)))) -> A.u e. J (F"u) e. K)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106   C_ wss 2593   class class class wbr 3338  `'ccnv 3985  dom cdm 3986  ran crn 3987  "cima 3989  Fun wfun 3992   Fn wfn 3993  -->wf 3994  -onto->wfo 3996  -1-1-onto->wf1o 3997  ` cfv 3998  (class class class)co 4884  RRcr 6385  0cc0 6386   < clt 6653  Metcme 9066   ball cbl 9068  Opencopn 9069

This theorem is referenced by:  ismtyhmeo 15951

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  ax-inf2 5731

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-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-1st 5020  df-2nd 5021  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-enr 6318  df-nr 6319  df-0r 6323  df-c 6392  df-r 6396  df-bl 9072  df-opn 9073

Copyright terms: Public domain