Metamath Proof Explorer

Theorem axcontlem12

Description: Lemma for axcont . Eliminate the trivial cases from the previous lemmas. (Contributed by Scott Fenton, 20-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 rzal ⊢ ( 𝐵 = ∅ → ∀ 𝑦 ∈ 𝐵 𝑍 Btwn ⟨ 𝑥 , 𝑦 ⟩ )
2 1 ralrimivw ⊢ ( 𝐵 = ∅ → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑍 Btwn ⟨ 𝑥 , 𝑦 ⟩ )
3 breq1 ⊢ ( 𝑏 = 𝑍 → ( 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑍 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
4 3 2ralbidv ⊢ ( 𝑏 = 𝑍 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑍 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
5 4 rspcev ⊢ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑍 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ )
6 5 expcom ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑍 Btwn ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
7 2 6 syl ⊢ ( 𝐵 = ∅ → ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
8 7 adantld ⊢ ( 𝐵 = ∅ → ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
9 8 adantld ⊢ ( 𝐵 = ∅ → ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑍 ≠ 𝑢 ) ∧ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
10 simprrl ⊢ ( ( 𝐵 ≠ ∅ ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑍 ≠ 𝑢 ) ∧ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) )
11 simprrr ⊢ ( ( 𝐵 ≠ ∅ ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑍 ≠ 𝑢 ) ∧ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
12 simprll ⊢ ( ( 𝐵 ≠ ∅ ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑍 ≠ 𝑢 ) ∧ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝑢 ∈ 𝐴 )
13 simpl ⊢ ( ( 𝐵 ≠ ∅ ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑍 ≠ 𝑢 ) ∧ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐵 ≠ ∅ )
14 11 12 13 3jca ⊢ ( ( 𝐵 ≠ ∅ ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑍 ≠ 𝑢 ) ∧ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) )
15 simprlr ⊢ ( ( 𝐵 ≠ ∅ ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑍 ≠ 𝑢 ) ∧ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝑍 ≠ 𝑢 )
16 axcontlem11 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑢 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑢 ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ )
17 10 14 15 16 syl12anc ⊢ ( ( 𝐵 ≠ ∅ ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑍 ≠ 𝑢 ) ∧ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ )
18 17 ex ⊢ ( 𝐵 ≠ ∅ → ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑍 ≠ 𝑢 ) ∧ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
19 9 18 pm2.61ine ⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑍 ≠ 𝑢 ) ∧ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ )
20 19 ex ⊢ ( ( 𝑢 ∈ 𝐴 ∧ 𝑍 ≠ 𝑢 ) → ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
21 20 rexlimiva ⊢ ( ∃ 𝑢 ∈ 𝐴 𝑍 ≠ 𝑢 → ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
22 df-ne ⊢ ( 𝑍 ≠ 𝑢 ↔ ¬ 𝑍 = 𝑢 )
23 22 con2bii ⊢ ( 𝑍 = 𝑢 ↔ ¬ 𝑍 ≠ 𝑢 )
24 23 ralbii ⊢ ( ∀ 𝑢 ∈ 𝐴 𝑍 = 𝑢 ↔ ∀ 𝑢 ∈ 𝐴 ¬ 𝑍 ≠ 𝑢 )
25 ralnex ⊢ ( ∀ 𝑢 ∈ 𝐴 ¬ 𝑍 ≠ 𝑢 ↔ ¬ ∃ 𝑢 ∈ 𝐴 𝑍 ≠ 𝑢 )
26 24 25 bitri ⊢ ( ∀ 𝑢 ∈ 𝐴 𝑍 = 𝑢 ↔ ¬ ∃ 𝑢 ∈ 𝐴 𝑍 ≠ 𝑢 )
27 simpr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ )
28 eqeq2 ⊢ ( 𝑢 = 𝑥 → ( 𝑍 = 𝑢 ↔ 𝑍 = 𝑥 ) )
29 28 rspccva ⊢ ( ( ∀ 𝑢 ∈ 𝐴 𝑍 = 𝑢 ∧ 𝑥 ∈ 𝐴 ) → 𝑍 = 𝑥 )
30 opeq1 ⊢ ( 𝑍 = 𝑥 → ⟨ 𝑍 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
31 30 breq2d ⊢ ( 𝑍 = 𝑥 → ( 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ↔ 𝑥 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
32 breq1 ⊢ ( 𝑍 = 𝑥 → ( 𝑍 Btwn ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑥 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
33 31 32 bitr4d ⊢ ( 𝑍 = 𝑥 → ( 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ↔ 𝑍 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
34 33 ralbidv ⊢ ( 𝑍 = 𝑥 → ( ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ↔ ∀ 𝑦 ∈ 𝐵 𝑍 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
35 29 34 syl ⊢ ( ( ∀ 𝑢 ∈ 𝐴 𝑍 = 𝑢 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ↔ ∀ 𝑦 ∈ 𝐵 𝑍 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
36 35 ralbidva ⊢ ( ∀ 𝑢 ∈ 𝐴 𝑍 = 𝑢 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑍 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
37 36 biimpa ⊢ ( ( ∀ 𝑢 ∈ 𝐴 𝑍 = 𝑢 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑍 Btwn ⟨ 𝑥 , 𝑦 ⟩ )
38 27 37 sylan2 ⊢ ( ( ∀ 𝑢 ∈ 𝐴 𝑍 = 𝑢 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑍 Btwn ⟨ 𝑥 , 𝑦 ⟩ )
39 38 5 sylan2 ⊢ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( ∀ 𝑢 ∈ 𝐴 𝑍 = 𝑢 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ )
40 39 ancoms ⊢ ( ( ( ∀ 𝑢 ∈ 𝐴 𝑍 = 𝑢 ∧ ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ )
41 40 expl ⊢ ( ∀ 𝑢 ∈ 𝐴 𝑍 = 𝑢 → ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
42 26 41 sylbir ⊢ ( ¬ ∃ 𝑢 ∈ 𝐴 𝑍 ≠ 𝑢 → ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ ) )
43 21 42 pm2.61i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑏 Btwn ⟨ 𝑥 , 𝑦 ⟩ )