Metamath Proof Explorer

Theorem rencldnfilem

Description: Lemma for rencldnfi . (Contributed by Stefan O'Rear, 18-Oct-2014)

Ref Expression
Assertion rencldnfilem ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐴 ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 ) → ¬ 𝐴 ∈ Fin )

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ ( 𝑎 = 𝑐 → ( 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) ↔ 𝑐 = ( abs ‘ ( 𝑏 − 𝐵 ) ) ) )
2 1 rexbidv ⊢ ( 𝑎 = 𝑐 → ( ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) ↔ ∃ 𝑏 ∈ 𝐴 𝑐 = ( abs ‘ ( 𝑏 − 𝐵 ) ) ) )
3 2 elrab ⊢ ( 𝑐 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ↔ ( 𝑐 ∈ ℝ ∧ ∃ 𝑏 ∈ 𝐴 𝑐 = ( abs ‘ ( 𝑏 − 𝐵 ) ) ) )
4 simp-4l ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑏 ∈ 𝐴 ) → 𝐴 ⊆ ℝ )
5 simpr ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑏 ∈ 𝐴 ) → 𝑏 ∈ 𝐴 )
6 4 5 sseldd ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑏 ∈ 𝐴 ) → 𝑏 ∈ ℝ )
7 6 recnd ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑏 ∈ 𝐴 ) → 𝑏 ∈ ℂ )
8 simp-4r ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑏 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
9 8 recnd ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑏 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
10 7 9 subcld ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑏 ∈ 𝐴 ) → ( 𝑏 − 𝐵 ) ∈ ℂ )
11 simprr ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) → ¬ 𝐵 ∈ 𝐴 )
12 11 ad2antrr ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑏 ∈ 𝐴 ) → ¬ 𝐵 ∈ 𝐴 )
13 nelneq ⊢ ( ( 𝑏 ∈ 𝐴 ∧ ¬ 𝐵 ∈ 𝐴 ) → ¬ 𝑏 = 𝐵 )
14 5 12 13 syl2anc ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑏 ∈ 𝐴 ) → ¬ 𝑏 = 𝐵 )
15 subeq0 ⊢ ( ( 𝑏 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝑏 − 𝐵 ) = 0 ↔ 𝑏 = 𝐵 ) )
16 15 necon3abid ⊢ ( ( 𝑏 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝑏 − 𝐵 ) ≠ 0 ↔ ¬ 𝑏 = 𝐵 ) )
17 7 9 16 syl2anc ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑏 ∈ 𝐴 ) → ( ( 𝑏 − 𝐵 ) ≠ 0 ↔ ¬ 𝑏 = 𝐵 ) )
18 14 17 mpbird ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑏 ∈ 𝐴 ) → ( 𝑏 − 𝐵 ) ≠ 0 )
19 10 18 absrpcld ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑏 ∈ 𝐴 ) → ( abs ‘ ( 𝑏 − 𝐵 ) ) ∈ ℝ+ )
20 eleq1 ⊢ ( 𝑐 = ( abs ‘ ( 𝑏 − 𝐵 ) ) → ( 𝑐 ∈ ℝ+ ↔ ( abs ‘ ( 𝑏 − 𝐵 ) ) ∈ ℝ+ ) )
21 19 20 syl5ibrcom ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑏 ∈ 𝐴 ) → ( 𝑐 = ( abs ‘ ( 𝑏 − 𝐵 ) ) → 𝑐 ∈ ℝ+ ) )
22 21 rexlimdva ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝑐 ∈ ℝ ) → ( ∃ 𝑏 ∈ 𝐴 𝑐 = ( abs ‘ ( 𝑏 − 𝐵 ) ) → 𝑐 ∈ ℝ+ ) )
23 22 expimpd ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) → ( ( 𝑐 ∈ ℝ ∧ ∃ 𝑏 ∈ 𝐴 𝑐 = ( abs ‘ ( 𝑏 − 𝐵 ) ) ) → 𝑐 ∈ ℝ+ ) )
24 3 23 syl5bi ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) → ( 𝑐 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } → 𝑐 ∈ ℝ+ ) )
25 24 ssrdv ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) → { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ⊆ ℝ+ )
26 25 adantr ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) → { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ⊆ ℝ+ )
27 abrexfi ⊢ ( 𝐴 ∈ Fin → { 𝑎 ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ∈ Fin )
28 rabssab ⊢ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ⊆ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) }
29 ssfi ⊢ ( ( { 𝑎 ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ∈ Fin ∧ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ⊆ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ) → { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ∈ Fin )
30 27 28 29 sylancl ⊢ ( 𝐴 ∈ Fin → { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ∈ Fin )
31 30 adantl ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) → { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ∈ Fin )
32 simplrl ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) → 𝐴 ≠ ∅ )
33 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐴 )
34 32 33 sylib ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) → ∃ 𝑦 𝑦 ∈ 𝐴 )
35 simp-4l ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → 𝐴 ⊆ ℝ )
36 simpr ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
37 35 36 sseldd ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
38 37 recnd ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℂ )
39 simp-4r ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
40 39 recnd ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
41 38 40 subcld ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 − 𝐵 ) ∈ ℂ )
42 41 abscld ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → ( abs ‘ ( 𝑦 − 𝐵 ) ) ∈ ℝ )
43 eqid ⊢ ( abs ‘ ( 𝑦 − 𝐵 ) ) = ( abs ‘ ( 𝑦 − 𝐵 ) )
44 fvoveq1 ⊢ ( 𝑏 = 𝑦 → ( abs ‘ ( 𝑏 − 𝐵 ) ) = ( abs ‘ ( 𝑦 − 𝐵 ) ) )
45 44 rspceeqv ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( abs ‘ ( 𝑦 − 𝐵 ) ) = ( abs ‘ ( 𝑦 − 𝐵 ) ) ) → ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑦 − 𝐵 ) ) = ( abs ‘ ( 𝑏 − 𝐵 ) ) )
46 43 45 mpan2 ⊢ ( 𝑦 ∈ 𝐴 → ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑦 − 𝐵 ) ) = ( abs ‘ ( 𝑏 − 𝐵 ) ) )
47 46 adantl ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑦 − 𝐵 ) ) = ( abs ‘ ( 𝑏 − 𝐵 ) ) )
48 eqeq1 ⊢ ( 𝑎 = ( abs ‘ ( 𝑦 − 𝐵 ) ) → ( 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) ↔ ( abs ‘ ( 𝑦 − 𝐵 ) ) = ( abs ‘ ( 𝑏 − 𝐵 ) ) ) )
49 48 rexbidv ⊢ ( 𝑎 = ( abs ‘ ( 𝑦 − 𝐵 ) ) → ( ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) ↔ ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑦 − 𝐵 ) ) = ( abs ‘ ( 𝑏 − 𝐵 ) ) ) )
50 49 elrab ⊢ ( ( abs ‘ ( 𝑦 − 𝐵 ) ) ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ↔ ( ( abs ‘ ( 𝑦 − 𝐵 ) ) ∈ ℝ ∧ ∃ 𝑏 ∈ 𝐴 ( abs ‘ ( 𝑦 − 𝐵 ) ) = ( abs ‘ ( 𝑏 − 𝐵 ) ) ) )
51 42 47 50 sylanbrc ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → ( abs ‘ ( 𝑦 − 𝐵 ) ) ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } )
52 51 ne0d ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ≠ ∅ )
53 34 52 exlimddv ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) → { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ≠ ∅ )
54 ssrab2 ⊢ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ⊆ ℝ
55 54 a1i ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) → { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ⊆ ℝ )
56 gtso ⊢ ◡ < Or ℝ
57 fisupcl ⊢ ( ( ◡ < Or ℝ ∧ ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ∈ Fin ∧ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ≠ ∅ ∧ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ⊆ ℝ ) ) → sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } )
58 56 57 mpan ⊢ ( ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ∈ Fin ∧ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ≠ ∅ ∧ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ⊆ ℝ ) → sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } )
59 31 53 55 58 syl3anc ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) → sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } )
60 26 59 sseldd ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) → sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) ∈ ℝ+ )
61 54 a1i ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ⊆ ℝ )
62 soss ⊢ ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ⊆ ℝ → ( ◡ < Or ℝ → ◡ < Or { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ) )
63 54 56 62 mp2 ⊢ ◡ < Or { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) }
64 63 a1i ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) → ◡ < Or { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } )
65 fisupg ⊢ ( ( ◡ < Or { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ∧ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ∈ Fin ∧ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ≠ ∅ ) → ∃ 𝑐 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ( ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ¬ 𝑐 ◡ < 𝑑 ∧ ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ( 𝑑 ◡ < 𝑐 → ∃ 𝑥 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } 𝑑 ◡ < 𝑥 ) ) )
66 64 31 53 65 syl3anc ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) → ∃ 𝑐 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ( ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ¬ 𝑐 ◡ < 𝑑 ∧ ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ( 𝑑 ◡ < 𝑐 → ∃ 𝑥 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } 𝑑 ◡ < 𝑥 ) ) )
67 elrabi ⊢ ( 𝑐 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } → 𝑐 ∈ ℝ )
68 elrabi ⊢ ( 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } → 𝑑 ∈ ℝ )
69 vex ⊢ 𝑐 ∈ V
70 vex ⊢ 𝑑 ∈ V
71 69 70 brcnv ⊢ ( 𝑐 ◡ < 𝑑 ↔ 𝑑 < 𝑐 )
72 71 notbii ⊢ ( ¬ 𝑐 ◡ < 𝑑 ↔ ¬ 𝑑 < 𝑐 )
73 lenlt ⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( 𝑐 ≤ 𝑑 ↔ ¬ 𝑑 < 𝑐 ) )
74 73 biimprd ⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( ¬ 𝑑 < 𝑐 → 𝑐 ≤ 𝑑 ) )
75 72 74 syl5bi ⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( ¬ 𝑐 ◡ < 𝑑 → 𝑐 ≤ 𝑑 ) )
76 75 adantll ⊢ ( ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑑 ∈ ℝ ) → ( ¬ 𝑐 ◡ < 𝑑 → 𝑐 ≤ 𝑑 ) )
77 68 76 sylan2 ⊢ ( ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑐 ∈ ℝ ) ∧ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ) → ( ¬ 𝑐 ◡ < 𝑑 → 𝑐 ≤ 𝑑 ) )
78 77 ralimdva ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑐 ∈ ℝ ) → ( ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ¬ 𝑐 ◡ < 𝑑 → ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } 𝑐 ≤ 𝑑 ) )
79 78 adantrd ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑐 ∈ ℝ ) → ( ( ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ¬ 𝑐 ◡ < 𝑑 ∧ ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ( 𝑑 ◡ < 𝑐 → ∃ 𝑥 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } 𝑑 ◡ < 𝑥 ) ) → ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } 𝑐 ≤ 𝑑 ) )
80 67 79 sylan2 ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑐 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ) → ( ( ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ¬ 𝑐 ◡ < 𝑑 ∧ ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ( 𝑑 ◡ < 𝑐 → ∃ 𝑥 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } 𝑑 ◡ < 𝑥 ) ) → ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } 𝑐 ≤ 𝑑 ) )
81 80 reximdva ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) → ( ∃ 𝑐 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ( ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ¬ 𝑐 ◡ < 𝑑 ∧ ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ( 𝑑 ◡ < 𝑐 → ∃ 𝑥 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } 𝑑 ◡ < 𝑥 ) ) → ∃ 𝑐 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } 𝑐 ≤ 𝑑 ) )
82 66 81 mpd ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) → ∃ 𝑐 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } 𝑐 ≤ 𝑑 )
83 82 adantr ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑐 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } 𝑐 ≤ 𝑑 )
84 lbinfle ⊢ ( ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ⊆ ℝ ∧ ∃ 𝑐 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ∀ 𝑑 ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } 𝑐 ≤ 𝑑 ∧ ( abs ‘ ( 𝑦 − 𝐵 ) ) ∈ { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } ) → inf ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , < ) ≤ ( abs ‘ ( 𝑦 − 𝐵 ) ) )
85 61 83 51 84 syl3anc ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → inf ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , < ) ≤ ( abs ‘ ( 𝑦 − 𝐵 ) ) )
86 df-inf ⊢ inf ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , < ) = sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < )
87 86 eqcomi ⊢ sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) = inf ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , < )
88 87 breq1i ⊢ ( sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) ≤ ( abs ‘ ( 𝑦 − 𝐵 ) ) ↔ inf ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , < ) ≤ ( abs ‘ ( 𝑦 − 𝐵 ) ) )
89 85 88 sylibr ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) ≤ ( abs ‘ ( 𝑦 − 𝐵 ) ) )
90 54 59 sselid ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) → sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) ∈ ℝ )
91 90 adantr ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) ∈ ℝ )
92 91 42 lenltd ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → ( sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) ≤ ( abs ‘ ( 𝑦 − 𝐵 ) ) ↔ ¬ ( abs ‘ ( 𝑦 − 𝐵 ) ) < sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) ) )
93 89 92 mpbid ⊢ ( ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) ∧ 𝑦 ∈ 𝐴 ) → ¬ ( abs ‘ ( 𝑦 − 𝐵 ) ) < sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) )
94 93 ralrimiva ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) → ∀ 𝑦 ∈ 𝐴 ¬ ( abs ‘ ( 𝑦 − 𝐵 ) ) < sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) )
95 breq2 ⊢ ( 𝑥 = sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) → ( ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 ↔ ( abs ‘ ( 𝑦 − 𝐵 ) ) < sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) ) )
96 95 notbid ⊢ ( 𝑥 = sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) → ( ¬ ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 ↔ ¬ ( abs ‘ ( 𝑦 − 𝐵 ) ) < sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) ) )
97 96 ralbidv ⊢ ( 𝑥 = sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) → ( ∀ 𝑦 ∈ 𝐴 ¬ ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ¬ ( abs ‘ ( 𝑦 − 𝐵 ) ) < sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) ) )
98 97 rspcev ⊢ ( ( sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) ∈ ℝ+ ∧ ∀ 𝑦 ∈ 𝐴 ¬ ( abs ‘ ( 𝑦 − 𝐵 ) ) < sup ( { 𝑎 ∈ ℝ ∣ ∃ 𝑏 ∈ 𝐴 𝑎 = ( abs ‘ ( 𝑏 − 𝐵 ) ) } , ℝ , ◡ < ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝐴 ¬ ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 )
99 60 94 98 syl2anc ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝐴 ¬ ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 )
100 ralnex ⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 ↔ ¬ ∃ 𝑦 ∈ 𝐴 ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 )
101 100 rexbii ⊢ ( ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝐴 ¬ ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 ↔ ∃ 𝑥 ∈ ℝ+ ¬ ∃ 𝑦 ∈ 𝐴 ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 )
102 rexnal ⊢ ( ∃ 𝑥 ∈ ℝ+ ¬ ∃ 𝑦 ∈ 𝐴 ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 ↔ ¬ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐴 ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 )
103 101 102 bitri ⊢ ( ∃ 𝑥 ∈ ℝ+ ∀ 𝑦 ∈ 𝐴 ¬ ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 ↔ ¬ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐴 ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 )
104 99 103 sylib ⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ 𝐴 ∈ Fin ) → ¬ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐴 ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 )
105 104 ex ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) → ( 𝐴 ∈ Fin → ¬ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐴 ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 ) )
106 105 3impa ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) → ( 𝐴 ∈ Fin → ¬ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐴 ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 ) )
107 106 con2d ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐴 ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 → ¬ 𝐴 ∈ Fin ) )
108 107 imp ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴 ) ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐴 ( abs ‘ ( 𝑦 − 𝐵 ) ) < 𝑥 ) → ¬ 𝐴 ∈ Fin )