Metamath Proof Explorer


Theorem brsegle

Description: Binary relation form of the segment comparison relationship. (Contributed by Scott Fenton, 11-Oct-2013)

Ref Expression
Assertion brsegle ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg𝐶 , 𝐷 ⟩ ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 opex 𝐴 , 𝐵 ⟩ ∈ V
2 opex 𝐶 , 𝐷 ⟩ ∈ V
3 eqeq1 ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ) )
4 eqcom ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
5 3 4 bitrdi ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ↔ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ) )
6 5 3anbi1d ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
7 6 rexbidv ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
8 7 2rexbidv ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
9 8 2rexbidv ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
10 eqeq1 ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ↔ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ) )
11 eqcom ( ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ↔ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
12 10 11 bitrdi ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ↔ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ) )
13 12 3anbi2d ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
14 13 rexbidv ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
15 14 2rexbidv ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
16 15 2rexbidv ( 𝑞 = ⟨ 𝐶 , 𝐷 ⟩ → ( ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
17 df-segle Seg = { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑞 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) }
18 1 2 9 16 17 brab ( ⟨ 𝐴 , 𝐵 ⟩ Seg𝐶 , 𝐷 ⟩ ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) )
19 vex 𝑎 ∈ V
20 vex 𝑏 ∈ V
21 19 20 opth ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑎 = 𝐴𝑏 = 𝐵 ) )
22 vex 𝑐 ∈ V
23 vex 𝑑 ∈ V
24 22 23 opth ( ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝑐 = 𝐶𝑑 = 𝐷 ) )
25 biid ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) )
26 21 24 25 3anbi123i ( ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) )
27 26 2rexbii ( ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) )
28 27 2rexbii ( ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) )
29 28 rexbii ( ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) )
30 simpl2l ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
31 30 ad2antrl ( ( ( 𝑎 = 𝐴 ∧ ( 𝑏 = 𝐵 ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ) ) ∧ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
32 eleenn ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → 𝑁 ∈ ℕ )
33 31 32 syl ( ( ( 𝑎 = 𝐴 ∧ ( 𝑏 = 𝐵 ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ) ) ∧ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) ) → 𝑁 ∈ ℕ )
34 simprlr ( ( ( 𝑎 = 𝐴 ∧ ( 𝑏 = 𝐵 ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ) ) ∧ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) ) → 𝑛 ∈ ℕ )
35 simprll ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) )
36 35 adantl ( ( ( 𝑎 = 𝐴 ∧ ( 𝑏 = 𝐵 ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ) ) ∧ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) )
37 axdimuniq ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) ) → 𝑁 = 𝑛 )
38 33 31 34 36 37 syl22anc ( ( ( 𝑎 = 𝐴 ∧ ( 𝑏 = 𝐵 ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ) ) ∧ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) ) → 𝑁 = 𝑛 )
39 38 fveq2d ( ( ( 𝑎 = 𝐴 ∧ ( 𝑏 = 𝐵 ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ) ) ∧ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) ) → ( 𝔼 ‘ 𝑁 ) = ( 𝔼 ‘ 𝑛 ) )
40 39 rexeqdv ( ( ( 𝑎 = 𝐴 ∧ ( 𝑏 = 𝐵 ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ) ) ∧ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) ) → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
41 40 exbiri ( ( 𝑎 = 𝐴 ∧ ( 𝑏 = 𝐵 ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ) ) → ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) )
42 41 anassrs ( ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ) → ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) )
43 eleq1 ( 𝑎 = 𝐴 → ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) )
44 eleq1 ( 𝑏 = 𝐵 → ( 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) )
45 43 44 bi2anan9 ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ) ↔ ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ) )
46 eleq1 ( 𝑐 = 𝐶 → ( 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) )
47 eleq1 ( 𝑑 = 𝐷 → ( 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐷 ∈ ( 𝔼 ‘ 𝑛 ) ) )
48 46 47 bi2anan9 ( ( 𝑐 = 𝐶𝑑 = 𝐷 ) → ( ( 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ) ↔ ( 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑛 ) ) ) )
49 45 48 bi2anan9 ( ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ) → ( ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ↔ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) )
50 49 anbi2d ( ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ) → ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) ↔ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) ) )
51 opeq12 ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
52 51 breq1d ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) )
53 52 anbi2d ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → ( ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ↔ ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) )
54 opeq12 ( ( 𝑐 = 𝐶𝑑 = 𝐷 ) → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
55 54 breq2d ( ( 𝑐 = 𝐶𝑑 = 𝐷 ) → ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ↔ 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ) )
56 opeq1 ( 𝑐 = 𝐶 → ⟨ 𝑐 , 𝑦 ⟩ = ⟨ 𝐶 , 𝑦 ⟩ )
57 56 breq2d ( 𝑐 = 𝐶 → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) )
58 57 adantr ( ( 𝑐 = 𝐶𝑑 = 𝐷 ) → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) )
59 55 58 anbi12d ( ( 𝑐 = 𝐶𝑑 = 𝐷 ) → ( ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ↔ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
60 53 59 sylan9bb ( ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ) → ( ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ↔ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
61 60 rexbidv ( ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ) → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
62 61 imbi1d ( ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ) → ( ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ↔ ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) )
63 42 50 62 3imtr4d ( ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ) → ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) )
64 63 com12 ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) → ( ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ) → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) )
65 64 expd ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) → ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) → ( ( 𝑐 = 𝐶𝑑 = 𝐷 ) → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) ) )
66 65 3impd ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) → ( ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
67 66 expr ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ) ) → ( ( 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ) → ( ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) )
68 67 rexlimdvv ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ) ) → ( ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
69 68 rexlimdvva ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
70 69 rexlimdva ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ( 𝑎 = 𝐴𝑏 = 𝐵 ) ∧ ( 𝑐 = 𝐶𝑑 = 𝐷 ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
71 29 70 syl5bi ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
72 simpl1 ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → 𝑁 ∈ ℕ )
73 simpl2l ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
74 simpl2r ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
75 simpl3l ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
76 simpl3r ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
77 eqidd ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
78 eqidd ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
79 simpr ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) )
80 opeq1 ( 𝑐 = 𝐶 → ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝑑 ⟩ )
81 80 eqeq1d ( 𝑐 = 𝐶 → ( ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝐶 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ) )
82 80 breq2d ( 𝑐 = 𝐶 → ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ↔ 𝑦 Btwn ⟨ 𝐶 , 𝑑 ⟩ ) )
83 82 57 anbi12d ( 𝑐 = 𝐶 → ( ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ↔ ( 𝑦 Btwn ⟨ 𝐶 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
84 83 rexbidv ( 𝑐 = 𝐶 → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
85 81 84 3anbi23d ( 𝑐 = 𝐶 → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) )
86 opeq2 ( 𝑑 = 𝐷 → ⟨ 𝐶 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
87 86 eqeq1d ( 𝑑 = 𝐷 → ( ⟨ 𝐶 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ) )
88 86 breq2d ( 𝑑 = 𝐷 → ( 𝑦 Btwn ⟨ 𝐶 , 𝑑 ⟩ ↔ 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ) )
89 88 anbi1d ( 𝑑 = 𝐷 → ( ( 𝑦 Btwn ⟨ 𝐶 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ↔ ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
90 89 rexbidv ( 𝑑 = 𝐷 → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
91 87 90 3anbi23d ( 𝑑 = 𝐷 → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) )
92 85 91 rspc2ev ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) )
93 75 76 77 78 79 92 syl113anc ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) )
94 opeq1 ( 𝑎 = 𝐴 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝑏 ⟩ )
95 94 eqeq1d ( 𝑎 = 𝐴 → ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ) )
96 94 breq1d ( 𝑎 = 𝐴 → ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ↔ ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) )
97 96 anbi2d ( 𝑎 = 𝐴 → ( ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ↔ ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) )
98 97 rexbidv ( 𝑎 = 𝐴 → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) )
99 95 98 3anbi13d ( 𝑎 = 𝐴 → ( ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ( ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
100 99 2rexbidv ( 𝑎 = 𝐴 → ( ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ( ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
101 opeq2 ( 𝑏 = 𝐵 → ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
102 101 eqeq1d ( 𝑏 = 𝐵 → ( ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ) )
103 101 breq1d ( 𝑏 = 𝐵 → ( ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) )
104 103 anbi2d ( 𝑏 = 𝐵 → ( ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ↔ ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) )
105 104 rexbidv ( 𝑏 = 𝐵 → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) )
106 102 105 3anbi13d ( 𝑏 = 𝐵 → ( ( ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
107 106 2rexbidv ( 𝑏 = 𝐵 → ( ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ( ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
108 100 107 rspc2ev ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) → ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) )
109 73 74 93 108 syl3anc ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) )
110 fveq2 ( 𝑛 = 𝑁 → ( 𝔼 ‘ 𝑛 ) = ( 𝔼 ‘ 𝑁 ) )
111 110 rexeqdv ( 𝑛 = 𝑁 → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) )
112 111 3anbi3d ( 𝑛 = 𝑁 → ( ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
113 110 112 rexeqbidv ( 𝑛 = 𝑁 → ( ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
114 110 113 rexeqbidv ( 𝑛 = 𝑁 → ( ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
115 110 114 rexeqbidv ( 𝑛 = 𝑁 → ( ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
116 110 115 rexeqbidv ( 𝑛 = 𝑁 → ( ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
117 116 rspcev ( ( 𝑁 ∈ ℕ ∧ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑁 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) )
118 72 109 117 syl2anc ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) → ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) )
119 118 ex ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) → ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ) )
120 71 119 impbid ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ∧ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑦 Btwn ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑐 , 𝑦 ⟩ ) ) ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )
121 18 120 syl5bb ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Seg𝐶 , 𝐷 ⟩ ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑦 Btwn ⟨ 𝐶 , 𝐷 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐶 , 𝑦 ⟩ ) ) )