Theorem bfplem2 38024

Description: Lemma for bfp 38025. Using the point found in bfplem1 38023, we show that this convergent point is a fixed point of 𝐹. Since for any positive 𝑥, the sequence 𝐺 is in 𝐵(𝑥 / 2, 𝑃) for all 𝑘 ∈ (ℤ_≥‘𝑗) (where 𝑃 = ((⇝_𝑡‘𝐽)‘𝐺)), we have 𝐷(𝐺(𝑗 + 1), 𝐹(𝑃)) ≤ 𝐷(𝐺(𝑗), 𝑃) < 𝑥 / 2 and 𝐷(𝐺(𝑗 + 1), 𝑃) < 𝑥 / 2, so 𝐹(𝑃) is in every neighborhood of 𝑃 and 𝑃 is a fixed point of 𝐹. (Contributed by Jeff Madsen, 5-Jun-2014.)

Hypotheses

Ref	Expression
bfp.2	⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
bfp.3	⊢ (𝜑 → 𝑋 ≠ ∅)
bfp.4	⊢ (𝜑 → 𝐾 ∈ ℝ+)
bfp.5	⊢ (𝜑 → 𝐾 < 1)
bfp.6	⊢ (𝜑 → 𝐹:𝑋⟶𝑋)
bfp.7	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)))
bfp.8	⊢ 𝐽 = (MetOpen‘𝐷)
bfp.9	⊢ (𝜑 → 𝐴 ∈ 𝑋)
bfp.10	⊢ 𝐺 = seq1((𝐹 ∘ 1st ), (ℕ × {𝐴}))

Assertion

Ref	Expression
bfplem2	⊢ (𝜑 → ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧)

Distinct variable groups:   𝑥,𝑦,𝑧,𝐷   𝑥,𝐺,𝑦,𝑧   𝑥,𝐽,𝑦,𝑧   𝜑,𝑥,𝑦   𝑥,𝐹,𝑦,𝑧   𝑥,𝐾,𝑦   𝑥,𝑋,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑧)   𝐴(𝑥,𝑦,𝑧)   𝐾(𝑧)

Proof of Theorem bfplem2

Dummy variables 𝑗 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bfp.2	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
2		cmetmet 25242	. . . . 5 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
3	1, 2	syl 17	. . . 4 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
4		metxmet 24278	. . . 4 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
5		bfp.8	. . . . 5 ⊢ 𝐽 = (MetOpen‘𝐷)
6	5	mopntopon 24383	. . . 4 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
7	3, 4, 6	3syl 18	. . 3 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
8		bfp.3	. . . 4 ⊢ (𝜑 → 𝑋 ≠ ∅)
9		bfp.4	. . . 4 ⊢ (𝜑 → 𝐾 ∈ ℝ+)
10		bfp.5	. . . 4 ⊢ (𝜑 → 𝐾 < 1)
11		bfp.6	. . . 4 ⊢ (𝜑 → 𝐹:𝑋⟶𝑋)
12		bfp.7	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)))
13		bfp.9	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
14		bfp.10	. . . 4 ⊢ 𝐺 = seq1((𝐹 ∘ 1st ), (ℕ × {𝐴}))
15	1, 8, 9, 10, 11, 12, 5, 13, 14	bfplem1 38023	. . 3 ⊢ (𝜑 → 𝐺(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐺))
16		lmcl 23241	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐺(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐺)) → ((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋)
17	7, 15, 16	syl2anc 584	. 2 ⊢ (𝜑 → ((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋)
18	3	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈ (Met‘𝑋))
19	18, 4	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈ (∞Met‘𝑋))
20		nnuz 12790	. . . . . . . . . 10 ⊢ ℕ = (ℤ≥‘1)
21		1zzd 12522	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℤ)
22		eqidd 2737	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) = (𝐺‘𝑘))
23	15	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐺(⇝𝑡‘𝐽)((⇝𝑡‘𝐽)‘𝐺))
24		rphalfcl 12934	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ+)
25	24	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ+)
26	5, 19, 20, 21, 22, 23, 25	lmmcvg 25217	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘) ∈ 𝑋 ∧ ((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)))
27		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝐺‘𝑘) ∈ 𝑋 ∧ ((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)) → ((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2))
28	27	ralimi 3073	. . . . . . . . . . 11 ⊢ (∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘) ∈ 𝑋 ∧ ((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)) → ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2))
29		nnz 12509	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℤ)
30	29	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℤ)
31		uzid 12766	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ ℤ → 𝑗 ∈ (ℤ≥‘𝑗))
32		fveq2 6834	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑗 → (𝐺‘𝑘) = (𝐺‘𝑗))
33	32	oveq1d 7373	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑗 → ((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) = ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)))
34	33	breq1d 5108	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑗 → (((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) ↔ ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)))
35	34	rspcv 3572	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ (ℤ≥‘𝑗) → (∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) → ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)))
36	30, 31, 35	3syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) → ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)))
37	30, 31	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ (ℤ≥‘𝑗))
38		peano2uz 12814	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (ℤ≥‘𝑗) → (𝑗 + 1) ∈ (ℤ≥‘𝑗))
39		fveq2 6834	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = (𝑗 + 1) → (𝐺‘𝑘) = (𝐺‘(𝑗 + 1)))
40	39	oveq1d 7373	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (𝑗 + 1) → ((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) = ((𝐺‘(𝑗 + 1))𝐷((⇝𝑡‘𝐽)‘𝐺)))
41	40	breq1d 5108	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝑗 + 1) → (((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) ↔ ((𝐺‘(𝑗 + 1))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)))
42	41	rspcv 3572	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 + 1) ∈ (ℤ≥‘𝑗) → (∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) → ((𝐺‘(𝑗 + 1))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)))
43	37, 38, 42	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) → ((𝐺‘(𝑗 + 1))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)))
44		1zzd 12522	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 1 ∈ ℤ)
45	20, 14, 44, 13, 11	algrp1 16501	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) = (𝐹‘(𝐺‘𝑗)))
46	45	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (𝐺‘(𝑗 + 1)) = (𝐹‘(𝐺‘𝑗)))
47	46	oveq1d 7373	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐺‘(𝑗 + 1))𝐷((⇝𝑡‘𝐽)‘𝐺)) = ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)))
48	47	breq1d 5108	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (((𝐺‘(𝑗 + 1))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) ↔ ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)))
49	43, 48	sylibd 239	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) → ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)))
50	36, 49	jcad 512	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) → (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) ∧ ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2))))
51	3	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 𝐷 ∈ (Met‘𝑋))
52	20, 14, 44, 13, 11	algrf 16500	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺:ℕ⟶𝑋)
53	52	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐺:ℕ⟶𝑋)
54	53	ffvelcdmda 7029	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (𝐺‘𝑗) ∈ 𝑋)
55	17	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋)
56		metcl 24276	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐺‘𝑗) ∈ 𝑋 ∧ ((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋) → ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ)
57	51, 54, 55, 56	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ)
58	11	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 𝐹:𝑋⟶𝑋)
59	58, 54	ffvelcdmd 7030	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (𝐹‘(𝐺‘𝑗)) ∈ 𝑋)
60		metcl 24276	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘(𝐺‘𝑗)) ∈ 𝑋 ∧ ((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋) → ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ)
61	51, 59, 55, 60	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ)
62		rpre 12914	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ)
63	62	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 𝑥 ∈ ℝ)
64		lt2halves 12376	. . . . . . . . . . . . 13 ⊢ ((((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ ∧ ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) ∧ ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)) → (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) < 𝑥))
65	57, 61, 63, 64	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) ∧ ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)) → (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) < 𝑥))
66	11, 17	ffvelcdmd 7030	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) ∈ 𝑋)
67		metcl 24276	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) ∈ 𝑋 ∧ ((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ)
68	3, 66, 17, 67	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ)
69	68	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ)
70	58, 55	ffvelcdmd 7030	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) ∈ 𝑋)
71		metcl 24276	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘(𝐺‘𝑗)) ∈ 𝑋 ∧ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) ∈ 𝑋) → ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) ∈ ℝ)
72	51, 59, 70, 71	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) ∈ ℝ)
73	72, 61	readdcld 11161	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) ∈ ℝ)
74	57, 61	readdcld 11161	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) ∈ ℝ)
75		mettri2 24285	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ ((𝐹‘(𝐺‘𝑗)) ∈ 𝑋 ∧ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) ∈ 𝑋 ∧ ((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋)) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))))
76	51, 59, 70, 55, 75	syl13anc 1374	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))))
77	9	rpred 12949	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ ℝ)
78	77	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 𝐾 ∈ ℝ)
79	78, 57	remulcld 11162	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (𝐾 · ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))) ∈ ℝ)
80	54, 55	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐺‘𝑗) ∈ 𝑋 ∧ ((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋))
81	12	ralrimivva 3179	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)))
82	81	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)))
83		fveq2 6834	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝐺‘𝑗) → (𝐹‘𝑥) = (𝐹‘(𝐺‘𝑗)))
84	83	oveq1d 7373	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝐺‘𝑗) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) = ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘𝑦)))
85		oveq1 7365	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝐺‘𝑗) → (𝑥𝐷𝑦) = ((𝐺‘𝑗)𝐷𝑦))
86	85	oveq2d 7374	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝐺‘𝑗) → (𝐾 · (𝑥𝐷𝑦)) = (𝐾 · ((𝐺‘𝑗)𝐷𝑦)))
87	84, 86	breq12d 5111	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝐺‘𝑗) → (((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)) ↔ ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘𝑦)) ≤ (𝐾 · ((𝐺‘𝑗)𝐷𝑦))))
88		fveq2 6834	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((⇝𝑡‘𝐽)‘𝐺) → (𝐹‘𝑦) = (𝐹‘((⇝𝑡‘𝐽)‘𝐺)))
89	88	oveq2d 7374	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((⇝𝑡‘𝐽)‘𝐺) → ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘𝑦)) = ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))))
90		oveq2 7366	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = ((⇝𝑡‘𝐽)‘𝐺) → ((𝐺‘𝑗)𝐷𝑦) = ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)))
91	90	oveq2d 7374	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = ((⇝𝑡‘𝐽)‘𝐺) → (𝐾 · ((𝐺‘𝑗)𝐷𝑦)) = (𝐾 · ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))))
92	89, 91	breq12d 5111	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = ((⇝𝑡‘𝐽)‘𝐺) → (((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘𝑦)) ≤ (𝐾 · ((𝐺‘𝑗)𝐷𝑦)) ↔ ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) ≤ (𝐾 · ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)))))
93	87, 92	rspc2v 3587	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺‘𝑗) ∈ 𝑋 ∧ ((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) ≤ (𝐾 · (𝑥𝐷𝑦)) → ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) ≤ (𝐾 · ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)))))
94	80, 82, 93	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) ≤ (𝐾 · ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))))
95		1red 11133	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 1 ∈ ℝ)
96		metge0 24289	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐺‘𝑗) ∈ 𝑋 ∧ ((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋) → 0 ≤ ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)))
97	51, 54, 55, 96	syl3anc 1373	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 0 ≤ ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)))
98		1re 11132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℝ
99		ltle 11221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐾 < 1 → 𝐾 ≤ 1))
100	77, 98, 99	sylancl 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐾 < 1 → 𝐾 ≤ 1))
101	10, 100	mpd 15	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ≤ 1)
102	101	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → 𝐾 ≤ 1)
103	78, 95, 57, 97, 102	lemul1ad 12081	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (𝐾 · ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))) ≤ (1 · ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))))
104	57	recnd 11160	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℂ)
105	104	mullidd 11150	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (1 · ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))) = ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)))
106	103, 105	breqtrd 5124	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (𝐾 · ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺))) ≤ ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)))
107	72, 79, 57, 94, 106	letrd 11290	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) ≤ ((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)))
108	72, 57, 61, 107	leadd1dd 11751	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (((𝐹‘(𝐺‘𝑗))𝐷(𝐹‘((⇝𝑡‘𝐽)‘𝐺))) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) ≤ (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))))
109	69, 73, 74, 76, 108	letrd 11290	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))))
110		lelttr 11223	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ ∧ (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) ∧ (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) < 𝑥) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥))
111	69, 74, 63, 110	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) ∧ (((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) < 𝑥) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥))
112	109, 111	mpand 695	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → ((((𝐺‘𝑗)𝐷((⇝𝑡‘𝐽)‘𝐺)) + ((𝐹‘(𝐺‘𝑗))𝐷((⇝𝑡‘𝐽)‘𝐺))) < 𝑥 → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥))
113	50, 65, 112	3syld 60	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥))
114	28, 113	syl5 34	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ ℕ) → (∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘) ∈ 𝑋 ∧ ((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥))
115	114	rexlimdva 3137	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐺‘𝑘) ∈ 𝑋 ∧ ((𝐺‘𝑘)𝐷((⇝𝑡‘𝐽)‘𝐺)) < (𝑥 / 2)) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥))
116	26, 115	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥)
117		ltle 11221	. . . . . . . . 9 ⊢ ((((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ ∧ 𝑥 ∈ ℝ) → (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥 → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ 𝑥))
118	68, 62, 117	syl2an 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) < 𝑥 → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ 𝑥))
119	116, 118	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ 𝑥)
120	62	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
121	120	recnd 11160	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
122	121	addlidd 11334	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (0 + 𝑥) = 𝑥)
123	119, 122	breqtrrd 5126	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (0 + 𝑥))
124	123	ralrimiva 3128	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (0 + 𝑥))
125		0re 11134	. . . . . 6 ⊢ 0 ∈ ℝ
126		alrple 13121	. . . . . 6 ⊢ ((((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ ∧ 0 ∈ ℝ) → (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ 0 ↔ ∀𝑥 ∈ ℝ+ ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (0 + 𝑥)))
127	68, 125, 126	sylancl 586	. . . . 5 ⊢ (𝜑 → (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ 0 ↔ ∀𝑥 ∈ ℝ+ ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ (0 + 𝑥)))
128	124, 127	mpbird 257	. . . 4 ⊢ (𝜑 → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ 0)
129		metge0 24289	. . . . 5 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) ∈ 𝑋 ∧ ((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋) → 0 ≤ ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)))
130	3, 66, 17, 129	syl3anc 1373	. . . 4 ⊢ (𝜑 → 0 ≤ ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)))
131		letri3 11218	. . . . 5 ⊢ ((((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ∈ ℝ ∧ 0 ∈ ℝ) → (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) = 0 ↔ (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ 0 ∧ 0 ≤ ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)))))
132	68, 125, 131	sylancl 586	. . . 4 ⊢ (𝜑 → (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) = 0 ↔ (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) ≤ 0 ∧ 0 ≤ ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)))))
133	128, 130, 132	mpbir2and 713	. . 3 ⊢ (𝜑 → ((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) = 0)
134		meteq0 24283	. . . 4 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) ∈ 𝑋 ∧ ((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋) → (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) = 0 ↔ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) = ((⇝𝑡‘𝐽)‘𝐺)))
135	3, 66, 17, 134	syl3anc 1373	. . 3 ⊢ (𝜑 → (((𝐹‘((⇝𝑡‘𝐽)‘𝐺))𝐷((⇝𝑡‘𝐽)‘𝐺)) = 0 ↔ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) = ((⇝𝑡‘𝐽)‘𝐺)))
136	133, 135	mpbid 232	. 2 ⊢ (𝜑 → (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) = ((⇝𝑡‘𝐽)‘𝐺))
137		fveq2 6834	. . . 4 ⊢ (𝑧 = ((⇝𝑡‘𝐽)‘𝐺) → (𝐹‘𝑧) = (𝐹‘((⇝𝑡‘𝐽)‘𝐺)))
138		id 22	. . . 4 ⊢ (𝑧 = ((⇝𝑡‘𝐽)‘𝐺) → 𝑧 = ((⇝𝑡‘𝐽)‘𝐺))
139	137, 138	eqeq12d 2752	. . 3 ⊢ (𝑧 = ((⇝𝑡‘𝐽)‘𝐺) → ((𝐹‘𝑧) = 𝑧 ↔ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) = ((⇝𝑡‘𝐽)‘𝐺)))
140	139	rspcev 3576	. 2 ⊢ ((((⇝𝑡‘𝐽)‘𝐺) ∈ 𝑋 ∧ (𝐹‘((⇝𝑡‘𝐽)‘𝐺)) = ((⇝𝑡‘𝐽)‘𝐺)) → ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧)
141	17, 136, 140	syl2anc 584	1 ⊢ (𝜑 → ∃𝑧 ∈ 𝑋 (𝐹‘𝑧) = 𝑧)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ≠ wne 2932  ∀wral 3051  ∃wrex 3060  ∅c0 4285  {csn 4580   class class class wbr 5098   × cxp 5622   ∘ ccom 5628  ⟶wf 6488  ‘cfv 6492  (class class class)co 7358  1^st c1st 7931  ℝcr 11025  0cc0 11026  1c1 11027   + caddc 11029   · cmul 11031   < clt 11166   ≤ cle 11167   / cdiv 11794  ℕcn 12145  2c2 12200  ℤcz 12488  ℤ_≥cuz 12751  ℝ⁺crp 12905  seqcseq 13924  ∞Metcxmet 21294  Metcmet 21295  MetOpencmopn 21299  TopOnctopon 22854  ⇝_𝑡clm 23170  CMetccmet 25210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-inf2 9550  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103  ax-pre-sup 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-int 4903  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-se 5578  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-1o 8397  df-er 8635  df-map 8765  df-pm 8766  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9345  df-inf 9346  df-oi 9415  df-card 9851  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-div 11795  df-nn 12146  df-2 12208  df-3 12209  df-n0 12402  df-z 12489  df-uz 12752  df-q 12862  df-rp 12906  df-xneg 13026  df-xadd 13027  df-xmul 13028  df-ico 13267  df-icc 13268  df-fz 13424  df-fzo 13571  df-fl 13712  df-seq 13925  df-exp 13985  df-hash 14254  df-cj 15022  df-re 15023  df-im 15024  df-sqrt 15158  df-abs 15159  df-clim 15411  df-rlim 15412  df-sum 15610  df-rest 17342  df-topgen 17363  df-psmet 21301  df-xmet 21302  df-met 21303  df-bl 21304  df-mopn 21305  df-fbas 21306  df-fg 21307  df-top 22838  df-topon 22855  df-bases 22890  df-ntr 22964  df-nei 23042  df-lm 23173  df-haus 23259  df-fil 23790  df-fm 23882  df-flim 23883  df-flf 23884  df-cfil 25211  df-cau 25212  df-cmet 25213

This theorem is referenced by:  bfp  38025