Theorem elntg

Description: The line definition in the Tarski structure for the Euclidean geometry. (Contributed by Thierry Arnoux, 7-Apr-2019)

	Ref	Expression
Hypotheses	elntg.1	⊢ 𝑃 = ( Base ‘ ( EEG ‘ 𝑁 ) )
	elntg.2	⊢ 𝐼 = ( Itv ‘ ( EEG ‘ 𝑁 ) )
Assertion	elntg	⊢ ( 𝑁 ∈ ℕ → ( LineG ‘ ( EEG ‘ 𝑁 ) ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )

Proof

Step	Hyp	Ref	Expression
1		elntg.1	⊢ 𝑃 = ( Base ‘ ( EEG ‘ 𝑁 ) )
2		elntg.2	⊢ 𝐼 = ( Itv ‘ ( EEG ‘ 𝑁 ) )
3		lngid	⊢ LineG = Slot ( LineG ‘ ndx )
4		fvex	⊢ ( EEG ‘ 𝑁 ) ∈ V
5	4	a1i	⊢ ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) ∈ V )
6		eengstr	⊢ ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) Struct ⟨ 1 , ; 1 7 ⟩ )
7		structn0fun	⊢ ( ( EEG ‘ 𝑁 ) Struct ⟨ 1 , ; 1 7 ⟩ → Fun ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) )
8	6 7	syl	⊢ ( 𝑁 ∈ ℕ → Fun ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) )
9		structcnvcnv	⊢ ( ( EEG ‘ 𝑁 ) Struct ⟨ 1 , ; 1 7 ⟩ → ◡ ◡ ( EEG ‘ 𝑁 ) = ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) )
10	6 9	syl	⊢ ( 𝑁 ∈ ℕ → ◡ ◡ ( EEG ‘ 𝑁 ) = ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) )
11	10	funeqd	⊢ ( 𝑁 ∈ ℕ → ( Fun ◡ ◡ ( EEG ‘ 𝑁 ) ↔ Fun ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) ) )
12	8 11	mpbird	⊢ ( 𝑁 ∈ ℕ → Fun ◡ ◡ ( EEG ‘ 𝑁 ) )
13		opex	⊢ ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ ∈ V
14	13	prid2	⊢ ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ ∈ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ }
15		elun2	⊢ ( ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ ∈ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } → ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ ∈ ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } ) )
16	14 15	ax-mp	⊢ ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ ∈ ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } )
17		eengv	⊢ ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) = ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } ) )
18	16 17	eleqtrrid	⊢ ( 𝑁 ∈ ℕ → ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ ∈ ( EEG ‘ 𝑁 ) )
19		fvex	⊢ ( 𝔼 ‘ 𝑁 ) ∈ V
20	19	difexi	⊢ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ∈ V
21	19 20	mpoex	⊢ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ∈ V
22	21	a1i	⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ∈ V )
23	3 5 12 18 22	strfv2d	⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) = ( LineG ‘ ( EEG ‘ 𝑁 ) ) )
24		eengbas	⊢ ( 𝑁 ∈ ℕ → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) )
25	24 1	eqtr4di	⊢ ( 𝑁 ∈ ℕ → ( 𝔼 ‘ 𝑁 ) = 𝑃 )
26	25	difeq1d	⊢ ( 𝑁 ∈ ℕ → ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) = ( 𝑃 ∖ { 𝑥 } ) )
27	26	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) = ( 𝑃 ∖ { 𝑥 } ) )
28	25	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ) ) → ( 𝔼 ‘ 𝑁 ) = 𝑃 )
29		simpll	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ) ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
30		simplrl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ) ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
31	29 25	syl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ) ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝔼 ‘ 𝑁 ) = 𝑃 )
32	30 31	eleqtrd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ) ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑥 ∈ 𝑃 )
33		simplrr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ) ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) )
34	33	eldifad	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ) ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) )
35	34 31	eleqtrd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ) ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑦 ∈ 𝑃 )
36		simpr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ) ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) )
37	36 31	eleqtrd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ) ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑧 ∈ 𝑃 )
38	29 1 2 32 35 37	ebtwntg	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ) ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ) )
39	29 1 2 37 35 32	ebtwntg	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ) ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ↔ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ) )
40	29 1 2 32 37 35	ebtwntg	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ) ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ↔ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) )
41	38 39 40	3orbi123d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ) ) ∧ 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ↔ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) ) )
42	28 41	rabeqbidva	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ) ) → { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } = { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } )
43	25 27 42	mpoeq123dva	⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )
44	23 43	eqtr3d	⊢ ( 𝑁 ∈ ℕ → ( LineG ‘ ( EEG ‘ 𝑁 ) ) = ( 𝑥 ∈ 𝑃 , 𝑦 ∈ ( 𝑃 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑃 ∣ ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝐼 𝑧 ) ) } ) )