bfplem2

Description: Lemma for bfp . Using the point found in bfplem1 , we show that this convergent point is a fixed point of F . Since for any positive x , the sequence G is in B ( x / 2 , P ) for all k e. ( ZZ>=j ) (where P = ( ( ~>tJ )G ) ), we have D ( G ( j + 1 ) , F ( P ) ) <_ D ( G ( j ) , P ) < x / 2 and D ( G ( j + 1 ) , P ) < x / 2 , so F ( P ) is in every neighborhood of P and P is a fixed point of F . (Contributed by Jeff Madsen, 5-Jun-2014)

	Ref	Expression
Hypotheses	bfp.2	$⊢ φ \to D \in CMet (X)$
	bfp.3	$⊢ φ \to X \neq \emptyset$
	bfp.4	$⊢ φ \to K \in ℝ^{+}$
	bfp.5	$⊢ φ \to K < 1$
	bfp.6	$⊢ φ \to F : X ⟶ X$
	bfp.7	$⊢ (φ \land (x \in X \land y \in X)) \to F (x) D F (y) \leq K (x D y)$
	bfp.8	$⊢ J = MetOpen (D)$
	bfp.9	$⊢ φ \to A \in X$
	bfp.10	$⊢ G = seq 1 ((F \circ 1^{st}), (ℕ \times \{A\}))$
Assertion	bfplem2	$⊢ φ \to \exists z \in X F (z) = z$

Proof

Step	Hyp	Ref	Expression
1		bfp.2	$⊢ φ \to D \in CMet (X)$
2		bfp.3	$⊢ φ \to X \neq \emptyset$
3		bfp.4	$⊢ φ \to K \in ℝ^{+}$
4		bfp.5	$⊢ φ \to K < 1$
5		bfp.6	$⊢ φ \to F : X ⟶ X$
6		bfp.7	$⊢ (φ \land (x \in X \land y \in X)) \to F (x) D F (y) \leq K (x D y)$
7		bfp.8	$⊢ J = MetOpen (D)$
8		bfp.9	$⊢ φ \to A \in X$
9		bfp.10	$⊢ G = seq 1 ((F \circ 1^{st}), (ℕ \times \{A\}))$
10		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
11	1 10	syl	$⊢ φ \to D \in Met (X)$
12		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
13	7	mopntopon	$⊢ D \in ∞Met (X) \to J \in TopOn (X)$
14	11 12 13	3syl	$⊢ φ \to J \in TopOn (X)$
15	1 2 3 4 5 6 7 8 9	bfplem1	$⊢ φ \to G \underset{t}{⇝} (J) \underset{t}{⇝} (J) (G)$
16		lmcl	$⊢ (J \in TopOn (X) \land G \underset{t}{⇝} (J) \underset{t}{⇝} (J) (G)) \to \underset{t}{⇝} (J) (G) \in X$
17	14 15 16	syl2anc	$⊢ φ \to \underset{t}{⇝} (J) (G) \in X$
18	11	adantr	$⊢ (φ \land x \in ℝ^{+}) \to D \in Met (X)$
19	18 12	syl	$⊢ (φ \land x \in ℝ^{+}) \to D \in ∞Met (X)$
20		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
21		1zzd	$⊢ (φ \land x \in ℝ^{+}) \to 1 \in ℤ$
22		eqidd	$⊢ ((φ \land x \in ℝ^{+}) \land k \in ℕ) \to G (k) = G (k)$
23	15	adantr	$⊢ (φ \land x \in ℝ^{+}) \to G \underset{t}{⇝} (J) \underset{t}{⇝} (J) (G)$
24		rphalfcl	$⊢ x \in ℝ^{+} \to \frac{x}{2} \in ℝ^{+}$
25	24	adantl	$⊢ (φ \land x \in ℝ^{+}) \to \frac{x}{2} \in ℝ^{+}$
26	7 19 20 21 22 23 25	lmmcvg	$⊢ (φ \land x \in ℝ^{+}) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} (G (k) \in X \land G (k) D \underset{t}{⇝} (J) (G) < \frac{x}{2})$
27		simpr	$⊢ (G (k) \in X \land G (k) D \underset{t}{⇝} (J) (G) < \frac{x}{2}) \to G (k) D \underset{t}{⇝} (J) (G) < \frac{x}{2}$
28	27	ralimi	$⊢ \forall k \in ℤ_{\geq j} (G (k) \in X \land G (k) D \underset{t}{⇝} (J) (G) < \frac{x}{2}) \to \forall k \in ℤ_{\geq j} G (k) D \underset{t}{⇝} (J) (G) < \frac{x}{2}$
29		nnz	$⊢ j \in ℕ \to j \in ℤ$
30	29	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to j \in ℤ$
31		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
32		fveq2	$⊢ k = j \to G (k) = G (j)$
33	32	oveq1d	$⊢ k = j \to G (k) D \underset{t}{⇝} (J) (G) = G (j) D \underset{t}{⇝} (J) (G)$
34	33	breq1d	$⊢ k = j \to (G (k) D \underset{t}{⇝} (J) (G) < \frac{x}{2} \leftrightarrow G (j) D \underset{t}{⇝} (J) (G) < \frac{x}{2})$
35	34	rspcv	$⊢ j \in ℤ_{\geq j} \to (\forall k \in ℤ_{\geq j} G (k) D \underset{t}{⇝} (J) (G) < \frac{x}{2} \to G (j) D \underset{t}{⇝} (J) (G) < \frac{x}{2})$
36	30 31 35	3syl	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to (\forall k \in ℤ_{\geq j} G (k) D \underset{t}{⇝} (J) (G) < \frac{x}{2} \to G (j) D \underset{t}{⇝} (J) (G) < \frac{x}{2})$
37	30 31	syl	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to j \in ℤ_{\geq j}$
38		peano2uz	$⊢ j \in ℤ_{\geq j} \to j + 1 \in ℤ_{\geq j}$
39		fveq2	$⊢ k = j + 1 \to G (k) = G (j + 1)$
40	39	oveq1d	$⊢ k = j + 1 \to G (k) D \underset{t}{⇝} (J) (G) = G (j + 1) D \underset{t}{⇝} (J) (G)$
41	40	breq1d	$⊢ k = j + 1 \to (G (k) D \underset{t}{⇝} (J) (G) < \frac{x}{2} \leftrightarrow G (j + 1) D \underset{t}{⇝} (J) (G) < \frac{x}{2})$
42	41	rspcv	$⊢ j + 1 \in ℤ_{\geq j} \to (\forall k \in ℤ_{\geq j} G (k) D \underset{t}{⇝} (J) (G) < \frac{x}{2} \to G (j + 1) D \underset{t}{⇝} (J) (G) < \frac{x}{2})$
43	37 38 42	3syl	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to (\forall k \in ℤ_{\geq j} G (k) D \underset{t}{⇝} (J) (G) < \frac{x}{2} \to G (j + 1) D \underset{t}{⇝} (J) (G) < \frac{x}{2})$
44		1zzd	$⊢ φ \to 1 \in ℤ$
45	20 9 44 8 5	algrp1	$⊢ (φ \land j \in ℕ) \to G (j + 1) = F (G (j))$
46	45	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to G (j + 1) = F (G (j))$
47	46	oveq1d	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to G (j + 1) D \underset{t}{⇝} (J) (G) = F (G (j)) D \underset{t}{⇝} (J) (G)$
48	47	breq1d	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to (G (j + 1) D \underset{t}{⇝} (J) (G) < \frac{x}{2} \leftrightarrow F (G (j)) D \underset{t}{⇝} (J) (G) < \frac{x}{2})$
49	43 48	sylibd	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to (\forall k \in ℤ_{\geq j} G (k) D \underset{t}{⇝} (J) (G) < \frac{x}{2} \to F (G (j)) D \underset{t}{⇝} (J) (G) < \frac{x}{2})$
50	36 49	jcad	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to (\forall k \in ℤ_{\geq j} G (k) D \underset{t}{⇝} (J) (G) < \frac{x}{2} \to (G (j) D \underset{t}{⇝} (J) (G) < \frac{x}{2} \land F (G (j)) D \underset{t}{⇝} (J) (G) < \frac{x}{2}))$
51	11	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to D \in Met (X)$
52	20 9 44 8 5	algrf	$⊢ φ \to G : ℕ ⟶ X$
53	52	adantr	$⊢ (φ \land x \in ℝ^{+}) \to G : ℕ ⟶ X$
54	53	ffvelcdmda	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to G (j) \in X$
55	17	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to \underset{t}{⇝} (J) (G) \in X$
56		metcl	$⊢ (D \in Met (X) \land G (j) \in X \land \underset{t}{⇝} (J) (G) \in X) \to G (j) D \underset{t}{⇝} (J) (G) \in ℝ$
57	51 54 55 56	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to G (j) D \underset{t}{⇝} (J) (G) \in ℝ$
58	5	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to F : X ⟶ X$
59	58 54	ffvelcdmd	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to F (G (j)) \in X$
60		metcl	$⊢ (D \in Met (X) \land F (G (j)) \in X \land \underset{t}{⇝} (J) (G) \in X) \to F (G (j)) D \underset{t}{⇝} (J) (G) \in ℝ$
61	51 59 55 60	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to F (G (j)) D \underset{t}{⇝} (J) (G) \in ℝ$
62		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
63	62	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to x \in ℝ$
64		lt2halves	$⊢ (G (j) D \underset{t}{⇝} (J) (G) \in ℝ \land F (G (j)) D \underset{t}{⇝} (J) (G) \in ℝ \land x \in ℝ) \to ((G (j) D \underset{t}{⇝} (J) (G) < \frac{x}{2} \land F (G (j)) D \underset{t}{⇝} (J) (G) < \frac{x}{2}) \to (G (j) D \underset{t}{⇝} (J) (G)) + (F (G (j)) D \underset{t}{⇝} (J) (G)) < x)$
65	57 61 63 64	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to ((G (j) D \underset{t}{⇝} (J) (G) < \frac{x}{2} \land F (G (j)) D \underset{t}{⇝} (J) (G) < \frac{x}{2}) \to (G (j) D \underset{t}{⇝} (J) (G)) + (F (G (j)) D \underset{t}{⇝} (J) (G)) < x)$
66	5 17	ffvelcdmd	$⊢ φ \to F (\underset{t}{⇝} (J) (G)) \in X$
67		metcl	$⊢ (D \in Met (X) \land F (\underset{t}{⇝} (J) (G)) \in X \land \underset{t}{⇝} (J) (G) \in X) \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \in ℝ$
68	11 66 17 67	syl3anc	$⊢ φ \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \in ℝ$
69	68	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \in ℝ$
70	58 55	ffvelcdmd	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to F (\underset{t}{⇝} (J) (G)) \in X$
71		metcl	$⊢ (D \in Met (X) \land F (G (j)) \in X \land F (\underset{t}{⇝} (J) (G)) \in X) \to F (G (j)) D F (\underset{t}{⇝} (J) (G)) \in ℝ$
72	51 59 70 71	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to F (G (j)) D F (\underset{t}{⇝} (J) (G)) \in ℝ$
73	72 61	readdcld	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to (F (G (j)) D F (\underset{t}{⇝} (J) (G))) + (F (G (j)) D \underset{t}{⇝} (J) (G)) \in ℝ$
74	57 61	readdcld	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to (G (j) D \underset{t}{⇝} (J) (G)) + (F (G (j)) D \underset{t}{⇝} (J) (G)) \in ℝ$
75		mettri2	$⊢ (D \in Met (X) \land (F (G (j)) \in X \land F (\underset{t}{⇝} (J) (G)) \in X \land \underset{t}{⇝} (J) (G) \in X)) \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \leq (F (G (j)) D F (\underset{t}{⇝} (J) (G))) + (F (G (j)) D \underset{t}{⇝} (J) (G))$
76	51 59 70 55 75	syl13anc	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \leq (F (G (j)) D F (\underset{t}{⇝} (J) (G))) + (F (G (j)) D \underset{t}{⇝} (J) (G))$
77	3	rpred	$⊢ φ \to K \in ℝ$
78	77	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to K \in ℝ$
79	78 57	remulcld	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to K (G (j) D \underset{t}{⇝} (J) (G)) \in ℝ$
80	54 55	jca	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to (G (j) \in X \land \underset{t}{⇝} (J) (G) \in X)$
81	6	ralrimivva	$⊢ φ \to \forall x \in X \forall y \in X F (x) D F (y) \leq K (x D y)$
82	81	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to \forall x \in X \forall y \in X F (x) D F (y) \leq K (x D y)$
83		fveq2	$⊢ x = G (j) \to F (x) = F (G (j))$
84	83	oveq1d	$⊢ x = G (j) \to F (x) D F (y) = F (G (j)) D F (y)$
85		oveq1	$⊢ x = G (j) \to x D y = G (j) D y$
86	85	oveq2d	$⊢ x = G (j) \to K (x D y) = K (G (j) D y)$
87	84 86	breq12d	$⊢ x = G (j) \to (F (x) D F (y) \leq K (x D y) \leftrightarrow F (G (j)) D F (y) \leq K (G (j) D y))$
88		fveq2	$⊢ y = \underset{t}{⇝} (J) (G) \to F (y) = F (\underset{t}{⇝} (J) (G))$
89	88	oveq2d	$⊢ y = \underset{t}{⇝} (J) (G) \to F (G (j)) D F (y) = F (G (j)) D F (\underset{t}{⇝} (J) (G))$
90		oveq2	$⊢ y = \underset{t}{⇝} (J) (G) \to G (j) D y = G (j) D \underset{t}{⇝} (J) (G)$
91	90	oveq2d	$⊢ y = \underset{t}{⇝} (J) (G) \to K (G (j) D y) = K (G (j) D \underset{t}{⇝} (J) (G))$
92	89 91	breq12d	$⊢ y = \underset{t}{⇝} (J) (G) \to (F (G (j)) D F (y) \leq K (G (j) D y) \leftrightarrow F (G (j)) D F (\underset{t}{⇝} (J) (G)) \leq K (G (j) D \underset{t}{⇝} (J) (G)))$
93	87 92	rspc2v	$⊢ (G (j) \in X \land \underset{t}{⇝} (J) (G) \in X) \to (\forall x \in X \forall y \in X F (x) D F (y) \leq K (x D y) \to F (G (j)) D F (\underset{t}{⇝} (J) (G)) \leq K (G (j) D \underset{t}{⇝} (J) (G)))$
94	80 82 93	sylc	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to F (G (j)) D F (\underset{t}{⇝} (J) (G)) \leq K (G (j) D \underset{t}{⇝} (J) (G))$
95		1red	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to 1 \in ℝ$
96		metge0	$⊢ (D \in Met (X) \land G (j) \in X \land \underset{t}{⇝} (J) (G) \in X) \to 0 \leq G (j) D \underset{t}{⇝} (J) (G)$
97	51 54 55 96	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to 0 \leq G (j) D \underset{t}{⇝} (J) (G)$
98		1re	$⊢ 1 \in ℝ$
99		ltle	$⊢ (K \in ℝ \land 1 \in ℝ) \to (K < 1 \to K \leq 1)$
100	77 98 99	sylancl	$⊢ φ \to (K < 1 \to K \leq 1)$
101	4 100	mpd	$⊢ φ \to K \leq 1$
102	101	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to K \leq 1$
103	78 95 57 97 102	lemul1ad	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to K (G (j) D \underset{t}{⇝} (J) (G)) \leq 1 (G (j) D \underset{t}{⇝} (J) (G))$
104	57	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to G (j) D \underset{t}{⇝} (J) (G) \in ℂ$
105	104	mullidd	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to 1 (G (j) D \underset{t}{⇝} (J) (G)) = G (j) D \underset{t}{⇝} (J) (G)$
106	103 105	breqtrd	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to K (G (j) D \underset{t}{⇝} (J) (G)) \leq G (j) D \underset{t}{⇝} (J) (G)$
107	72 79 57 94 106	letrd	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to F (G (j)) D F (\underset{t}{⇝} (J) (G)) \leq G (j) D \underset{t}{⇝} (J) (G)$
108	72 57 61 107	leadd1dd	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to (F (G (j)) D F (\underset{t}{⇝} (J) (G))) + (F (G (j)) D \underset{t}{⇝} (J) (G)) \leq (G (j) D \underset{t}{⇝} (J) (G)) + (F (G (j)) D \underset{t}{⇝} (J) (G))$
109	69 73 74 76 108	letrd	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \leq (G (j) D \underset{t}{⇝} (J) (G)) + (F (G (j)) D \underset{t}{⇝} (J) (G))$
110		lelttr	$⊢ (F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \in ℝ \land (G (j) D \underset{t}{⇝} (J) (G)) + (F (G (j)) D \underset{t}{⇝} (J) (G)) \in ℝ \land x \in ℝ) \to ((F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \leq (G (j) D \underset{t}{⇝} (J) (G)) + (F (G (j)) D \underset{t}{⇝} (J) (G)) \land (G (j) D \underset{t}{⇝} (J) (G)) + (F (G (j)) D \underset{t}{⇝} (J) (G)) < x) \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) < x)$
111	69 74 63 110	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to ((F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \leq (G (j) D \underset{t}{⇝} (J) (G)) + (F (G (j)) D \underset{t}{⇝} (J) (G)) \land (G (j) D \underset{t}{⇝} (J) (G)) + (F (G (j)) D \underset{t}{⇝} (J) (G)) < x) \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) < x)$
112	109 111	mpand	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to ((G (j) D \underset{t}{⇝} (J) (G)) + (F (G (j)) D \underset{t}{⇝} (J) (G)) < x \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) < x)$
113	50 65 112	3syld	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to (\forall k \in ℤ_{\geq j} G (k) D \underset{t}{⇝} (J) (G) < \frac{x}{2} \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) < x)$
114	28 113	syl5	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℕ) \to (\forall k \in ℤ_{\geq j} (G (k) \in X \land G (k) D \underset{t}{⇝} (J) (G) < \frac{x}{2}) \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) < x)$
115	114	rexlimdva	$⊢ (φ \land x \in ℝ^{+}) \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} (G (k) \in X \land G (k) D \underset{t}{⇝} (J) (G) < \frac{x}{2}) \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) < x)$
116	26 115	mpd	$⊢ (φ \land x \in ℝ^{+}) \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) < x$
117		ltle	$⊢ (F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \in ℝ \land x \in ℝ) \to (F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) < x \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \leq x)$
118	68 62 117	syl2an	$⊢ (φ \land x \in ℝ^{+}) \to (F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) < x \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \leq x)$
119	116 118	mpd	$⊢ (φ \land x \in ℝ^{+}) \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \leq x$
120	62	adantl	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ$
121	120	recnd	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℂ$
122	121	addlidd	$⊢ (φ \land x \in ℝ^{+}) \to 0 + x = x$
123	119 122	breqtrrd	$⊢ (φ \land x \in ℝ^{+}) \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \leq 0 + x$
124	123	ralrimiva	$⊢ φ \to \forall x \in ℝ^{+} F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \leq 0 + x$
125		0re	$⊢ 0 \in ℝ$
126		alrple	$⊢ (F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \in ℝ \land 0 \in ℝ) \to (F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \leq 0 \leftrightarrow \forall x \in ℝ^{+} F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \leq 0 + x)$
127	68 125 126	sylancl	$⊢ φ \to (F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \leq 0 \leftrightarrow \forall x \in ℝ^{+} F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \leq 0 + x)$
128	124 127	mpbird	$⊢ φ \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \leq 0$
129		metge0	$⊢ (D \in Met (X) \land F (\underset{t}{⇝} (J) (G)) \in X \land \underset{t}{⇝} (J) (G) \in X) \to 0 \leq F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G)$
130	11 66 17 129	syl3anc	$⊢ φ \to 0 \leq F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G)$
131		letri3	$⊢ (F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \in ℝ \land 0 \in ℝ) \to (F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) = 0 \leftrightarrow (F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \leq 0 \land 0 \leq F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G)))$
132	68 125 131	sylancl	$⊢ φ \to (F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) = 0 \leftrightarrow (F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) \leq 0 \land 0 \leq F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G)))$
133	128 130 132	mpbir2and	$⊢ φ \to F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) = 0$
134		meteq0	$⊢ (D \in Met (X) \land F (\underset{t}{⇝} (J) (G)) \in X \land \underset{t}{⇝} (J) (G) \in X) \to (F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) = 0 \leftrightarrow F (\underset{t}{⇝} (J) (G)) = \underset{t}{⇝} (J) (G))$
135	11 66 17 134	syl3anc	$⊢ φ \to (F (\underset{t}{⇝} (J) (G)) D \underset{t}{⇝} (J) (G) = 0 \leftrightarrow F (\underset{t}{⇝} (J) (G)) = \underset{t}{⇝} (J) (G))$
136	133 135	mpbid	$⊢ φ \to F (\underset{t}{⇝} (J) (G)) = \underset{t}{⇝} (J) (G)$
137		fveq2	$⊢ z = \underset{t}{⇝} (J) (G) \to F (z) = F (\underset{t}{⇝} (J) (G))$
138		id	$⊢ z = \underset{t}{⇝} (J) (G) \to z = \underset{t}{⇝} (J) (G)$
139	137 138	eqeq12d	$⊢ z = \underset{t}{⇝} (J) (G) \to (F (z) = z \leftrightarrow F (\underset{t}{⇝} (J) (G)) = \underset{t}{⇝} (J) (G))$
140	139	rspcev	$⊢ (\underset{t}{⇝} (J) (G) \in X \land F (\underset{t}{⇝} (J) (G)) = \underset{t}{⇝} (J) (G)) \to \exists z \in X F (z) = z$
141	17 136 140	syl2anc	$⊢ φ \to \exists z \in X F (z) = z$

Metamath Proof Explorer

Theorem bfplem2

Proof