Metamath Proof Explorer

Theorem axcontlem9

Description: Lemma for axcont . Given the separation assumption, all values of F over A are less than or equal to all values of F over B . (Contributed by Scott Fenton, 20-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 axcontlem9.1 ⊢ 𝐷 = { 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) }
2 axcontlem9.2 ⊢ 𝐹 = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) }
3 simpll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝑁 ∈ ℕ )
4 simprl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
5 simplr1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) )
6 simprl2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝑈 ∈ 𝐴 )
7 5 6 sseldd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
8 simprr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝑍 ≠ 𝑈 )
9 1 2 axcontlem2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) → 𝐹 : 𝐷 –1-1-onto→ ( 0 [,) +∞ ) )
10 3 4 7 8 9 syl31anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝐹 : 𝐷 –1-1-onto→ ( 0 [,) +∞ ) )
11 f1ofun ⊢ ( 𝐹 : 𝐷 –1-1-onto→ ( 0 [,) +∞ ) → Fun 𝐹 )
12 fvelima ⊢ ( ( Fun 𝐹 ∧ 𝑛 ∈ ( 𝐹 “ 𝐴 ) ) → ∃ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑛 )
13 12 ex ⊢ ( Fun 𝐹 → ( 𝑛 ∈ ( 𝐹 “ 𝐴 ) → ∃ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑛 ) )
14 10 11 13 3syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( 𝑛 ∈ ( 𝐹 “ 𝐴 ) → ∃ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑛 ) )
15 fvelima ⊢ ( ( Fun 𝐹 ∧ 𝑚 ∈ ( 𝐹 “ 𝐵 ) ) → ∃ 𝑏 ∈ 𝐵 ( 𝐹 ‘ 𝑏 ) = 𝑚 )
16 15 ex ⊢ ( Fun 𝐹 → ( 𝑚 ∈ ( 𝐹 “ 𝐵 ) → ∃ 𝑏 ∈ 𝐵 ( 𝐹 ‘ 𝑏 ) = 𝑚 ) )
17 10 11 16 3syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( 𝑚 ∈ ( 𝐹 “ 𝐵 ) → ∃ 𝑏 ∈ 𝐵 ( 𝐹 ‘ 𝑏 ) = 𝑚 ) )
18 reeanv ⊢ ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) = 𝑛 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑚 ) ↔ ( ∃ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑛 ∧ ∃ 𝑏 ∈ 𝐵 ( 𝐹 ‘ 𝑏 ) = 𝑚 ) )
19 simplr3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ )
20 breq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ↔ 𝑎 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) )
21 opeq2 ⊢ ( 𝑦 = 𝑏 → ⟨ 𝑍 , 𝑦 ⟩ = ⟨ 𝑍 , 𝑏 ⟩ )
22 21 breq2d ⊢ ( 𝑦 = 𝑏 → ( 𝑎 Btwn ⟨ 𝑍 , 𝑦 ⟩ ↔ 𝑎 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) )
23 20 22 rspc2v ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ → 𝑎 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) )
24 19 23 mpan9 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 Btwn ⟨ 𝑍 , 𝑏 ⟩ )
25 simplll ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑁 ∈ ℕ )
26 4 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
27 7 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
28 25 26 27 3jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) )
29 simplrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑍 ≠ 𝑈 )
30 1 axcontlem4 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝐴 ⊆ 𝐷 )
31 30 sseld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( 𝑎 ∈ 𝐴 → 𝑎 ∈ 𝐷 ) )
32 simpl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) )
33 1 axcontlem3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) → 𝐵 ⊆ 𝐷 )
34 32 4 6 8 33 syl13anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝐵 ⊆ 𝐷 )
35 34 sseld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( 𝑏 ∈ 𝐵 → 𝑏 ∈ 𝐷 ) )
36 31 35 anim12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷 ) ) )
37 36 imp ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷 ) )
38 1 2 axcontlem7 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷 ) ) → ( 𝑎 Btwn ⟨ 𝑍 , 𝑏 ⟩ ↔ ( 𝐹 ‘ 𝑎 ) ≤ ( 𝐹 ‘ 𝑏 ) ) )
39 28 29 37 38 syl21anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 Btwn ⟨ 𝑍 , 𝑏 ⟩ ↔ ( 𝐹 ‘ 𝑎 ) ≤ ( 𝐹 ‘ 𝑏 ) ) )
40 24 39 mpbid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑎 ) ≤ ( 𝐹 ‘ 𝑏 ) )
41 breq12 ⊢ ( ( ( 𝐹 ‘ 𝑎 ) = 𝑛 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑚 ) → ( ( 𝐹 ‘ 𝑎 ) ≤ ( 𝐹 ‘ 𝑏 ) ↔ 𝑛 ≤ 𝑚 ) )
42 40 41 syl5ibcom ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = 𝑛 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑚 ) → 𝑛 ≤ 𝑚 ) )
43 42 rexlimdvva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ( ( 𝐹 ‘ 𝑎 ) = 𝑛 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑚 ) → 𝑛 ≤ 𝑚 ) )
44 18 43 biimtrrid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( ( ∃ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑛 ∧ ∃ 𝑏 ∈ 𝐵 ( 𝐹 ‘ 𝑏 ) = 𝑚 ) → 𝑛 ≤ 𝑚 ) )
45 14 17 44 syl2and ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ( ( 𝑛 ∈ ( 𝐹 “ 𝐴 ) ∧ 𝑚 ∈ ( 𝐹 “ 𝐵 ) ) → 𝑛 ≤ 𝑚 ) )
46 45 ralrimivv ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ∀ 𝑛 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑚 ∈ ( 𝐹 “ 𝐵 ) 𝑛 ≤ 𝑚 )