Metamath Proof Explorer

Theorem axcontlem10

Description: Lemma for axcont . Given a handful of assumptions, derive the conclusion of the final theorem. (Contributed by Scott Fenton, 20-Jun-2013)

Ref Expression
Hypotheses axcontlem10.1 ⊢ 𝐷 = { 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) }
axcontlem10.2 ⊢ 𝐹 = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) }
Assertion axcontlem10 ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ )

Proof

Step Hyp Ref Expression
1 axcontlem10.1 ⊢ 𝐷 = { 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) }
2 axcontlem10.2 ⊢ 𝐹 = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) }
3 imassrn ⊢ ( 𝐹 “ 𝐴 ) ⊆ ran 𝐹
4 simpll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝑁 ∈ ℕ )
5 simprl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
6 simplr1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) )
7 simprl2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝑈 ∈ 𝐴 )
8 6 7 sseldd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
9 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝑍 ≠ 𝑈 )
10 1 2 axcontlem2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) → 𝐹 : 𝐷 –1-1-onto→ ( 0 [,) +∞ ) )
11 4 5 8 9 10 syl31anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝐹 : 𝐷 –1-1-onto→ ( 0 [,) +∞ ) )
12 f1ofo ⊢ ( 𝐹 : 𝐷 –1-1-onto→ ( 0 [,) +∞ ) → 𝐹 : 𝐷 –onto→ ( 0 [,) +∞ ) )
13 forn ⊢ ( 𝐹 : 𝐷 –onto→ ( 0 [,) +∞ ) → ran 𝐹 = ( 0 [,) +∞ ) )
14 11 12 13 3syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ran 𝐹 = ( 0 [,) +∞ ) )
15 3 14 sseqtrid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( 𝐹 “ 𝐴 ) ⊆ ( 0 [,) +∞ ) )
16 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
17 15 16 sstrdi ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( 𝐹 “ 𝐴 ) ⊆ ℝ )
18 imassrn ⊢ ( 𝐹 “ 𝐵 ) ⊆ ran 𝐹
19 18 14 sseqtrid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( 𝐹 “ 𝐵 ) ⊆ ( 0 [,) +∞ ) )
20 19 16 sstrdi ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( 𝐹 “ 𝐵 ) ⊆ ℝ )
21 1 2 axcontlem9 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) 𝑚 ≤ 𝑛 )
22 dedekindle ⊢ ( ( ( 𝐹 “ 𝐴 ) ⊆ ℝ ∧ ( 𝐹 “ 𝐵 ) ⊆ ℝ ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) 𝑚 ≤ 𝑛 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) )
23 17 20 21 22 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) )
24 simpr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) ∧ 𝑘 ∈ ℝ ) → 𝑘 ∈ ℝ )
25 simprl3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝐵 ≠ ∅ )
26 25 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) ∧ 𝑘 ∈ ℝ ) → 𝐵 ≠ ∅ )
27 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ 𝐵 )
28 26 27 sylib ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) ∧ 𝑘 ∈ ℝ ) → ∃ 𝑏 𝑏 ∈ 𝐵 )
29 0red ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) ∧ ( 𝑘 ∈ ℝ ∧ 𝑏 ∈ 𝐵 ) ) → 0 ∈ ℝ )
30 f1of ⊢ ( 𝐹 : 𝐷 –1-1-onto→ ( 0 [,) +∞ ) → 𝐹 : 𝐷 ⟶ ( 0 [,) +∞ ) )
31 11 30 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝐹 : 𝐷 ⟶ ( 0 [,) +∞ ) )
32 1 axcontlem4 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝐴 ⊆ 𝐷 )
33 32 7 sseldd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝑈 ∈ 𝐷 )
34 31 33 ffvelcdmd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( 𝐹 ‘ 𝑈 ) ∈ ( 0 [,) +∞ ) )
35 16 34 sselid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( 𝐹 ‘ 𝑈 ) ∈ ℝ )
36 35 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) ∧ ( 𝑘 ∈ ℝ ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑈 ) ∈ ℝ )
37 simprl ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) ∧ ( 𝑘 ∈ ℝ ∧ 𝑏 ∈ 𝐵 ) ) → 𝑘 ∈ ℝ )
38 elrege0 ⊢ ( ( 𝐹 ‘ 𝑈 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑈 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑈 ) ) )
39 38 simprbi ⊢ ( ( 𝐹 ‘ 𝑈 ) ∈ ( 0 [,) +∞ ) → 0 ≤ ( 𝐹 ‘ 𝑈 ) )
40 34 39 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 0 ≤ ( 𝐹 ‘ 𝑈 ) )
41 40 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) ∧ ( 𝑘 ∈ ℝ ∧ 𝑏 ∈ 𝐵 ) ) → 0 ≤ ( 𝐹 ‘ 𝑈 ) )
42 f1of1 ⊢ ( 𝐹 : 𝐷 –1-1-onto→ ( 0 [,) +∞ ) → 𝐹 : 𝐷 –1-1→ ( 0 [,) +∞ ) )
43 11 42 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝐹 : 𝐷 –1-1→ ( 0 [,) +∞ ) )
44 f1elima ⊢ ( ( 𝐹 : 𝐷 –1-1→ ( 0 [,) +∞ ) ∧ 𝑈 ∈ 𝐷 ∧ 𝐴 ⊆ 𝐷 ) → ( ( 𝐹 ‘ 𝑈 ) ∈ ( 𝐹 “ 𝐴 ) ↔ 𝑈 ∈ 𝐴 ) )
45 43 33 32 44 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( ( 𝐹 ‘ 𝑈 ) ∈ ( 𝐹 “ 𝐴 ) ↔ 𝑈 ∈ 𝐴 ) )
46 7 45 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( 𝐹 ‘ 𝑈 ) ∈ ( 𝐹 “ 𝐴 ) )
47 46 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( 𝑘 ∈ ℝ ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑈 ) ∈ ( 𝐹 “ 𝐴 ) )
48 simpr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
49 43 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝐹 : 𝐷 –1-1→ ( 0 [,) +∞ ) )
50 simpl1 ⊢ ( ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
51 simpl2 ⊢ ( ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) → 𝑈 ∈ 𝐴 )
52 simpr ⊢ ( ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) → 𝑍 ≠ 𝑈 )
53 50 51 52 3jca ⊢ ( ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) → ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) )
54 1 axcontlem3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) → 𝐵 ⊆ 𝐷 )
55 53 54 sylan2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝐵 ⊆ 𝐷 )
56 55 sselda ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐷 )
57 55 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝐵 ⊆ 𝐷 )
58 f1elima ⊢ ( ( 𝐹 : 𝐷 –1-1→ ( 0 [,) +∞ ) ∧ 𝑏 ∈ 𝐷 ∧ 𝐵 ⊆ 𝐷 ) → ( ( 𝐹 ‘ 𝑏 ) ∈ ( 𝐹 “ 𝐵 ) ↔ 𝑏 ∈ 𝐵 ) )
59 49 56 57 58 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑏 ) ∈ ( 𝐹 “ 𝐵 ) ↔ 𝑏 ∈ 𝐵 ) )
60 48 59 mpbird ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑏 ) ∈ ( 𝐹 “ 𝐵 ) )
61 60 adantrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( 𝑘 ∈ ℝ ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑏 ) ∈ ( 𝐹 “ 𝐵 ) )
62 47 61 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( 𝑘 ∈ ℝ ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑈 ) ∈ ( 𝐹 “ 𝐴 ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ ( 𝐹 “ 𝐵 ) ) )
63 breq1 ⊢ ( 𝑚 = ( 𝐹 ‘ 𝑈 ) → ( 𝑚 ≤ 𝑘 ↔ ( 𝐹 ‘ 𝑈 ) ≤ 𝑘 ) )
64 63 anbi1d ⊢ ( 𝑚 = ( 𝐹 ‘ 𝑈 ) → ( ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ↔ ( ( 𝐹 ‘ 𝑈 ) ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) )
65 breq2 ⊢ ( 𝑛 = ( 𝐹 ‘ 𝑏 ) → ( 𝑘 ≤ 𝑛 ↔ 𝑘 ≤ ( 𝐹 ‘ 𝑏 ) ) )
66 65 anbi2d ⊢ ( 𝑛 = ( 𝐹 ‘ 𝑏 ) → ( ( ( 𝐹 ‘ 𝑈 ) ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ↔ ( ( 𝐹 ‘ 𝑈 ) ≤ 𝑘 ∧ 𝑘 ≤ ( 𝐹 ‘ 𝑏 ) ) ) )
67 64 66 rspc2va ⊢ ( ( ( ( 𝐹 ‘ 𝑈 ) ∈ ( 𝐹 “ 𝐴 ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ ( 𝐹 “ 𝐵 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑈 ) ≤ 𝑘 ∧ 𝑘 ≤ ( 𝐹 ‘ 𝑏 ) ) )
68 62 67 sylan ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( 𝑘 ∈ ℝ ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑈 ) ≤ 𝑘 ∧ 𝑘 ≤ ( 𝐹 ‘ 𝑏 ) ) )
69 68 an32s ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) ∧ ( 𝑘 ∈ ℝ ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑈 ) ≤ 𝑘 ∧ 𝑘 ≤ ( 𝐹 ‘ 𝑏 ) ) )
70 69 simpld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) ∧ ( 𝑘 ∈ ℝ ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑈 ) ≤ 𝑘 )
71 29 36 37 41 70 letrd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) ∧ ( 𝑘 ∈ ℝ ∧ 𝑏 ∈ 𝐵 ) ) → 0 ≤ 𝑘 )
72 71 expr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) ∧ 𝑘 ∈ ℝ ) → ( 𝑏 ∈ 𝐵 → 0 ≤ 𝑘 ) )
73 72 exlimdv ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) ∧ 𝑘 ∈ ℝ ) → ( ∃ 𝑏 𝑏 ∈ 𝐵 → 0 ≤ 𝑘 ) )
74 28 73 mpd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) ∧ 𝑘 ∈ ℝ ) → 0 ≤ 𝑘 )
75 elrege0 ⊢ ( 𝑘 ∈ ( 0 [,) +∞ ) ↔ ( 𝑘 ∈ ℝ ∧ 0 ≤ 𝑘 ) )
76 24 74 75 sylanbrc ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) ∧ 𝑘 ∈ ℝ ) → 𝑘 ∈ ( 0 [,) +∞ ) )
77 76 ex ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) → ( 𝑘 ∈ ℝ → 𝑘 ∈ ( 0 [,) +∞ ) ) )
78 1 ssrab3 ⊢ 𝐷 ⊆ ( 𝔼 ‘ 𝑁 )
79 simpr ⊢ ( ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) → 𝑘 ∈ ( 0 [,) +∞ ) )
80 f1ocnvdm ⊢ ( ( 𝐹 : 𝐷 –1-1-onto→ ( 0 [,) +∞ ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) → ( ◡ 𝐹 ‘ 𝑘 ) ∈ 𝐷 )
81 11 79 80 syl2an ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ) → ( ◡ 𝐹 ‘ 𝑘 ) ∈ 𝐷 )
82 78 81 sselid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ) → ( ◡ 𝐹 ‘ 𝑘 ) ∈ ( 𝔼 ‘ 𝑁 ) )
83 4 5 8 3jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) )
84 83 9 jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) )
85 84 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) ) → ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) )
86 32 sselda ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑞 ∈ 𝐴 ) → 𝑞 ∈ 𝐷 )
87 86 adantrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑞 ∈ 𝐷 )
88 87 adantrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) ) → 𝑞 ∈ 𝐷 )
89 simplr ⊢ ( ( ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑘 ∈ ( 0 [,) +∞ ) )
90 11 89 80 syl2an ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) ) → ( ◡ 𝐹 ‘ 𝑘 ) ∈ 𝐷 )
91 55 sselda ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑟 ∈ 𝐵 ) → 𝑟 ∈ 𝐷 )
92 91 adantrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑟 ∈ 𝐷 )
93 92 adantrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) ) → 𝑟 ∈ 𝐷 )
94 88 90 93 3jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) ) → ( 𝑞 ∈ 𝐷 ∧ ( ◡ 𝐹 ‘ 𝑘 ) ∈ 𝐷 ∧ 𝑟 ∈ 𝐷 ) )
95 85 94 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) ) → ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑞 ∈ 𝐷 ∧ ( ◡ 𝐹 ‘ 𝑘 ) ∈ 𝐷 ∧ 𝑟 ∈ 𝐷 ) ) )
96 f1ofun ⊢ ( 𝐹 : 𝐷 –1-1-onto→ ( 0 [,) +∞ ) → Fun 𝐹 )
97 11 96 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → Fun 𝐹 )
98 fdm ⊢ ( 𝐹 : 𝐷 ⟶ ( 0 [,) +∞ ) → dom 𝐹 = 𝐷 )
99 11 30 98 3syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → dom 𝐹 = 𝐷 )
100 32 99 sseqtrrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝐴 ⊆ dom 𝐹 )
101 funfvima2 ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝑞 ∈ 𝐴 → ( 𝐹 ‘ 𝑞 ) ∈ ( 𝐹 “ 𝐴 ) ) )
102 97 100 101 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( 𝑞 ∈ 𝐴 → ( 𝐹 ‘ 𝑞 ) ∈ ( 𝐹 “ 𝐴 ) ) )
103 55 99 sseqtrrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝐵 ⊆ dom 𝐹 )
104 funfvima2 ⊢ ( ( Fun 𝐹 ∧ 𝐵 ⊆ dom 𝐹 ) → ( 𝑟 ∈ 𝐵 → ( 𝐹 ‘ 𝑟 ) ∈ ( 𝐹 “ 𝐵 ) ) )
105 97 103 104 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( 𝑟 ∈ 𝐵 → ( 𝐹 ‘ 𝑟 ) ∈ ( 𝐹 “ 𝐵 ) ) )
106 102 105 anim12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑞 ) ∈ ( 𝐹 “ 𝐴 ) ∧ ( 𝐹 ‘ 𝑟 ) ∈ ( 𝐹 “ 𝐵 ) ) ) )
107 106 imp ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑞 ) ∈ ( 𝐹 “ 𝐴 ) ∧ ( 𝐹 ‘ 𝑟 ) ∈ ( 𝐹 “ 𝐵 ) ) )
108 107 adantrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) ) → ( ( 𝐹 ‘ 𝑞 ) ∈ ( 𝐹 “ 𝐴 ) ∧ ( 𝐹 ‘ 𝑟 ) ∈ ( 𝐹 “ 𝐵 ) ) )
109 simprll ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) ) → ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) )
110 breq1 ⊢ ( 𝑚 = ( 𝐹 ‘ 𝑞 ) → ( 𝑚 ≤ 𝑘 ↔ ( 𝐹 ‘ 𝑞 ) ≤ 𝑘 ) )
111 110 anbi1d ⊢ ( 𝑚 = ( 𝐹 ‘ 𝑞 ) → ( ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ↔ ( ( 𝐹 ‘ 𝑞 ) ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) )
112 breq2 ⊢ ( 𝑛 = ( 𝐹 ‘ 𝑟 ) → ( 𝑘 ≤ 𝑛 ↔ 𝑘 ≤ ( 𝐹 ‘ 𝑟 ) ) )
113 112 anbi2d ⊢ ( 𝑛 = ( 𝐹 ‘ 𝑟 ) → ( ( ( 𝐹 ‘ 𝑞 ) ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ↔ ( ( 𝐹 ‘ 𝑞 ) ≤ 𝑘 ∧ 𝑘 ≤ ( 𝐹 ‘ 𝑟 ) ) ) )
114 111 113 rspc2v ⊢ ( ( ( 𝐹 ‘ 𝑞 ) ∈ ( 𝐹 “ 𝐴 ) ∧ ( 𝐹 ‘ 𝑟 ) ∈ ( 𝐹 “ 𝐵 ) ) → ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) → ( ( 𝐹 ‘ 𝑞 ) ≤ 𝑘 ∧ 𝑘 ≤ ( 𝐹 ‘ 𝑟 ) ) ) )
115 108 109 114 sylc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) ) → ( ( 𝐹 ‘ 𝑞 ) ≤ 𝑘 ∧ 𝑘 ≤ ( 𝐹 ‘ 𝑟 ) ) )
116 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝐷 –1-1-onto→ ( 0 [,) +∞ ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑘 ) ) = 𝑘 )
117 11 89 116 syl2an ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑘 ) ) = 𝑘 )
118 117 breq2d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) ) → ( ( 𝐹 ‘ 𝑞 ) ≤ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑘 ) ) ↔ ( 𝐹 ‘ 𝑞 ) ≤ 𝑘 ) )
119 117 breq1d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑘 ) ) ≤ ( 𝐹 ‘ 𝑟 ) ↔ 𝑘 ≤ ( 𝐹 ‘ 𝑟 ) ) )
120 118 119 anbi12d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) ) → ( ( ( 𝐹 ‘ 𝑞 ) ≤ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑘 ) ) ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑘 ) ) ≤ ( 𝐹 ‘ 𝑟 ) ) ↔ ( ( 𝐹 ‘ 𝑞 ) ≤ 𝑘 ∧ 𝑘 ≤ ( 𝐹 ‘ 𝑟 ) ) ) )
121 115 120 mpbird ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) ) → ( ( 𝐹 ‘ 𝑞 ) ≤ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑘 ) ) ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑘 ) ) ≤ ( 𝐹 ‘ 𝑟 ) ) )
122 1 2 axcontlem8 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑞 ∈ 𝐷 ∧ ( ◡ 𝐹 ‘ 𝑘 ) ∈ 𝐷 ∧ 𝑟 ∈ 𝐷 ) ) → ( ( ( 𝐹 ‘ 𝑞 ) ≤ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑘 ) ) ∧ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑘 ) ) ≤ ( 𝐹 ‘ 𝑟 ) ) → ( ◡ 𝐹 ‘ 𝑘 ) Btwn ⟨ 𝑞 , 𝑟 ⟩ ) )
123 95 121 122 sylc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) ) → ( ◡ 𝐹 ‘ 𝑘 ) Btwn ⟨ 𝑞 , 𝑟 ⟩ )
124 123 anassrs ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐵 ) ) → ( ◡ 𝐹 ‘ 𝑘 ) Btwn ⟨ 𝑞 , 𝑟 ⟩ )
125 124 ralrimivva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ) → ∀ 𝑞 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ◡ 𝐹 ‘ 𝑘 ) Btwn ⟨ 𝑞 , 𝑟 ⟩ )
126 opeq1 ⊢ ( 𝑞 = 𝑥 → ⟨ 𝑞 , 𝑟 ⟩ = ⟨ 𝑥 , 𝑟 ⟩ )
127 126 breq2d ⊢ ( 𝑞 = 𝑥 → ( ( ◡ 𝐹 ‘ 𝑘 ) Btwn ⟨ 𝑞 , 𝑟 ⟩ ↔ ( ◡ 𝐹 ‘ 𝑘 ) Btwn ⟨ 𝑥 , 𝑟 ⟩ ) )
128 opeq2 ⊢ ( 𝑟 = 𝑦 → ⟨ 𝑥 , 𝑟 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
129 128 breq2d ⊢ ( 𝑟 = 𝑦 → ( ( ◡ 𝐹 ‘ 𝑘 ) Btwn ⟨ 𝑥 , 𝑟 ⟩ ↔ ( ◡ 𝐹 ‘ 𝑘 ) Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
130 127 129 cbvral2vw ⊢ ( ∀ 𝑞 ∈ 𝐴 ∀ 𝑟 ∈ 𝐵 ( ◡ 𝐹 ‘ 𝑘 ) Btwn ⟨ 𝑞 , 𝑟 ⟩ ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 ‘ 𝑘 ) Btwn ⟨ 𝑥 , 𝑦 ⟩ )
131 125 130 sylib ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 ‘ 𝑘 ) Btwn ⟨ 𝑥 , 𝑦 ⟩ )
132 breq1 ⊢ ( 𝑏 = ( ◡ 𝐹 ‘ 𝑘 ) → ( 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ↔ ( ◡ 𝐹 ‘ 𝑘 ) Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
133 132 2ralbidv ⊢ ( 𝑏 = ( ◡ 𝐹 ‘ 𝑘 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 ‘ 𝑘 ) Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
134 133 rspcev ⊢ ( ( ( ◡ 𝐹 ‘ 𝑘 ) ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 ‘ 𝑘 ) Btwn ⟨ 𝑥 , 𝑦 ⟩ ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ )
135 82 131 134 syl2anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ∧ 𝑘 ∈ ( 0 [,) +∞ ) ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ )
136 135 expr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) → ( 𝑘 ∈ ( 0 [,) +∞ ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
137 77 136 syld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) ) → ( 𝑘 ∈ ℝ → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
138 137 ex ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) → ( 𝑘 ∈ ℝ → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) )
139 138 com23 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( 𝑘 ∈ ℝ → ( ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) ) )
140 139 rexlimdv ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑚 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑛 ∈ ( 𝐹 “ 𝐵 ) ( 𝑚 ≤ 𝑘 ∧ 𝑘 ≤ 𝑛 ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
141 23 140 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ )