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	sselid	⊢ ( 𝜑 → 𝑊 ∈ ( 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	bitrid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌 ) ) → ( ( ( 𝑥 𝐷 𝑤 ) ↑ 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	⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )