Theorem metcnplem 7869

Description: Lemma for metcnp 7870.

Hypotheses

Ref	Expression
metcn.1	|- X = dom dom C
metcn.2	|- J = (Open` C)
metcn.3	|- Y = dom dom D
metcn.4	|- K = (Open` D)

Assertion

Ref	Expression
metcnplem	|- (((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) -> (A.y e. RR (0 < y -> E.z e. RR (0 < z /\ (P( ball ` C)z) (_ (`'F"((F` P)( ball ` D)y)))) <-> A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((PCw) < z -> ((F` P)D(F` w)) < y)))))

Distinct variable groups:   y,w,z,F   w,C,y,z   w,D,y,z   w,X,y,z   w,Y,y,z   w,P,y,z   w,J,y,z   y,K

Proof of Theorem metcnplem

Step	Hyp	Ref	Expression
1		funimass5 3804	. . . . . . . . . 10 |- ((Fun F /\ (P( ball ` C)z) (_ dom F) -> ((P( ball ` C)z) (_ (`'F"((F` P)( ball ` D)y)) <-> A.w e. (P( ball ` C)z)(F` w) e. ((F` P)( ball ` D)y)))
2		ffun 3626	. . . . . . . . . . . 12 |- (F:X-->Y -> Fun F)
3	2	adantr 389	. . . . . . . . . . 11 |- ((F:X-->Y /\ P e. X) -> Fun F)
4	3	ad2antlr 405	. . . . . . . . . 10 |- ((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) -> Fun F)
5		metcn.1	. . . . . . . . . . . . 13 |- X = dom dom C
6	5	blssm 7832	. . . . . . . . . . . 12 |- (((C e. Met /\ P e. X) /\ (z e. RR /\ 0 < z)) -> (P( ball ` C)z) (_ X)
7		pm3.26 319	. . . . . . . . . . . . . 14 |- ((C e. Met /\ D e. Met) -> C e. Met)
8		pm3.27 323	. . . . . . . . . . . . . 14 |- ((F:X-->Y /\ P e. X) -> P e. X)
9	7, 8	anim12i 333	. . . . . . . . . . . . 13 |- (((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) -> (C e. Met /\ P e. X))
10	9	adantr 389	. . . . . . . . . . . 12 |- ((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) -> (C e. Met /\ P e. X))
11		simprr 415	. . . . . . . . . . . 12 |- ((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) -> (z e. RR /\ 0 < z))
12	6, 10, 11	sylanc 471	. . . . . . . . . . 11 |- ((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) -> (P( ball ` C)z) (_ X)
13		fdm 3628	. . . . . . . . . . . . 13 |- (F:X-->Y -> dom F = X)
14	13	adantr 389	. . . . . . . . . . . 12 |- ((F:X-->Y /\ P e. X) -> dom F = X)
15	14	ad2antlr 405	. . . . . . . . . . 11 |- ((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) -> dom F = X)
16	12, 15	sseqtr4d 2096	. . . . . . . . . 10 |- ((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) -> (P( ball ` C)z) (_ dom F)
17	1, 4, 16	sylanc 471	. . . . . . . . 9 |- ((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) -> ((P( ball ` C)z) (_ (`'F"((F` P)( ball ` D)y)) <-> A.w e. (P( ball ` C)z)(F` w) e. ((F` P)( ball ` D)y)))
18		ssel2 2062	. . . . . . . . . . . . . . 15 |- (((P( ball ` C)z) (_ X /\ w e. (P( ball ` C)z)) -> w e. X)
19	18, 12	sylan 448	. . . . . . . . . . . . . 14 |- (((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) /\ w e. (P( ball ` C)z)) -> w e. X)
20		biimt 730	. . . . . . . . . . . . . 14 |- (w e. X -> ((F` w) e. ((F` P)( ball ` D)y) <-> (w e. X -> (F` w) e. ((F` P)( ball ` D)y))))
21	19, 20	syl 10	. . . . . . . . . . . . 13 |- (((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) /\ w e. (P( ball ` C)z)) -> ((F` w) e. ((F` P)( ball ` D)y) <-> (w e. X -> (F` w) e. ((F` P)( ball ` D)y))))
22	21	pm5.74da 585	. . . . . . . . . . . 12 |- ((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) -> ((w e. (P( ball ` C)z) -> (F` w) e. ((F` P)( ball ` D)y)) <-> (w e. (P( ball ` C)z) -> (w e. X -> (F` w) e. ((F` P)( ball ` D)y)))))
23		bi2.04 160	. . . . . . . . . . . 12 |- ((w e. (P( ball ` C)z) -> (w e. X -> (F` w) e. ((F` P)( ball ` D)y))) <-> (w e. X -> (w e. (P( ball ` C)z) -> (F` w) e. ((F` P)( ball ` D)y))))
24	22, 23	syl6bb 535	. . . . . . . . . . 11 |- ((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) -> ((w e. (P( ball ` C)z) -> (F` w) e. ((F` P)( ball ` D)y)) <-> (w e. X -> (w e. (P( ball ` C)z) -> (F` w) e. ((F` P)( ball ` D)y)))))
25	5	elbl2 7820	. . . . . . . . . . . . . 14 |- (((C e. Met /\ P e. X /\ w e. X) /\ (z e. RR /\ 0 < z)) -> (w e. (P( ball ` C)z) <-> (PCw) < z))
26		simpll 412	. . . . . . . . . . . . . . . 16 |- (((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) -> C e. Met)
27	26	ad2antrr 404	. . . . . . . . . . . . . . 15 |- (((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) /\ w e. X) -> C e. Met)
28		simprr 415	. . . . . . . . . . . . . . . 16 |- (((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) -> P e. X)
29	28	ad2antrr 404	. . . . . . . . . . . . . . 15 |- (((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) /\ w e. X) -> P e. X)
30		pm3.27 323	. . . . . . . . . . . . . . 15 |- (((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) /\ w e. X) -> w e. X)
31	27, 29, 30	3jca 818	. . . . . . . . . . . . . 14 |- (((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) /\ w e. X) -> (C e. Met /\ P e. X /\ w e. X))
32	11	adantr 389	. . . . . . . . . . . . . 14 |- (((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) /\ w e. X) -> (z e. RR /\ 0 < z))
33	25, 31, 32	sylanc 471	. . . . . . . . . . . . 13 |- (((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) /\ w e. X) -> (w e. (P( ball ` C)z) <-> (PCw) < z))
34		metcn.3	. . . . . . . . . . . . . . 15 |- Y = dom dom D
35	34	elbl2 7820	. . . . . . . . . . . . . 14 |- (((D e. Met /\ (F` P) e. Y /\ (F` w) e. Y) /\ (y e. RR /\ 0 < y)) -> ((F` w) e. ((F` P)( ball ` D)y) <-> ((F` P)D(F` w)) < y))
36		simplr 413	. . . . . . . . . . . . . . . 16 |- (((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) -> D e. Met)
37	36	ad2antrr 404	. . . . . . . . . . . . . . 15 |- (((((C e. Met /\ D e. Met) /\ (F:X-->Y /\ P e. X)) /\ ((y e. RR /\ 0 < y) /\ (z e. RR /\ 0 < z))) /\ w e. X) -> D e. Met)
38		ffvelrn 3811	. . . . . . . . . . . . . . . . 17 |- ((F:X