Metamath Proof Explorer

Theorem minvecolem7

Description: Lemma for minveco . Since any two minimal points are distance zero away from each other, the minimal point is unique. (Contributed by Mario Carneiro, 9-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses minveco.x ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
minveco.m ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
minveco.n ⊢ 𝑁 = ( normCV ‘ 𝑈 )
minveco.y ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
minveco.u ⊢ ( 𝜑 → 𝑈 ∈ CPreHilOLD )
minveco.w ⊢ ( 𝜑 → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
minveco.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
minveco.d ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
minveco.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
minveco.r ⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
minveco.s ⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
Assertion minvecolem7 ( 𝜑 → ∃! 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 minveco.x ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 minveco.m ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3 minveco.n ⊢ 𝑁 = ( normCV ‘ 𝑈 )
4 minveco.y ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
5 minveco.u ⊢ ( 𝜑 → 𝑈 ∈ CPreHilOLD )
6 minveco.w ⊢ ( 𝜑 → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
7 minveco.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8 minveco.d ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
9 minveco.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
10 minveco.r ⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
11 minveco.s ⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
12 1 2 3 4 5 6 7 8 9 10 11 minvecolem5 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
13 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → 𝑈 ∈ CPreHilOLD )
14 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
15 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → 𝐴 ∈ 𝑋 )
16 0re ⊢ 0 ∈ ℝ
17 16 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → 0 ∈ ℝ )
18 0le0 ⊢ 0 ≤ 0
19 18 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → 0 ≤ 0 )
20 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → 𝑥 ∈ 𝑌 )
21 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → 𝑤 ∈ 𝑌 )
22 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) )
23 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) )
24 1 2 3 4 13 14 15 8 9 10 11 17 19 20 21 22 23 minvecolem2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) ∧ ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ) → ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ ( 4 · 0 ) )
25 24 ex ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) → ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ ( 4 · 0 ) ) )
26 1 2 3 4 5 6 7 8 9 10 11 minvecolem6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
27 26 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
28 1 2 3 4 5 6 7 8 9 10 11 minvecolem6 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑌 ) → ( ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑤 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
29 28 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑤 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
30 27 29 anbi12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( ( 𝐴 𝐷 𝑥 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ∧ ( ( 𝐴 𝐷 𝑤 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 0 ) ) ↔ ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑤 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) ) )
31 4cn ⊢ 4 ∈ ℂ
32 31 mul01i ⊢ ( 4 · 0 ) = 0
33 32 breq2i ⊢ ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ ( 4 · 0 ) ↔ ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ 0 )
34 phnv ⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec )
35 5 34 syl ⊢ ( 𝜑 → 𝑈 ∈ NrmCVec )
36 35 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑈 ∈ NrmCVec )
37 1 8 imsmet ⊢ ( 𝑈 ∈ NrmCVec → 𝐷 ∈ ( Met ‘ 𝑋 ) )
38 36 37 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
39 inss1 ⊢ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) ⊆ ( SubSp ‘ 𝑈 )
40 39 6 sseldi ⊢ ( 𝜑 → 𝑊 ∈ ( SubSp ‘ 𝑈 ) )
41 eqid ⊢ ( SubSp ‘ 𝑈 ) = ( SubSp ‘ 𝑈 )
42 1 4 41 sspba ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) → 𝑌 ⊆ 𝑋 )
43 35 40 42 syl2anc ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
44 43 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑌 ⊆ 𝑋 )
45 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑥 ∈ 𝑌 )
46 44 45 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑥 ∈ 𝑋 )
47 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑤 ∈ 𝑌 )
48 44 47 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 𝑤 ∈ 𝑋 )
49 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑤 ) ∈ ℝ )
50 38 46 48 49 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( 𝑥 𝐷 𝑤 ) ∈ ℝ )
51 50 sqge0d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → 0 ≤ ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) )
52 51 biantrud ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ 0 ↔ ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ 0 ∧ 0 ≤ ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ) ) )
53 50 resqcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ∈ ℝ )
54 letri3 ⊢ ( ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) = 0 ↔ ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ 0 ∧ 0 ≤ ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ) ) )
55 53 16 54 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) = 0 ↔ ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ 0 ∧ 0 ≤ ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ) ) )
56 50 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( 𝑥 𝐷 𝑤 ) ∈ ℂ )
57 sqeq0 ⊢ ( ( 𝑥 𝐷 𝑤 ) ∈ ℂ → ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) = 0 ↔ ( 𝑥 𝐷 𝑤 ) = 0 ) )
58 56 57 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) = 0 ↔ ( 𝑥 𝐷 𝑤 ) = 0 ) )
59 meteq0 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑥 𝐷 𝑤 ) = 0 ↔ 𝑥 = 𝑤 ) )
60 38 46 48 59 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( 𝑥 𝐷 𝑤 ) = 0 ↔ 𝑥 = 𝑤 ) )
61 58 60 bitrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) = 0 ↔ 𝑥 = 𝑤 ) )
62 52 55 61 3bitr2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ 0 ↔ 𝑥 = 𝑤 ) )
63 33 62 syl5bb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝑥 𝐷 𝑤 ) ↑ 2 ) ≤ ( 4 · 0 ) ↔ 𝑥 = 𝑤 ) )
64 25 30 63 3imtr3d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑤 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) → 𝑥 = 𝑤 ) )
65 64 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑌 ∀ 𝑤 ∈ 𝑌 ( ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑤 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) → 𝑥 = 𝑤 ) )
66 oveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐴 𝑀 𝑥 ) = ( 𝐴 𝑀 𝑤 ) )
67 66 fveq2d ⊢ ( 𝑥 = 𝑤 → ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝑤 ) ) )
68 67 breq1d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝐴 𝑀 𝑤 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
69 68 ralbidv ⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑤 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
70 69 reu4 ⊢ ( ∃! 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↔ ( ∃ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∧ ∀ 𝑥 ∈ 𝑌 ∀ 𝑤 ∈ 𝑌 ( ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑤 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) → 𝑥 = 𝑤 ) ) )
71 12 65 70 sylanbrc ⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )