Theorem bfp

Description: Banach fixed point theorem, also known as contraction mapping theorem. A contraction on a complete metric space has a unique fixed point. We show existence in the lemmas, and uniqueness here - if F has two fixed points, then the distance between them is less than K times itself, a contradiction. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 5-Jun-2014)

	Ref	Expression
Hypotheses	bfp.2	⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
	bfp.3	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
	bfp.4	⊢ ( 𝜑 → 𝐾 ∈ ℝ+ )
	bfp.5	⊢ ( 𝜑 → 𝐾 < 1 )
	bfp.6	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑋 )
	bfp.7	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) )
Assertion	bfp	⊢ ( 𝜑 → ∃! 𝑧 ∈ 𝑋 ( 𝐹 ‘ 𝑧 ) = 𝑧 )

Proof

Step	Hyp	Ref	Expression
1		bfp.2	⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
2		bfp.3	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
3		bfp.4	⊢ ( 𝜑 → 𝐾 ∈ ℝ+ )
4		bfp.5	⊢ ( 𝜑 → 𝐾 < 1 )
5		bfp.6	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑋 )
6		bfp.7	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) )
7		n0	⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ 𝑋 )
8	2 7	sylib	⊢ ( 𝜑 → ∃ 𝑤 𝑤 ∈ 𝑋 )
9	1	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
10	2	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → 𝑋 ≠ ∅ )
11	3	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → 𝐾 ∈ ℝ+ )
12	4	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → 𝐾 < 1 )
13	5	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → 𝐹 : 𝑋 ⟶ 𝑋 )
14	6	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) )
15		eqid	⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
16		simpr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → 𝑤 ∈ 𝑋 )
17		eqid	⊢ seq 1 ( ( 𝐹 ∘ 1st ) , ( ℕ × { 𝑤 } ) ) = seq 1 ( ( 𝐹 ∘ 1st ) , ( ℕ × { 𝑤 } ) )
18	9 10 11 12 13 14 15 16 17	bfplem2	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → ∃ 𝑧 ∈ 𝑋 ( 𝐹 ‘ 𝑧 ) = 𝑧 )
19	8 18	exlimddv	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑋 ( 𝐹 ‘ 𝑧 ) = 𝑧 )
20		oveq12	⊢ ( ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 𝐷 𝑦 ) )
21	20	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) = ( 𝑥 𝐷 𝑦 ) )
22	6	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝐷 ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) )
23	21 22	eqbrtrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) )
24		cmetmet	⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
25	1 24	syl	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
26	25	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
27		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → 𝑥 ∈ 𝑋 )
28		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → 𝑦 ∈ 𝑋 )
29		metcl	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ )
30	26 27 28 29	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ )
31	3	rpred	⊢ ( 𝜑 → 𝐾 ∈ ℝ )
32	31	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → 𝐾 ∈ ℝ )
33	32 30	remulcld	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) ∈ ℝ )
34	30 33	suble0d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( ( ( 𝑥 𝐷 𝑦 ) − ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) ) ≤ 0 ↔ ( 𝑥 𝐷 𝑦 ) ≤ ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) ) )
35	23 34	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( ( 𝑥 𝐷 𝑦 ) − ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) ) ≤ 0 )
36		1cnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → 1 ∈ ℂ )
37	32	recnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → 𝐾 ∈ ℂ )
38	30	recnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( 𝑥 𝐷 𝑦 ) ∈ ℂ )
39	36 37 38	subdird	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( ( 1 − 𝐾 ) · ( 𝑥 𝐷 𝑦 ) ) = ( ( 1 · ( 𝑥 𝐷 𝑦 ) ) − ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) ) )
40	38	mullidd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( 1 · ( 𝑥 𝐷 𝑦 ) ) = ( 𝑥 𝐷 𝑦 ) )
41	40	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( ( 1 · ( 𝑥 𝐷 𝑦 ) ) − ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) ) = ( ( 𝑥 𝐷 𝑦 ) − ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) ) )
42	39 41	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( ( 1 − 𝐾 ) · ( 𝑥 𝐷 𝑦 ) ) = ( ( 𝑥 𝐷 𝑦 ) − ( 𝐾 · ( 𝑥 𝐷 𝑦 ) ) ) )
43		1re	⊢ 1 ∈ ℝ
44		resubcl	⊢ ( ( 1 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 1 − 𝐾 ) ∈ ℝ )
45	43 31 44	sylancr	⊢ ( 𝜑 → ( 1 − 𝐾 ) ∈ ℝ )
46	45	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( 1 − 𝐾 ) ∈ ℝ )
47	46	recnd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( 1 − 𝐾 ) ∈ ℂ )
48	47	mul01d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( ( 1 − 𝐾 ) · 0 ) = 0 )
49	35 42 48	3brtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( ( 1 − 𝐾 ) · ( 𝑥 𝐷 𝑦 ) ) ≤ ( ( 1 − 𝐾 ) · 0 ) )
50		0red	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → 0 ∈ ℝ )
51		posdif	⊢ ( ( 𝐾 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐾 < 1 ↔ 0 < ( 1 − 𝐾 ) ) )
52	31 43 51	sylancl	⊢ ( 𝜑 → ( 𝐾 < 1 ↔ 0 < ( 1 − 𝐾 ) ) )
53	4 52	mpbid	⊢ ( 𝜑 → 0 < ( 1 − 𝐾 ) )
54	53	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → 0 < ( 1 − 𝐾 ) )
55		lemul2	⊢ ( ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ ∧ 0 ∈ ℝ ∧ ( ( 1 − 𝐾 ) ∈ ℝ ∧ 0 < ( 1 − 𝐾 ) ) ) → ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ↔ ( ( 1 − 𝐾 ) · ( 𝑥 𝐷 𝑦 ) ) ≤ ( ( 1 − 𝐾 ) · 0 ) ) )
56	30 50 46 54 55	syl112anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ↔ ( ( 1 − 𝐾 ) · ( 𝑥 𝐷 𝑦 ) ) ≤ ( ( 1 − 𝐾 ) · 0 ) ) )
57	49 56	mpbird	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( 𝑥 𝐷 𝑦 ) ≤ 0 )
58		metge0	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ ( 𝑥 𝐷 𝑦 ) )
59	26 27 28 58	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → 0 ≤ ( 𝑥 𝐷 𝑦 ) )
60		0re	⊢ 0 ∈ ℝ
61		letri3	⊢ ( ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ∧ 0 ≤ ( 𝑥 𝐷 𝑦 ) ) ) )
62	30 60 61	sylancl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ∧ 0 ≤ ( 𝑥 𝐷 𝑦 ) ) ) )
63	57 59 62	mpbir2and	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( 𝑥 𝐷 𝑦 ) = 0 )
64		meteq0	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
65	26 27 28 64	syl3anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
66	63 65	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) → 𝑥 = 𝑦 )
67	66	ex	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) → 𝑥 = 𝑦 ) )
68	67	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) → 𝑥 = 𝑦 ) )
69		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
70		id	⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 )
71	69 70	eqeq12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ↔ ( 𝐹 ‘ 𝑧 ) = 𝑧 ) )
72	71	anbi1d	⊢ ( 𝑥 = 𝑧 → ( ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑧 ) = 𝑧 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) ) )
73		equequ1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝑦 ↔ 𝑧 = 𝑦 ) )
74	72 73	imbi12d	⊢ ( 𝑥 = 𝑧 → ( ( ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( ( ( 𝐹 ‘ 𝑧 ) = 𝑧 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) → 𝑧 = 𝑦 ) ) )
75	74	ralbidv	⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝑋 ( ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑋 ( ( ( 𝐹 ‘ 𝑧 ) = 𝑧 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) → 𝑧 = 𝑦 ) ) )
76	75	cbvralvw	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝐹 ‘ 𝑧 ) = 𝑧 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) → 𝑧 = 𝑦 ) )
77	68 76	sylib	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝐹 ‘ 𝑧 ) = 𝑧 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) → 𝑧 = 𝑦 ) )
78		fveq2	⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )
79		id	⊢ ( 𝑧 = 𝑦 → 𝑧 = 𝑦 )
80	78 79	eqeq12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝐹 ‘ 𝑧 ) = 𝑧 ↔ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) )
81	80	reu4	⊢ ( ∃! 𝑧 ∈ 𝑋 ( 𝐹 ‘ 𝑧 ) = 𝑧 ↔ ( ∃ 𝑧 ∈ 𝑋 ( 𝐹 ‘ 𝑧 ) = 𝑧 ∧ ∀ 𝑧 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( ( 𝐹 ‘ 𝑧 ) = 𝑧 ∧ ( 𝐹 ‘ 𝑦 ) = 𝑦 ) → 𝑧 = 𝑦 ) ) )
82	19 77 81	sylanbrc	⊢ ( 𝜑 → ∃! 𝑧 ∈ 𝑋 ( 𝐹 ‘ 𝑧 ) = 𝑧 )