Theorem axcontlem11

Description: Lemma for axcont . Eliminate the hypotheses from axcontlem10 . (Contributed by Scott Fenton, 20-Jun-2013)

	Ref	Expression
Assertion	axcontlem11	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		opeq2	⊢ ( 𝑞 = 𝑝 → ⟨ 𝑍 , 𝑞 ⟩ = ⟨ 𝑍 , 𝑝 ⟩ )
2	1	breq2d	⊢ ( 𝑞 = 𝑝 → ( 𝑈 Btwn ⟨ 𝑍 , 𝑞 ⟩ ↔ 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ) )
3		breq1	⊢ ( 𝑞 = 𝑝 → ( 𝑞 Btwn ⟨ 𝑍 , 𝑈 ⟩ ↔ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) )
4	2 3	orbi12d	⊢ ( 𝑞 = 𝑝 → ( ( 𝑈 Btwn ⟨ 𝑍 , 𝑞 ⟩ ∨ 𝑞 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ↔ ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) )
5	4	cbvrabv	⊢ { 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑞 ⟩ ∨ 𝑞 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) } = { 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) }
6		eqid	⊢ { ⟨ 𝑧 , 𝑟 ⟩ ∣ ( 𝑧 ∈ { 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑞 ⟩ ∨ 𝑞 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) } ∧ ( 𝑟 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑧 ‘ 𝑗 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑗 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑗 ) ) ) ) ) } = { ⟨ 𝑧 , 𝑟 ⟩ ∣ ( 𝑧 ∈ { 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑞 ⟩ ∨ 𝑞 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) } ∧ ( 𝑟 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑧 ‘ 𝑗 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑗 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑗 ) ) ) ) ) }
7	6	axcontlem1	⊢ { ⟨ 𝑧 , 𝑟 ⟩ ∣ ( 𝑧 ∈ { 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑞 ⟩ ∨ 𝑞 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) } ∧ ( 𝑟 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑗 ∈ ( 1 ... 𝑁 ) ( 𝑧 ‘ 𝑗 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑗 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑗 ) ) ) ) ) } = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥 ∈ { 𝑞 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑞 ⟩ ∨ 𝑞 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) } ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) }
8	5 7	axcontlem10	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ )