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 syl5bb ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ( √ ‘ ( ( 𝑆 ↑ 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 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝐷 𝑦 ) = ( 𝐴 ( 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 syl5bir ⊢ ( 𝜑 → ( ( ∃ 𝑠 ∈ ℝ+ 𝑢 = { 𝑦 ∈ 𝑌 ∣ ( ( ( 𝐴 𝐷 𝑦 ) ↑ 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 ‘ 𝑌 ) )