Metamath Proof Explorer


Theorem imasf1oxmet

Description: The image of an extended metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses imasf1oxmet.u ⊒ ( πœ‘ β†’ π‘ˆ = ( 𝐹 β€œs 𝑅 ) )
imasf1oxmet.v ⊒ ( πœ‘ β†’ 𝑉 = ( Base β€˜ 𝑅 ) )
imasf1oxmet.f ⊒ ( πœ‘ β†’ 𝐹 : 𝑉 –1-1-ontoβ†’ 𝐡 )
imasf1oxmet.r ⊒ ( πœ‘ β†’ 𝑅 ∈ 𝑍 )
imasf1oxmet.e ⊒ 𝐸 = ( ( dist β€˜ 𝑅 ) β†Ύ ( 𝑉 Γ— 𝑉 ) )
imasf1oxmet.d ⊒ 𝐷 = ( dist β€˜ π‘ˆ )
imasf1oxmet.m ⊒ ( πœ‘ β†’ 𝐸 ∈ ( ∞Met β€˜ 𝑉 ) )
Assertion imasf1oxmet ( πœ‘ β†’ 𝐷 ∈ ( ∞Met β€˜ 𝐡 ) )

Proof

Step Hyp Ref Expression
1 imasf1oxmet.u ⊒ ( πœ‘ β†’ π‘ˆ = ( 𝐹 β€œs 𝑅 ) )
2 imasf1oxmet.v ⊒ ( πœ‘ β†’ 𝑉 = ( Base β€˜ 𝑅 ) )
3 imasf1oxmet.f ⊒ ( πœ‘ β†’ 𝐹 : 𝑉 –1-1-ontoβ†’ 𝐡 )
4 imasf1oxmet.r ⊒ ( πœ‘ β†’ 𝑅 ∈ 𝑍 )
5 imasf1oxmet.e ⊒ 𝐸 = ( ( dist β€˜ 𝑅 ) β†Ύ ( 𝑉 Γ— 𝑉 ) )
6 imasf1oxmet.d ⊒ 𝐷 = ( dist β€˜ π‘ˆ )
7 imasf1oxmet.m ⊒ ( πœ‘ β†’ 𝐸 ∈ ( ∞Met β€˜ 𝑉 ) )
8 f1ofo ⊒ ( 𝐹 : 𝑉 –1-1-ontoβ†’ 𝐡 β†’ 𝐹 : 𝑉 –ontoβ†’ 𝐡 )
9 3 8 syl ⊒ ( πœ‘ β†’ 𝐹 : 𝑉 –ontoβ†’ 𝐡 )
10 eqid ⊒ ( dist β€˜ 𝑅 ) = ( dist β€˜ 𝑅 )
11 1 2 9 4 10 6 imasdsfn ⊒ ( πœ‘ β†’ 𝐷 Fn ( 𝐡 Γ— 𝐡 ) )
12 1 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ π‘ˆ = ( 𝐹 β€œs 𝑅 ) )
13 2 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ 𝑉 = ( Base β€˜ 𝑅 ) )
14 3 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ 𝐹 : 𝑉 –1-1-ontoβ†’ 𝐡 )
15 4 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ 𝑅 ∈ 𝑍 )
16 7 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ 𝐸 ∈ ( ∞Met β€˜ 𝑉 ) )
17 simprl ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ π‘Ž ∈ 𝑉 )
18 simprr ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ 𝑏 ∈ 𝑉 )
19 12 13 14 15 5 6 16 17 18 imasdsf1o ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) = ( π‘Ž 𝐸 𝑏 ) )
20 xmetcl ⊒ ( ( 𝐸 ∈ ( ∞Met β€˜ 𝑉 ) ∧ π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) β†’ ( π‘Ž 𝐸 𝑏 ) ∈ ℝ* )
21 20 3expb ⊒ ( ( 𝐸 ∈ ( ∞Met β€˜ 𝑉 ) ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ ( π‘Ž 𝐸 𝑏 ) ∈ ℝ* )
22 7 21 sylan ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ ( π‘Ž 𝐸 𝑏 ) ∈ ℝ* )
23 19 22 eqeltrd ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ∈ ℝ* )
24 23 ralrimivva ⊒ ( πœ‘ β†’ βˆ€ π‘Ž ∈ 𝑉 βˆ€ 𝑏 ∈ 𝑉 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ∈ ℝ* )
25 f1ofn ⊒ ( 𝐹 : 𝑉 –1-1-ontoβ†’ 𝐡 β†’ 𝐹 Fn 𝑉 )
26 3 25 syl ⊒ ( πœ‘ β†’ 𝐹 Fn 𝑉 )
27 oveq2 ⊒ ( 𝑦 = ( 𝐹 β€˜ 𝑏 ) β†’ ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) )
28 27 eleq1d ⊒ ( 𝑦 = ( 𝐹 β€˜ 𝑏 ) β†’ ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ∈ ℝ* ↔ ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ∈ ℝ* ) )
29 28 ralrn ⊒ ( 𝐹 Fn 𝑉 β†’ ( βˆ€ 𝑦 ∈ ran 𝐹 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ∈ ℝ* ↔ βˆ€ 𝑏 ∈ 𝑉 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ∈ ℝ* ) )
30 26 29 syl ⊒ ( πœ‘ β†’ ( βˆ€ 𝑦 ∈ ran 𝐹 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ∈ ℝ* ↔ βˆ€ 𝑏 ∈ 𝑉 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ∈ ℝ* ) )
31 forn ⊒ ( 𝐹 : 𝑉 –ontoβ†’ 𝐡 β†’ ran 𝐹 = 𝐡 )
32 9 31 syl ⊒ ( πœ‘ β†’ ran 𝐹 = 𝐡 )
33 32 raleqdv ⊒ ( πœ‘ β†’ ( βˆ€ 𝑦 ∈ ran 𝐹 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ∈ ℝ* ↔ βˆ€ 𝑦 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ∈ ℝ* ) )
34 30 33 bitr3d ⊒ ( πœ‘ β†’ ( βˆ€ 𝑏 ∈ 𝑉 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ∈ ℝ* ↔ βˆ€ 𝑦 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ∈ ℝ* ) )
35 34 ralbidv ⊒ ( πœ‘ β†’ ( βˆ€ π‘Ž ∈ 𝑉 βˆ€ 𝑏 ∈ 𝑉 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ∈ ℝ* ↔ βˆ€ π‘Ž ∈ 𝑉 βˆ€ 𝑦 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ∈ ℝ* ) )
36 24 35 mpbid ⊒ ( πœ‘ β†’ βˆ€ π‘Ž ∈ 𝑉 βˆ€ 𝑦 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ∈ ℝ* )
37 oveq1 ⊒ ( π‘₯ = ( 𝐹 β€˜ π‘Ž ) β†’ ( π‘₯ 𝐷 𝑦 ) = ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) )
38 37 eleq1d ⊒ ( π‘₯ = ( 𝐹 β€˜ π‘Ž ) β†’ ( ( π‘₯ 𝐷 𝑦 ) ∈ ℝ* ↔ ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ∈ ℝ* ) )
39 38 ralbidv ⊒ ( π‘₯ = ( 𝐹 β€˜ π‘Ž ) β†’ ( βˆ€ 𝑦 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ∈ ℝ* ↔ βˆ€ 𝑦 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ∈ ℝ* ) )
40 39 ralrn ⊒ ( 𝐹 Fn 𝑉 β†’ ( βˆ€ π‘₯ ∈ ran 𝐹 βˆ€ 𝑦 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ∈ ℝ* ↔ βˆ€ π‘Ž ∈ 𝑉 βˆ€ 𝑦 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ∈ ℝ* ) )
41 26 40 syl ⊒ ( πœ‘ β†’ ( βˆ€ π‘₯ ∈ ran 𝐹 βˆ€ 𝑦 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ∈ ℝ* ↔ βˆ€ π‘Ž ∈ 𝑉 βˆ€ 𝑦 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ∈ ℝ* ) )
42 32 raleqdv ⊒ ( πœ‘ β†’ ( βˆ€ π‘₯ ∈ ran 𝐹 βˆ€ 𝑦 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ∈ ℝ* ↔ βˆ€ π‘₯ ∈ 𝐡 βˆ€ 𝑦 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ∈ ℝ* ) )
43 41 42 bitr3d ⊒ ( πœ‘ β†’ ( βˆ€ π‘Ž ∈ 𝑉 βˆ€ 𝑦 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ∈ ℝ* ↔ βˆ€ π‘₯ ∈ 𝐡 βˆ€ 𝑦 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ∈ ℝ* ) )
44 36 43 mpbid ⊒ ( πœ‘ β†’ βˆ€ π‘₯ ∈ 𝐡 βˆ€ 𝑦 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ∈ ℝ* )
45 ffnov ⊒ ( 𝐷 : ( 𝐡 Γ— 𝐡 ) ⟢ ℝ* ↔ ( 𝐷 Fn ( 𝐡 Γ— 𝐡 ) ∧ βˆ€ π‘₯ ∈ 𝐡 βˆ€ 𝑦 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ∈ ℝ* ) )
46 11 44 45 sylanbrc ⊒ ( πœ‘ β†’ 𝐷 : ( 𝐡 Γ— 𝐡 ) ⟢ ℝ* )
47 xmeteq0 ⊒ ( ( 𝐸 ∈ ( ∞Met β€˜ 𝑉 ) ∧ π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) β†’ ( ( π‘Ž 𝐸 𝑏 ) = 0 ↔ π‘Ž = 𝑏 ) )
48 16 17 18 47 syl3anc ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ ( ( π‘Ž 𝐸 𝑏 ) = 0 ↔ π‘Ž = 𝑏 ) )
49 19 eqeq1d ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) = 0 ↔ ( π‘Ž 𝐸 𝑏 ) = 0 ) )
50 f1of1 ⊒ ( 𝐹 : 𝑉 –1-1-ontoβ†’ 𝐡 β†’ 𝐹 : 𝑉 –1-1β†’ 𝐡 )
51 3 50 syl ⊒ ( πœ‘ β†’ 𝐹 : 𝑉 –1-1β†’ 𝐡 )
52 f1fveq ⊒ ( ( 𝐹 : 𝑉 –1-1β†’ 𝐡 ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ ( ( 𝐹 β€˜ π‘Ž ) = ( 𝐹 β€˜ 𝑏 ) ↔ π‘Ž = 𝑏 ) )
53 51 52 sylan ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ ( ( 𝐹 β€˜ π‘Ž ) = ( 𝐹 β€˜ 𝑏 ) ↔ π‘Ž = 𝑏 ) )
54 48 49 53 3bitr4d ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = ( 𝐹 β€˜ 𝑏 ) ) )
55 16 adantr ⊒ ( ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) β†’ 𝐸 ∈ ( ∞Met β€˜ 𝑉 ) )
56 simpr ⊒ ( ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) β†’ 𝑐 ∈ 𝑉 )
57 17 adantr ⊒ ( ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) β†’ π‘Ž ∈ 𝑉 )
58 18 adantr ⊒ ( ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) β†’ 𝑏 ∈ 𝑉 )
59 xmettri2 ⊒ ( ( 𝐸 ∈ ( ∞Met β€˜ 𝑉 ) ∧ ( 𝑐 ∈ 𝑉 ∧ π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ ( π‘Ž 𝐸 𝑏 ) ≀ ( ( 𝑐 𝐸 π‘Ž ) +𝑒 ( 𝑐 𝐸 𝑏 ) ) )
60 55 56 57 58 59 syl13anc ⊒ ( ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) β†’ ( π‘Ž 𝐸 𝑏 ) ≀ ( ( 𝑐 𝐸 π‘Ž ) +𝑒 ( 𝑐 𝐸 𝑏 ) ) )
61 19 adantr ⊒ ( ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) β†’ ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) = ( π‘Ž 𝐸 𝑏 ) )
62 12 adantr ⊒ ( ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) β†’ π‘ˆ = ( 𝐹 β€œs 𝑅 ) )
63 13 adantr ⊒ ( ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) β†’ 𝑉 = ( Base β€˜ 𝑅 ) )
64 14 adantr ⊒ ( ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) β†’ 𝐹 : 𝑉 –1-1-ontoβ†’ 𝐡 )
65 15 adantr ⊒ ( ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) β†’ 𝑅 ∈ 𝑍 )
66 62 63 64 65 5 6 55 56 57 imasdsf1o ⊒ ( ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) β†’ ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ π‘Ž ) ) = ( 𝑐 𝐸 π‘Ž ) )
67 62 63 64 65 5 6 55 56 58 imasdsf1o ⊒ ( ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) β†’ ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) = ( 𝑐 𝐸 𝑏 ) )
68 66 67 oveq12d ⊒ ( ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) β†’ ( ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) = ( ( 𝑐 𝐸 π‘Ž ) +𝑒 ( 𝑐 𝐸 𝑏 ) ) )
69 60 61 68 3brtr4d ⊒ ( ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑐 ∈ 𝑉 ) β†’ ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) )
70 69 ralrimiva ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ βˆ€ 𝑐 ∈ 𝑉 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) )
71 oveq1 ⊒ ( 𝑧 = ( 𝐹 β€˜ 𝑐 ) β†’ ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) = ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ π‘Ž ) ) )
72 oveq1 ⊒ ( 𝑧 = ( 𝐹 β€˜ 𝑐 ) β†’ ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) = ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) )
73 71 72 oveq12d ⊒ ( 𝑧 = ( 𝐹 β€˜ 𝑐 ) β†’ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) = ( ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) )
74 73 breq2d ⊒ ( 𝑧 = ( 𝐹 β€˜ 𝑐 ) β†’ ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ↔ ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ) )
75 74 ralrn ⊒ ( 𝐹 Fn 𝑉 β†’ ( βˆ€ 𝑧 ∈ ran 𝐹 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ↔ βˆ€ 𝑐 ∈ 𝑉 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ) )
76 26 75 syl ⊒ ( πœ‘ β†’ ( βˆ€ 𝑧 ∈ ran 𝐹 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ↔ βˆ€ 𝑐 ∈ 𝑉 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ) )
77 32 raleqdv ⊒ ( πœ‘ β†’ ( βˆ€ 𝑧 ∈ ran 𝐹 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ↔ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ) )
78 76 77 bitr3d ⊒ ( πœ‘ β†’ ( βˆ€ 𝑐 ∈ 𝑉 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ↔ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ) )
79 78 adantr ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ ( βˆ€ 𝑐 ∈ 𝑉 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( ( 𝐹 β€˜ 𝑐 ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ↔ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ) )
80 70 79 mpbid ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) )
81 54 80 jca ⊒ ( ( πœ‘ ∧ ( π‘Ž ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) β†’ ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = ( 𝐹 β€˜ 𝑏 ) ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ) )
82 81 ralrimivva ⊒ ( πœ‘ β†’ βˆ€ π‘Ž ∈ 𝑉 βˆ€ 𝑏 ∈ 𝑉 ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = ( 𝐹 β€˜ 𝑏 ) ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ) )
83 27 eqeq1d ⊒ ( 𝑦 = ( 𝐹 β€˜ 𝑏 ) β†’ ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = 0 ↔ ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) = 0 ) )
84 eqeq2 ⊒ ( 𝑦 = ( 𝐹 β€˜ 𝑏 ) β†’ ( ( 𝐹 β€˜ π‘Ž ) = 𝑦 ↔ ( 𝐹 β€˜ π‘Ž ) = ( 𝐹 β€˜ 𝑏 ) ) )
85 83 84 bibi12d ⊒ ( 𝑦 = ( 𝐹 β€˜ 𝑏 ) β†’ ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = 𝑦 ) ↔ ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = ( 𝐹 β€˜ 𝑏 ) ) ) )
86 oveq2 ⊒ ( 𝑦 = ( 𝐹 β€˜ 𝑏 ) β†’ ( 𝑧 𝐷 𝑦 ) = ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) )
87 86 oveq2d ⊒ ( 𝑦 = ( 𝐹 β€˜ 𝑏 ) β†’ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) )
88 27 87 breq12d ⊒ ( 𝑦 = ( 𝐹 β€˜ 𝑏 ) β†’ ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ↔ ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ) )
89 88 ralbidv ⊒ ( 𝑦 = ( 𝐹 β€˜ 𝑏 ) β†’ ( βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ↔ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ) )
90 85 89 anbi12d ⊒ ( 𝑦 = ( 𝐹 β€˜ 𝑏 ) β†’ ( ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = ( 𝐹 β€˜ 𝑏 ) ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ) ) )
91 90 ralrn ⊒ ( 𝐹 Fn 𝑉 β†’ ( βˆ€ 𝑦 ∈ ran 𝐹 ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ βˆ€ 𝑏 ∈ 𝑉 ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = ( 𝐹 β€˜ 𝑏 ) ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ) ) )
92 26 91 syl ⊒ ( πœ‘ β†’ ( βˆ€ 𝑦 ∈ ran 𝐹 ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ βˆ€ 𝑏 ∈ 𝑉 ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = ( 𝐹 β€˜ 𝑏 ) ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ) ) )
93 32 raleqdv ⊒ ( πœ‘ β†’ ( βˆ€ 𝑦 ∈ ran 𝐹 ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ βˆ€ 𝑦 ∈ 𝐡 ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
94 92 93 bitr3d ⊒ ( πœ‘ β†’ ( βˆ€ 𝑏 ∈ 𝑉 ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = ( 𝐹 β€˜ 𝑏 ) ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ) ↔ βˆ€ 𝑦 ∈ 𝐡 ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
95 94 ralbidv ⊒ ( πœ‘ β†’ ( βˆ€ π‘Ž ∈ 𝑉 βˆ€ 𝑏 ∈ 𝑉 ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = ( 𝐹 β€˜ 𝑏 ) ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 ( 𝐹 β€˜ 𝑏 ) ) ) ) ↔ βˆ€ π‘Ž ∈ 𝑉 βˆ€ 𝑦 ∈ 𝐡 ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
96 82 95 mpbid ⊒ ( πœ‘ β†’ βˆ€ π‘Ž ∈ 𝑉 βˆ€ 𝑦 ∈ 𝐡 ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
97 37 eqeq1d ⊒ ( π‘₯ = ( 𝐹 β€˜ π‘Ž ) β†’ ( ( π‘₯ 𝐷 𝑦 ) = 0 ↔ ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = 0 ) )
98 eqeq1 ⊒ ( π‘₯ = ( 𝐹 β€˜ π‘Ž ) β†’ ( π‘₯ = 𝑦 ↔ ( 𝐹 β€˜ π‘Ž ) = 𝑦 ) )
99 97 98 bibi12d ⊒ ( π‘₯ = ( 𝐹 β€˜ π‘Ž ) β†’ ( ( ( π‘₯ 𝐷 𝑦 ) = 0 ↔ π‘₯ = 𝑦 ) ↔ ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = 𝑦 ) ) )
100 oveq2 ⊒ ( π‘₯ = ( 𝐹 β€˜ π‘Ž ) β†’ ( 𝑧 𝐷 π‘₯ ) = ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) )
101 100 oveq1d ⊒ ( π‘₯ = ( 𝐹 β€˜ π‘Ž ) β†’ ( ( 𝑧 𝐷 π‘₯ ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
102 37 101 breq12d ⊒ ( π‘₯ = ( 𝐹 β€˜ π‘Ž ) β†’ ( ( π‘₯ 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 π‘₯ ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ↔ ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
103 102 ralbidv ⊒ ( π‘₯ = ( 𝐹 β€˜ π‘Ž ) β†’ ( βˆ€ 𝑧 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 π‘₯ ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ↔ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
104 99 103 anbi12d ⊒ ( π‘₯ = ( 𝐹 β€˜ π‘Ž ) β†’ ( ( ( ( π‘₯ 𝐷 𝑦 ) = 0 ↔ π‘₯ = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 π‘₯ ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
105 104 ralbidv ⊒ ( π‘₯ = ( 𝐹 β€˜ π‘Ž ) β†’ ( βˆ€ 𝑦 ∈ 𝐡 ( ( ( π‘₯ 𝐷 𝑦 ) = 0 ↔ π‘₯ = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 π‘₯ ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ βˆ€ 𝑦 ∈ 𝐡 ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
106 105 ralrn ⊒ ( 𝐹 Fn 𝑉 β†’ ( βˆ€ π‘₯ ∈ ran 𝐹 βˆ€ 𝑦 ∈ 𝐡 ( ( ( π‘₯ 𝐷 𝑦 ) = 0 ↔ π‘₯ = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 π‘₯ ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ βˆ€ π‘Ž ∈ 𝑉 βˆ€ 𝑦 ∈ 𝐡 ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
107 26 106 syl ⊒ ( πœ‘ β†’ ( βˆ€ π‘₯ ∈ ran 𝐹 βˆ€ 𝑦 ∈ 𝐡 ( ( ( π‘₯ 𝐷 𝑦 ) = 0 ↔ π‘₯ = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 π‘₯ ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ βˆ€ π‘Ž ∈ 𝑉 βˆ€ 𝑦 ∈ 𝐡 ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
108 32 raleqdv ⊒ ( πœ‘ β†’ ( βˆ€ π‘₯ ∈ ran 𝐹 βˆ€ 𝑦 ∈ 𝐡 ( ( ( π‘₯ 𝐷 𝑦 ) = 0 ↔ π‘₯ = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 π‘₯ ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ βˆ€ π‘₯ ∈ 𝐡 βˆ€ 𝑦 ∈ 𝐡 ( ( ( π‘₯ 𝐷 𝑦 ) = 0 ↔ π‘₯ = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 π‘₯ ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
109 107 108 bitr3d ⊒ ( πœ‘ β†’ ( βˆ€ π‘Ž ∈ 𝑉 βˆ€ 𝑦 ∈ 𝐡 ( ( ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) = 0 ↔ ( 𝐹 β€˜ π‘Ž ) = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( ( 𝐹 β€˜ π‘Ž ) 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 ( 𝐹 β€˜ π‘Ž ) ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ↔ βˆ€ π‘₯ ∈ 𝐡 βˆ€ 𝑦 ∈ 𝐡 ( ( ( π‘₯ 𝐷 𝑦 ) = 0 ↔ π‘₯ = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 π‘₯ ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) )
110 96 109 mpbid ⊒ ( πœ‘ β†’ βˆ€ π‘₯ ∈ 𝐡 βˆ€ 𝑦 ∈ 𝐡 ( ( ( π‘₯ 𝐷 𝑦 ) = 0 ↔ π‘₯ = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 π‘₯ ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
111 7 elfvexd ⊒ ( πœ‘ β†’ 𝑉 ∈ V )
112 fornex ⊒ ( 𝑉 ∈ V β†’ ( 𝐹 : 𝑉 –ontoβ†’ 𝐡 β†’ 𝐡 ∈ V ) )
113 111 9 112 sylc ⊒ ( πœ‘ β†’ 𝐡 ∈ V )
114 isxmet ⊒ ( 𝐡 ∈ V β†’ ( 𝐷 ∈ ( ∞Met β€˜ 𝐡 ) ↔ ( 𝐷 : ( 𝐡 Γ— 𝐡 ) ⟢ ℝ* ∧ βˆ€ π‘₯ ∈ 𝐡 βˆ€ 𝑦 ∈ 𝐡 ( ( ( π‘₯ 𝐷 𝑦 ) = 0 ↔ π‘₯ = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 π‘₯ ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
115 113 114 syl ⊒ ( πœ‘ β†’ ( 𝐷 ∈ ( ∞Met β€˜ 𝐡 ) ↔ ( 𝐷 : ( 𝐡 Γ— 𝐡 ) ⟢ ℝ* ∧ βˆ€ π‘₯ ∈ 𝐡 βˆ€ 𝑦 ∈ 𝐡 ( ( ( π‘₯ 𝐷 𝑦 ) = 0 ↔ π‘₯ = 𝑦 ) ∧ βˆ€ 𝑧 ∈ 𝐡 ( π‘₯ 𝐷 𝑦 ) ≀ ( ( 𝑧 𝐷 π‘₯ ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) ) ) )
116 46 110 115 mpbir2and ⊒ ( πœ‘ β†’ 𝐷 ∈ ( ∞Met β€˜ 𝐡 ) )