Theorem istrkge

Description: Property of fulfilling Euclid's axiom. (Contributed by Thierry Arnoux, 14-Mar-2019)

	Ref	Expression
Hypotheses	istrkg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	istrkg.d	⊢ − = ( dist ‘ 𝐺 )
	istrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
Assertion	istrkge	⊢ ( 𝐺 ∈ TarskiGE ↔ ( 𝐺 ∈ V ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		istrkg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		istrkg.d	⊢ − = ( dist ‘ 𝐺 )
3		istrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		simpl	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → 𝑝 = 𝑃 )
5		simpr	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → 𝑖 = 𝐼 )
6	5	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑥 𝑖 𝑣 ) = ( 𝑥 𝐼 𝑣 ) )
7	6	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ↔ 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ) )
8	5	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑦 𝑖 𝑧 ) = ( 𝑦 𝐼 𝑧 ) )
9	8	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ↔ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ) )
10	7 9	3anbi12d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ↔ ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) )
11	5	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑥 𝑖 𝑎 ) = ( 𝑥 𝐼 𝑎 ) )
12	11	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ↔ 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ) )
13	5	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑥 𝑖 𝑏 ) = ( 𝑥 𝐼 𝑏 ) )
14	13	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ↔ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ) )
15	5	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑎 𝑖 𝑏 ) = ( 𝑎 𝐼 𝑏 ) )
16	15	eleq2d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ↔ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) )
17	12 14 16	3anbi123d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ↔ ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
18	4 17	rexeqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ↔ ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
19	4 18	rexeqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ↔ ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
20	10 19	imbi12d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) ↔ ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
21	4 20	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) ↔ ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
22	4 21	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) ↔ ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
23	4 22	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) ↔ ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
24	4 23	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) ↔ ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
25	4 24	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) ↔ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
26	1 3 25	sbcie2s	⊢ ( 𝑓 = 𝐺 → ( [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) ↔ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
27		df-trkge	⊢ TarskiGE = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) }
28	26 27	elab4g	⊢ ( 𝐺 ∈ TarskiGE ↔ ( 𝐺 ∈ V ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )