Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∃! 𝑧 ∈ 𝑋 ( 𝐹 ‘ 𝑧 ) = 𝑧 )