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 ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ∀ 𝑛 ∈ ( 𝐹 “ 𝐴 ) ∀ 𝑚 ∈ ( 𝐹 “ 𝐵 ) 𝑛 ≤ 𝑚 )