Metamath Proof Explorer

Theorem minveclem3b

Description: Lemma for minvec . The set of vectors within a fixed distance of the infimum forms a filter base. (Contributed by Mario Carneiro, 15-Oct-2015) (Revised by AV, 3-Oct-2020)

Ref Expression
Hypotheses minvec.x ⊒ 𝑋 = ( Base β€˜ π‘ˆ )
minvec.m ⊒ βˆ’ = ( -g β€˜ π‘ˆ )
minvec.n ⊒ 𝑁 = ( norm β€˜ π‘ˆ )
minvec.u ⊒ ( πœ‘ β†’ π‘ˆ ∈ β„‚PreHil )
minvec.y ⊒ ( πœ‘ β†’ π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) )
minvec.w ⊒ ( πœ‘ β†’ ( π‘ˆ β†Ύs π‘Œ ) ∈ CMetSp )
minvec.a ⊒ ( πœ‘ β†’ 𝐴 ∈ 𝑋 )
minvec.j ⊒ 𝐽 = ( TopOpen β€˜ π‘ˆ )
minvec.r ⊒ 𝑅 = ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
minvec.s ⊒ 𝑆 = inf ( 𝑅 , ℝ , < )
minvec.d ⊒ 𝐷 = ( ( dist β€˜ π‘ˆ ) β†Ύ ( 𝑋 Γ— 𝑋 ) )
minvec.f ⊒ 𝐹 = ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } )
Assertion minveclem3b ( πœ‘ β†’ 𝐹 ∈ ( fBas β€˜ π‘Œ ) )

Proof

Step Hyp Ref Expression
1 minvec.x ⊒ 𝑋 = ( Base β€˜ π‘ˆ )
2 minvec.m ⊒ βˆ’ = ( -g β€˜ π‘ˆ )
3 minvec.n ⊒ 𝑁 = ( norm β€˜ π‘ˆ )
4 minvec.u ⊒ ( πœ‘ β†’ π‘ˆ ∈ β„‚PreHil )
5 minvec.y ⊒ ( πœ‘ β†’ π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) )
6 minvec.w ⊒ ( πœ‘ β†’ ( π‘ˆ β†Ύs π‘Œ ) ∈ CMetSp )
7 minvec.a ⊒ ( πœ‘ β†’ 𝐴 ∈ 𝑋 )
8 minvec.j ⊒ 𝐽 = ( TopOpen β€˜ π‘ˆ )
9 minvec.r ⊒ 𝑅 = ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
10 minvec.s ⊒ 𝑆 = inf ( 𝑅 , ℝ , < )
11 minvec.d ⊒ 𝐷 = ( ( dist β€˜ π‘ˆ ) β†Ύ ( 𝑋 Γ— 𝑋 ) )
12 minvec.f ⊒ 𝐹 = ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } )
13 ssrab2 ⊒ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } βŠ† π‘Œ
14 5 adantr ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) )
15 elpw2g ⊒ ( π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) β†’ ( { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ∈ 𝒫 π‘Œ ↔ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } βŠ† π‘Œ ) )
16 14 15 syl ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ∈ 𝒫 π‘Œ ↔ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } βŠ† π‘Œ ) )
17 13 16 mpbiri ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ∈ 𝒫 π‘Œ )
18 17 fmpttd ⊒ ( πœ‘ β†’ ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ) : ℝ+ ⟢ 𝒫 π‘Œ )
19 18 frnd ⊒ ( πœ‘ β†’ ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ) βŠ† 𝒫 π‘Œ )
20 12 19 eqsstrid ⊒ ( πœ‘ β†’ 𝐹 βŠ† 𝒫 π‘Œ )
21 1rp ⊒ 1 ∈ ℝ+
22 eqid ⊒ ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ) = ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } )
23 22 17 dmmptd ⊒ ( πœ‘ β†’ dom ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ) = ℝ+ )
24 21 23 eleqtrrid ⊒ ( πœ‘ β†’ 1 ∈ dom ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ) )
25 24 ne0d ⊒ ( πœ‘ β†’ dom ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ) β‰  βˆ… )
26 dm0rn0 ⊒ ( dom ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ) = βˆ… ↔ ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ) = βˆ… )
27 12 eqeq1i ⊒ ( 𝐹 = βˆ… ↔ ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ) = βˆ… )
28 26 27 bitr4i ⊒ ( dom ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ) = βˆ… ↔ 𝐹 = βˆ… )
29 28 necon3bii ⊒ ( dom ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ) β‰  βˆ… ↔ 𝐹 β‰  βˆ… )
30 25 29 sylib ⊒ ( πœ‘ β†’ 𝐹 β‰  βˆ… )
31 1 2 3 4 5 6 7 8 9 10 minveclem4c ⊒ ( πœ‘ β†’ 𝑆 ∈ ℝ )
32 31 resqcld ⊒ ( πœ‘ β†’ ( 𝑆 ↑ 2 ) ∈ ℝ )
33 ltaddrp ⊒ ( ( ( 𝑆 ↑ 2 ) ∈ ℝ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑆 ↑ 2 ) < ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) )
34 32 33 sylan ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑆 ↑ 2 ) < ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) )
35 32 adantr ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑆 ↑ 2 ) ∈ ℝ )
36 rpre ⊒ ( π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ ℝ )
37 36 adantl ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ π‘Ÿ ∈ ℝ )
38 35 37 readdcld ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ∈ ℝ )
39 38 recnd ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ∈ β„‚ )
40 39 sqsqrtd ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ↑ 2 ) = ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) )
41 34 40 breqtrrd ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑆 ↑ 2 ) < ( ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ↑ 2 ) )
42 1 2 3 4 5 6 7 8 9 minveclem1 ⊒ ( πœ‘ β†’ ( 𝑅 βŠ† ℝ ∧ 𝑅 β‰  βˆ… ∧ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 ) )
43 42 simp1d ⊒ ( πœ‘ β†’ 𝑅 βŠ† ℝ )
44 43 adantr ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ 𝑅 βŠ† ℝ )
45 42 simp2d ⊒ ( πœ‘ β†’ 𝑅 β‰  βˆ… )
46 45 adantr ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ 𝑅 β‰  βˆ… )
47 0re ⊒ 0 ∈ ℝ
48 42 simp3d ⊒ ( πœ‘ β†’ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 )
49 breq1 ⊒ ( 𝑦 = 0 β†’ ( 𝑦 ≀ 𝑀 ↔ 0 ≀ 𝑀 ) )
50 49 ralbidv ⊒ ( 𝑦 = 0 β†’ ( βˆ€ 𝑀 ∈ 𝑅 𝑦 ≀ 𝑀 ↔ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 ) )
51 50 rspcev ⊒ ( ( 0 ∈ ℝ ∧ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 ) β†’ βˆƒ 𝑦 ∈ ℝ βˆ€ 𝑀 ∈ 𝑅 𝑦 ≀ 𝑀 )
52 47 48 51 sylancr ⊒ ( πœ‘ β†’ βˆƒ 𝑦 ∈ ℝ βˆ€ 𝑀 ∈ 𝑅 𝑦 ≀ 𝑀 )
53 52 adantr ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ βˆƒ 𝑦 ∈ ℝ βˆ€ 𝑀 ∈ 𝑅 𝑦 ≀ 𝑀 )
54 infrecl ⊒ ( ( 𝑅 βŠ† ℝ ∧ 𝑅 β‰  βˆ… ∧ βˆƒ 𝑦 ∈ ℝ βˆ€ 𝑀 ∈ 𝑅 𝑦 ≀ 𝑀 ) β†’ inf ( 𝑅 , ℝ , < ) ∈ ℝ )
55 44 46 53 54 syl3anc ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ inf ( 𝑅 , ℝ , < ) ∈ ℝ )
56 10 55 eqeltrid ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ 𝑆 ∈ ℝ )
57 0red ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ 0 ∈ ℝ )
58 56 sqge0d ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ 0 ≀ ( 𝑆 ↑ 2 ) )
59 57 35 38 58 34 lelttrd ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ 0 < ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) )
60 57 38 59 ltled ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ 0 ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) )
61 38 60 resqrtcld ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ∈ ℝ )
62 48 adantr ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 )
63 infregelb ⊒ ( ( ( 𝑅 βŠ† ℝ ∧ 𝑅 β‰  βˆ… ∧ βˆƒ 𝑦 ∈ ℝ βˆ€ 𝑀 ∈ 𝑅 𝑦 ≀ 𝑀 ) ∧ 0 ∈ ℝ ) β†’ ( 0 ≀ inf ( 𝑅 , ℝ , < ) ↔ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 ) )
64 44 46 53 57 63 syl31anc ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 0 ≀ inf ( 𝑅 , ℝ , < ) ↔ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 ) )
65 62 64 mpbird ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ 0 ≀ inf ( 𝑅 , ℝ , < ) )
66 65 10 breqtrrdi ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ 0 ≀ 𝑆 )
67 38 60 sqrtge0d ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ 0 ≀ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) )
68 56 61 66 67 lt2sqd ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑆 < ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ↔ ( 𝑆 ↑ 2 ) < ( ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ↑ 2 ) ) )
69 41 68 mpbird ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ 𝑆 < ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) )
70 56 61 ltnled ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( 𝑆 < ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ↔ Β¬ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ 𝑆 ) )
71 69 70 mpbid ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ Β¬ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ 𝑆 )
72 10 breq2i ⊒ ( ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ 𝑆 ↔ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ inf ( 𝑅 , ℝ , < ) )
73 infregelb ⊒ ( ( ( 𝑅 βŠ† ℝ ∧ 𝑅 β‰  βˆ… ∧ βˆƒ 𝑦 ∈ ℝ βˆ€ 𝑀 ∈ 𝑅 𝑦 ≀ 𝑀 ) ∧ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ∈ ℝ ) β†’ ( ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ inf ( 𝑅 , ℝ , < ) ↔ βˆ€ 𝑀 ∈ 𝑅 ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ 𝑀 ) )
74 44 46 53 61 73 syl31anc ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ inf ( 𝑅 , ℝ , < ) ↔ βˆ€ 𝑀 ∈ 𝑅 ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ 𝑀 ) )
75 9 raleqi ⊒ ( βˆ€ 𝑀 ∈ 𝑅 ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ 𝑀 ↔ βˆ€ 𝑀 ∈ ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ 𝑀 )
76 fvex ⊒ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ∈ V
77 76 rgenw ⊒ βˆ€ 𝑦 ∈ π‘Œ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ∈ V
78 eqid ⊒ ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) = ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
79 breq2 ⊒ ( 𝑀 = ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) β†’ ( ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ 𝑀 ↔ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) )
80 78 79 ralrnmptw ⊒ ( βˆ€ 𝑦 ∈ π‘Œ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ∈ V β†’ ( βˆ€ 𝑀 ∈ ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ 𝑀 ↔ βˆ€ 𝑦 ∈ π‘Œ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) )
81 77 80 ax-mp ⊒ ( βˆ€ 𝑀 ∈ ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ 𝑀 ↔ βˆ€ 𝑦 ∈ π‘Œ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
82 75 81 bitri ⊒ ( βˆ€ 𝑀 ∈ 𝑅 ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ 𝑀 ↔ βˆ€ 𝑦 ∈ π‘Œ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
83 74 82 bitrdi ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ inf ( 𝑅 , ℝ , < ) ↔ βˆ€ 𝑦 ∈ π‘Œ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) )
84 72 83 bitrid ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ 𝑆 ↔ βˆ€ 𝑦 ∈ π‘Œ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) )
85 71 84 mtbid ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ Β¬ βˆ€ 𝑦 ∈ π‘Œ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
86 rexnal ⊒ ( βˆƒ 𝑦 ∈ π‘Œ Β¬ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ↔ Β¬ βˆ€ 𝑦 ∈ π‘Œ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
87 85 86 sylibr ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ βˆƒ 𝑦 ∈ π‘Œ Β¬ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
88 61 adantr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ∈ ℝ )
89 cphngp ⊒ ( π‘ˆ ∈ β„‚PreHil β†’ π‘ˆ ∈ NrmGrp )
90 4 89 syl ⊒ ( πœ‘ β†’ π‘ˆ ∈ NrmGrp )
91 ngpms ⊒ ( π‘ˆ ∈ NrmGrp β†’ π‘ˆ ∈ MetSp )
92 1 11 msmet ⊒ ( π‘ˆ ∈ MetSp β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
93 90 91 92 3syl ⊒ ( πœ‘ β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
94 93 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
95 7 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ 𝐴 ∈ 𝑋 )
96 eqid ⊒ ( LSubSp β€˜ π‘ˆ ) = ( LSubSp β€˜ π‘ˆ )
97 1 96 lssss ⊒ ( π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) β†’ π‘Œ βŠ† 𝑋 )
98 14 97 syl ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ π‘Œ βŠ† 𝑋 )
99 98 sselda ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ 𝑦 ∈ 𝑋 )
100 metcl ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) β†’ ( 𝐴 𝐷 𝑦 ) ∈ ℝ )
101 94 95 99 100 syl3anc ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝐴 𝐷 𝑦 ) ∈ ℝ )
102 67 adantr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ 0 ≀ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) )
103 metge0 ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) β†’ 0 ≀ ( 𝐴 𝐷 𝑦 ) )
104 94 95 99 103 syl3anc ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ 0 ≀ ( 𝐴 𝐷 𝑦 ) )
105 88 101 102 104 le2sqd ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ ( 𝐴 𝐷 𝑦 ) ↔ ( ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ↑ 2 ) ≀ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ) )
106 11 oveqi ⊒ ( 𝐴 𝐷 𝑦 ) = ( 𝐴 ( ( dist β€˜ π‘ˆ ) β†Ύ ( 𝑋 Γ— 𝑋 ) ) 𝑦 )
107 95 99 ovresd ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝐴 ( ( dist β€˜ π‘ˆ ) β†Ύ ( 𝑋 Γ— 𝑋 ) ) 𝑦 ) = ( 𝐴 ( dist β€˜ π‘ˆ ) 𝑦 ) )
108 106 107 eqtrid ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝐴 𝐷 𝑦 ) = ( 𝐴 ( dist β€˜ π‘ˆ ) 𝑦 ) )
109 90 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ π‘ˆ ∈ NrmGrp )
110 eqid ⊒ ( dist β€˜ π‘ˆ ) = ( dist β€˜ π‘ˆ )
111 3 1 2 110 ngpds ⊒ ( ( π‘ˆ ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) β†’ ( 𝐴 ( dist β€˜ π‘ˆ ) 𝑦 ) = ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
112 109 95 99 111 syl3anc ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝐴 ( dist β€˜ π‘ˆ ) 𝑦 ) = ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
113 108 112 eqtrd ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝐴 𝐷 𝑦 ) = ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
114 113 breq2d ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ ( 𝐴 𝐷 𝑦 ) ↔ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) )
115 40 adantr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ↑ 2 ) = ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) )
116 115 breq1d ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( ( ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ↑ 2 ) ≀ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ↔ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ≀ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ) )
117 105 114 116 3bitr3d ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ↔ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ≀ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ) )
118 117 notbid ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( Β¬ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ↔ Β¬ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ≀ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ) )
119 38 adantr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ∈ ℝ )
120 101 resqcld ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ∈ ℝ )
121 119 120 letrid ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ≀ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ∨ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) )
122 121 ord ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( Β¬ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ≀ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) β†’ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) )
123 118 122 sylbid ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( Β¬ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) β†’ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) )
124 123 reximdva ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ ( βˆƒ 𝑦 ∈ π‘Œ Β¬ ( √ β€˜ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) β†’ βˆƒ 𝑦 ∈ π‘Œ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) )
125 87 124 mpd ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ βˆƒ 𝑦 ∈ π‘Œ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) )
126 rabn0 ⊒ ( { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } β‰  βˆ… ↔ βˆƒ 𝑦 ∈ π‘Œ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) )
127 125 126 sylibr ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } β‰  βˆ… )
128 127 necomd ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ βˆ… β‰  { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } )
129 128 neneqd ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ Β¬ βˆ… = { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } )
130 129 nrexdv ⊒ ( πœ‘ β†’ Β¬ βˆƒ π‘Ÿ ∈ ℝ+ βˆ… = { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } )
131 12 eleq2i ⊒ ( βˆ… ∈ 𝐹 ↔ βˆ… ∈ ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ) )
132 0ex ⊒ βˆ… ∈ V
133 22 elrnmpt ⊒ ( βˆ… ∈ V β†’ ( βˆ… ∈ ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ) ↔ βˆƒ π‘Ÿ ∈ ℝ+ βˆ… = { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ) )
134 132 133 ax-mp ⊒ ( βˆ… ∈ ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ) ↔ βˆƒ π‘Ÿ ∈ ℝ+ βˆ… = { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } )
135 131 134 bitri ⊒ ( βˆ… ∈ 𝐹 ↔ βˆƒ π‘Ÿ ∈ ℝ+ βˆ… = { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } )
136 130 135 sylnibr ⊒ ( πœ‘ β†’ Β¬ βˆ… ∈ 𝐹 )
137 df-nel ⊒ ( βˆ… βˆ‰ 𝐹 ↔ Β¬ βˆ… ∈ 𝐹 )
138 136 137 sylibr ⊒ ( πœ‘ β†’ βˆ… βˆ‰ 𝐹 )
139 56 adantr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ 𝑆 ∈ ℝ )
140 139 resqcld ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝑆 ↑ 2 ) ∈ ℝ )
141 37 adantr ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ π‘Ÿ ∈ ℝ )
142 120 140 141 lesubadd2d ⊒ ( ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ ↔ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) ) )
143 142 rabbidva ⊒ ( ( πœ‘ ∧ π‘Ÿ ∈ ℝ+ ) β†’ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } = { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } )
144 143 mpteq2dva ⊒ ( πœ‘ β†’ ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } ) = ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ) )
145 144 rneqd ⊒ ( πœ‘ β†’ ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } ) = ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + π‘Ÿ ) } ) )
146 12 145 eqtr4id ⊒ ( πœ‘ β†’ 𝐹 = ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } ) )
147 146 eleq2d ⊒ ( πœ‘ β†’ ( 𝑒 ∈ 𝐹 ↔ 𝑒 ∈ ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } ) ) )
148 breq2 ⊒ ( π‘Ÿ = 𝑠 β†’ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ ↔ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 ) )
149 148 rabbidv ⊒ ( π‘Ÿ = 𝑠 β†’ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 } )
150 149 cbvmptv ⊒ ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } ) = ( 𝑠 ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 } )
151 150 elrnmpt ⊒ ( 𝑒 ∈ V β†’ ( 𝑒 ∈ ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } ) ↔ βˆƒ 𝑠 ∈ ℝ+ 𝑒 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 } ) )
152 151 elv ⊒ ( 𝑒 ∈ ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } ) ↔ βˆƒ 𝑠 ∈ ℝ+ 𝑒 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 } )
153 147 152 bitrdi ⊒ ( πœ‘ β†’ ( 𝑒 ∈ 𝐹 ↔ βˆƒ 𝑠 ∈ ℝ+ 𝑒 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 } ) )
154 146 eleq2d ⊒ ( πœ‘ β†’ ( 𝑣 ∈ 𝐹 ↔ 𝑣 ∈ ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } ) ) )
155 breq2 ⊒ ( π‘Ÿ = 𝑑 β†’ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ ↔ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 ) )
156 155 rabbidv ⊒ ( π‘Ÿ = 𝑑 β†’ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 } )
157 156 cbvmptv ⊒ ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } ) = ( 𝑑 ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 } )
158 157 elrnmpt ⊒ ( 𝑣 ∈ V β†’ ( 𝑣 ∈ ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } ) ↔ βˆƒ 𝑑 ∈ ℝ+ 𝑣 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 } ) )
159 158 elv ⊒ ( 𝑣 ∈ ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } ) ↔ βˆƒ 𝑑 ∈ ℝ+ 𝑣 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 } )
160 154 159 bitrdi ⊒ ( πœ‘ β†’ ( 𝑣 ∈ 𝐹 ↔ βˆƒ 𝑑 ∈ ℝ+ 𝑣 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 } ) )
161 153 160 anbi12d ⊒ ( πœ‘ β†’ ( ( 𝑒 ∈ 𝐹 ∧ 𝑣 ∈ 𝐹 ) ↔ ( βˆƒ 𝑠 ∈ ℝ+ 𝑒 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 } ∧ βˆƒ 𝑑 ∈ ℝ+ 𝑣 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 } ) ) )
162 reeanv ⊒ ( βˆƒ 𝑠 ∈ ℝ+ βˆƒ 𝑑 ∈ ℝ+ ( 𝑒 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 } ∧ 𝑣 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 } ) ↔ ( βˆƒ 𝑠 ∈ ℝ+ 𝑒 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 } ∧ βˆƒ 𝑑 ∈ ℝ+ 𝑣 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 } ) )
163 93 ad2antrr ⊒ ( ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ 𝑦 ∈ π‘Œ ) β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
164 7 ad2antrr ⊒ ( ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ 𝑦 ∈ π‘Œ ) β†’ 𝐴 ∈ 𝑋 )
165 5 97 syl ⊒ ( πœ‘ β†’ π‘Œ βŠ† 𝑋 )
166 165 adantr ⊒ ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) β†’ π‘Œ βŠ† 𝑋 )
167 166 sselda ⊒ ( ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ 𝑦 ∈ π‘Œ ) β†’ 𝑦 ∈ 𝑋 )
168 163 164 167 100 syl3anc ⊒ ( ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝐴 𝐷 𝑦 ) ∈ ℝ )
169 168 resqcld ⊒ ( ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) ∈ ℝ )
170 32 ad2antrr ⊒ ( ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( 𝑆 ↑ 2 ) ∈ ℝ )
171 169 170 resubcld ⊒ ( ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ∈ ℝ )
172 simplrl ⊒ ( ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ 𝑦 ∈ π‘Œ ) β†’ 𝑠 ∈ ℝ+ )
173 172 rpred ⊒ ( ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ 𝑦 ∈ π‘Œ ) β†’ 𝑠 ∈ ℝ )
174 simplrr ⊒ ( ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ 𝑦 ∈ π‘Œ ) β†’ 𝑑 ∈ ℝ+ )
175 174 rpred ⊒ ( ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ 𝑦 ∈ π‘Œ ) β†’ 𝑑 ∈ ℝ )
176 lemin ⊒ ( ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ∈ ℝ ∧ 𝑠 ∈ ℝ ∧ 𝑑 ∈ ℝ ) β†’ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ if ( 𝑠 ≀ 𝑑 , 𝑠 , 𝑑 ) ↔ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 ∧ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 ) ) )
177 171 173 175 176 syl3anc ⊒ ( ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ 𝑦 ∈ π‘Œ ) β†’ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ if ( 𝑠 ≀ 𝑑 , 𝑠 , 𝑑 ) ↔ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 ∧ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 ) ) )
178 177 rabbidva ⊒ ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) β†’ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ if ( 𝑠 ≀ 𝑑 , 𝑠 , 𝑑 ) } = { 𝑦 ∈ π‘Œ ∣ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 ∧ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 ) } )
179 ifcl ⊒ ( ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) β†’ if ( 𝑠 ≀ 𝑑 , 𝑠 , 𝑑 ) ∈ ℝ+ )
180 5 adantr ⊒ ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) β†’ π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) )
181 rabexg ⊒ ( π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) β†’ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ if ( 𝑠 ≀ 𝑑 , 𝑠 , 𝑑 ) } ∈ V )
182 180 181 syl ⊒ ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) β†’ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ if ( 𝑠 ≀ 𝑑 , 𝑠 , 𝑑 ) } ∈ V )
183 eqid ⊒ ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } ) = ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } )
184 breq2 ⊒ ( π‘Ÿ = if ( 𝑠 ≀ 𝑑 , 𝑠 , 𝑑 ) β†’ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ ↔ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ if ( 𝑠 ≀ 𝑑 , 𝑠 , 𝑑 ) ) )
185 184 rabbidv ⊒ ( π‘Ÿ = if ( 𝑠 ≀ 𝑑 , 𝑠 , 𝑑 ) β†’ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ if ( 𝑠 ≀ 𝑑 , 𝑠 , 𝑑 ) } )
186 183 185 elrnmpt1s ⊒ ( ( if ( 𝑠 ≀ 𝑑 , 𝑠 , 𝑑 ) ∈ ℝ+ ∧ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ if ( 𝑠 ≀ 𝑑 , 𝑠 , 𝑑 ) } ∈ V ) β†’ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ if ( 𝑠 ≀ 𝑑 , 𝑠 , 𝑑 ) } ∈ ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } ) )
187 179 182 186 syl2an2 ⊒ ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) β†’ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ if ( 𝑠 ≀ 𝑑 , 𝑠 , 𝑑 ) } ∈ ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } ) )
188 146 adantr ⊒ ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) β†’ 𝐹 = ran ( π‘Ÿ ∈ ℝ+ ↦ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ π‘Ÿ } ) )
189 187 188 eleqtrrd ⊒ ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) β†’ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ if ( 𝑠 ≀ 𝑑 , 𝑠 , 𝑑 ) } ∈ 𝐹 )
190 178 189 eqeltrrd ⊒ ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) β†’ { 𝑦 ∈ π‘Œ ∣ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 ∧ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 ) } ∈ 𝐹 )
191 ineq12 ⊒ ( ( 𝑒 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 } ∧ 𝑣 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 } ) β†’ ( 𝑒 ∩ 𝑣 ) = ( { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 } ∩ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 } ) )
192 inrab ⊒ ( { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 } ∩ { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 } ) = { 𝑦 ∈ π‘Œ ∣ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 ∧ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 ) }
193 191 192 eqtrdi ⊒ ( ( 𝑒 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 } ∧ 𝑣 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 } ) β†’ ( 𝑒 ∩ 𝑣 ) = { 𝑦 ∈ π‘Œ ∣ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 ∧ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 ) } )
194 193 eleq1d ⊒ ( ( 𝑒 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 } ∧ 𝑣 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 } ) β†’ ( ( 𝑒 ∩ 𝑣 ) ∈ 𝐹 ↔ { 𝑦 ∈ π‘Œ ∣ ( ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 ∧ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 ) } ∈ 𝐹 ) )
195 190 194 syl5ibrcom ⊒ ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) β†’ ( ( 𝑒 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 } ∧ 𝑣 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 } ) β†’ ( 𝑒 ∩ 𝑣 ) ∈ 𝐹 ) )
196 vex ⊒ 𝑒 ∈ V
197 196 inex1 ⊒ ( 𝑒 ∩ 𝑣 ) ∈ V
198 197 pwid ⊒ ( 𝑒 ∩ 𝑣 ) ∈ 𝒫 ( 𝑒 ∩ 𝑣 )
199 inelcm ⊒ ( ( ( 𝑒 ∩ 𝑣 ) ∈ 𝐹 ∧ ( 𝑒 ∩ 𝑣 ) ∈ 𝒫 ( 𝑒 ∩ 𝑣 ) ) β†’ ( 𝐹 ∩ 𝒫 ( 𝑒 ∩ 𝑣 ) ) β‰  βˆ… )
200 198 199 mpan2 ⊒ ( ( 𝑒 ∩ 𝑣 ) ∈ 𝐹 β†’ ( 𝐹 ∩ 𝒫 ( 𝑒 ∩ 𝑣 ) ) β‰  βˆ… )
201 195 200 syl6 ⊒ ( ( πœ‘ ∧ ( 𝑠 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) β†’ ( ( 𝑒 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 } ∧ 𝑣 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 } ) β†’ ( 𝐹 ∩ 𝒫 ( 𝑒 ∩ 𝑣 ) ) β‰  βˆ… ) )
202 201 rexlimdvva ⊒ ( πœ‘ β†’ ( βˆƒ 𝑠 ∈ ℝ+ βˆƒ 𝑑 ∈ ℝ+ ( 𝑒 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 } ∧ 𝑣 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 } ) β†’ ( 𝐹 ∩ 𝒫 ( 𝑒 ∩ 𝑣 ) ) β‰  βˆ… ) )
203 162 202 biimtrrid ⊒ ( πœ‘ β†’ ( ( βˆƒ 𝑠 ∈ ℝ+ 𝑒 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑠 } ∧ βˆƒ 𝑑 ∈ ℝ+ 𝑣 = { 𝑦 ∈ π‘Œ ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 2 ) βˆ’ ( 𝑆 ↑ 2 ) ) ≀ 𝑑 } ) β†’ ( 𝐹 ∩ 𝒫 ( 𝑒 ∩ 𝑣 ) ) β‰  βˆ… ) )
204 161 203 sylbid ⊒ ( πœ‘ β†’ ( ( 𝑒 ∈ 𝐹 ∧ 𝑣 ∈ 𝐹 ) β†’ ( 𝐹 ∩ 𝒫 ( 𝑒 ∩ 𝑣 ) ) β‰  βˆ… ) )
205 204 ralrimivv ⊒ ( πœ‘ β†’ βˆ€ 𝑒 ∈ 𝐹 βˆ€ 𝑣 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑒 ∩ 𝑣 ) ) β‰  βˆ… )
206 30 138 205 3jca ⊒ ( πœ‘ β†’ ( 𝐹 β‰  βˆ… ∧ βˆ… βˆ‰ 𝐹 ∧ βˆ€ 𝑒 ∈ 𝐹 βˆ€ 𝑣 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑒 ∩ 𝑣 ) ) β‰  βˆ… ) )
207 isfbas ⊒ ( π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) β†’ ( 𝐹 ∈ ( fBas β€˜ π‘Œ ) ↔ ( 𝐹 βŠ† 𝒫 π‘Œ ∧ ( 𝐹 β‰  βˆ… ∧ βˆ… βˆ‰ 𝐹 ∧ βˆ€ 𝑒 ∈ 𝐹 βˆ€ 𝑣 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑒 ∩ 𝑣 ) ) β‰  βˆ… ) ) ) )
208 5 207 syl ⊒ ( πœ‘ β†’ ( 𝐹 ∈ ( fBas β€˜ π‘Œ ) ↔ ( 𝐹 βŠ† 𝒫 π‘Œ ∧ ( 𝐹 β‰  βˆ… ∧ βˆ… βˆ‰ 𝐹 ∧ βˆ€ 𝑒 ∈ 𝐹 βˆ€ 𝑣 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑒 ∩ 𝑣 ) ) β‰  βˆ… ) ) ) )
209 20 206 208 mpbir2and ⊒ ( πœ‘ β†’ 𝐹 ∈ ( fBas β€˜ π‘Œ ) )