Theorem ebtwntg

Description: The betweenness relation used in the Tarski structure for the Euclidean geometry is the same as Btwn . (Contributed by Thierry Arnoux, 15-Mar-2019)

	Ref	Expression
Hypotheses	ebtwntg.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	ebtwntg.2	⊢ 𝑃 = ( Base ‘ ( EEG ‘ 𝑁 ) )
	ebtwntg.3	⊢ 𝐼 = ( Itv ‘ ( EEG ‘ 𝑁 ) )
	ebtwntg.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	ebtwntg.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	ebtwntg.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
Assertion	ebtwntg	⊢ ( 𝜑 → ( 𝑍 Btwn ⟨ 𝑋 , 𝑌 ⟩ ↔ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ebtwntg.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		ebtwntg.2	⊢ 𝑃 = ( Base ‘ ( EEG ‘ 𝑁 ) )
3		ebtwntg.3	⊢ 𝐼 = ( Itv ‘ ( EEG ‘ 𝑁 ) )
4		ebtwntg.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
5		ebtwntg.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
6		ebtwntg.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
7		itvid	⊢ Itv = Slot ( Itv ‘ ndx )
8		fvexd	⊢ ( 𝜑 → ( EEG ‘ 𝑁 ) ∈ V )
9		eengstr	⊢ ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) Struct ⟨ 1 , ; 1 7 ⟩ )
10	1 9	syl	⊢ ( 𝜑 → ( EEG ‘ 𝑁 ) Struct ⟨ 1 , ; 1 7 ⟩ )
11		structn0fun	⊢ ( ( EEG ‘ 𝑁 ) Struct ⟨ 1 , ; 1 7 ⟩ → Fun ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) )
12	10 11	syl	⊢ ( 𝜑 → Fun ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) )
13		structcnvcnv	⊢ ( ( EEG ‘ 𝑁 ) Struct ⟨ 1 , ; 1 7 ⟩ → ◡ ◡ ( EEG ‘ 𝑁 ) = ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) )
14	10 13	syl	⊢ ( 𝜑 → ◡ ◡ ( EEG ‘ 𝑁 ) = ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) )
15	14	funeqd	⊢ ( 𝜑 → ( Fun ◡ ◡ ( EEG ‘ 𝑁 ) ↔ Fun ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) ) )
16	12 15	mpbird	⊢ ( 𝜑 → Fun ◡ ◡ ( EEG ‘ 𝑁 ) )
17		opex	⊢ ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ ∈ V
18	17	prid1	⊢ ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ ∈ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ }
19		elun2	⊢ ( ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ ∈ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } → ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ ∈ ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } ) )
20	18 19	ax-mp	⊢ ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ ∈ ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } )
21		eengv	⊢ ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) = ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } ) )
22	1 21	syl	⊢ ( 𝜑 → ( EEG ‘ 𝑁 ) = ( { ⟨ ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) ⟩ , ⟨ ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) ⟩ } ∪ { ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ , ⟨ ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ∨ 𝑥 Btwn ⟨ 𝑧 , 𝑦 ⟩ ∨ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) } ) ⟩ } ) )
23	20 22	eleqtrrid	⊢ ( 𝜑 → ⟨ ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ⟩ ∈ ( EEG ‘ 𝑁 ) )
24		fvex	⊢ ( 𝔼 ‘ 𝑁 ) ∈ V
25	24 24	mpoex	⊢ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ∈ V
26	25	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) ∈ V )
27	7 8 16 23 26	strfv2d	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) = ( Itv ‘ ( EEG ‘ 𝑁 ) ) )
28	3 27	eqtr4id	⊢ ( 𝜑 → 𝐼 = ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } ) )
29		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑥 = 𝑋 )
30		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑦 = 𝑌 )
31	29 30	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
32	31	breq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ ) )
33	32	rabbidv	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑥 , 𝑦 ⟩ } = { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ } )
34	4 2	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
35		eengbas	⊢ ( 𝑁 ∈ ℕ → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) )
36	1 35	syl	⊢ ( 𝜑 → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) )
37	34 36	eleqtrrd	⊢ ( 𝜑 → 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) )
38	5 2	eleqtrdi	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
39	38 36	eleqtrrd	⊢ ( 𝜑 → 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) )
40	24	rabex	⊢ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ } ∈ V
41	40	a1i	⊢ ( 𝜑 → { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ } ∈ V )
42	28 33 37 39 41	ovmpod	⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ } )
43	42	eleq2d	⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝑍 ∈ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ } ) )
44	6 2	eleqtrdi	⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) )
45	44 36	eleqtrrd	⊢ ( 𝜑 → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
46		breq1	⊢ ( 𝑧 = 𝑍 → ( 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ ↔ 𝑍 Btwn ⟨ 𝑋 , 𝑌 ⟩ ) )
47	46	elrab3	⊢ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝑍 ∈ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ } ↔ 𝑍 Btwn ⟨ 𝑋 , 𝑌 ⟩ ) )
48	45 47	syl	⊢ ( 𝜑 → ( 𝑍 ∈ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn ⟨ 𝑋 , 𝑌 ⟩ } ↔ 𝑍 Btwn ⟨ 𝑋 , 𝑌 ⟩ ) )
49	43 48	bitr2d	⊢ ( 𝜑 → ( 𝑍 Btwn ⟨ 𝑋 , 𝑌 ⟩ ↔ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) )