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	4	eqcomd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → 𝑃 = 𝑝 )
6	5	adantr	⊢ ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) → 𝑃 = 𝑝 )
7	6	adantr	⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → 𝑃 = 𝑝 )
8	7	adantr	⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → 𝑃 = 𝑝 )
9	8	adantr	⊢ ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) → 𝑃 = 𝑝 )
10		simp-6r	⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → 𝑖 = 𝐼 )
11	10	eqcomd	⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → 𝐼 = 𝑖 )
12	11	oveqd	⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑥 𝐼 𝑣 ) = ( 𝑥 𝑖 𝑣 ) )
13	12	eleq2d	⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ↔ 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ) )
14	11	oveqd	⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑦 𝐼 𝑧 ) = ( 𝑦 𝑖 𝑧 ) )
15	14	eleq2d	⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ↔ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ) )
16	13 15	3anbi12d	⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ↔ ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) ) )
17	9	adantr	⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → 𝑃 = 𝑝 )
18	17	adantr	⊢ ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) → 𝑃 = 𝑝 )
19	10	ad2antrr	⊢ ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → 𝑖 = 𝐼 )
20	19	eqcomd	⊢ ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → 𝐼 = 𝑖 )
21	20	oveqd	⊢ ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → ( 𝑥 𝐼 𝑎 ) = ( 𝑥 𝑖 𝑎 ) )
22	21	eleq2d	⊢ ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ↔ 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ) )
23	20	oveqd	⊢ ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → ( 𝑥 𝐼 𝑏 ) = ( 𝑥 𝑖 𝑏 ) )
24	23	eleq2d	⊢ ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ↔ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ) )
25	20	oveqd	⊢ ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → ( 𝑎 𝐼 𝑏 ) = ( 𝑎 𝑖 𝑏 ) )
26	25	eleq2d	⊢ ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → ( 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ↔ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) )
27	22 24 26	3anbi123d	⊢ ( ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) → ( ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) )
28	18 27	rexeqbidva	⊢ ( ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑎 ∈ 𝑃 ) → ( ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) )
29	17 28	rexeqbidva	⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) )
30	16 29	imbi12d	⊢ ( ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) → ( ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ↔ ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) ) )
31	9 30	raleqbidva	⊢ ( ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑢 ∈ 𝑃 ) → ( ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ↔ ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) ) )
32	8 31	raleqbidva	⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ↔ ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) ) )
33	7 32	raleqbidva	⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → ( ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ↔ ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) ) )
34	6 33	raleqbidva	⊢ ( ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) ∧ 𝑥 ∈ 𝑃 ) → ( ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ↔ ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) ) )
35	5 34	raleqbidva	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ↔ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) ) )
36	1 3 35	sbcie2s	⊢ ( 𝑓 = 𝐺 → ( [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) ↔ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )
37		df-trkge	⊢ TarskiGE = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) }
38	36 37	elab4g	⊢ ( 𝐺 ∈ TarskiGE ↔ ( 𝐺 ∈ V ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝐼 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝐼 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝐼 𝑏 ) ) ) ) )