Definition df-trkge

Description: Define the class of geometries fulfilling Euclid's axiom, Axiom A10 of Schwabhauser p. 13. (Contributed by Thierry Arnoux, 14-Mar-2019)

	Ref	Expression
Assertion	df-trkge	⊢ TarskiGE = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cstrkge	⊢ TarskiGE
1		vf	⊢ 𝑓
2		cbs	⊢ Base
3	1	cv	⊢ 𝑓
4	3 2	cfv	⊢ ( Base ‘ 𝑓 )
5		vp	⊢ 𝑝
6		citv	⊢ Itv
7	3 6	cfv	⊢ ( Itv ‘ 𝑓 )
8		vi	⊢ 𝑖
9		vx	⊢ 𝑥
10	5	cv	⊢ 𝑝
11		vy	⊢ 𝑦
12		vz	⊢ 𝑧
13		vu	⊢ 𝑢
14		vv	⊢ 𝑣
15	13	cv	⊢ 𝑢
16	9	cv	⊢ 𝑥
17	8	cv	⊢ 𝑖
18	14	cv	⊢ 𝑣
19	16 18 17	co	⊢ ( 𝑥 𝑖 𝑣 )
20	15 19	wcel	⊢ 𝑢 ∈ ( 𝑥 𝑖 𝑣 )
21	11	cv	⊢ 𝑦
22	12	cv	⊢ 𝑧
23	21 22 17	co	⊢ ( 𝑦 𝑖 𝑧 )
24	15 23	wcel	⊢ 𝑢 ∈ ( 𝑦 𝑖 𝑧 )
25	16 15	wne	⊢ 𝑥 ≠ 𝑢
26	20 24 25	w3a	⊢ ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 )
27		va	⊢ 𝑎
28		vb	⊢ 𝑏
29	27	cv	⊢ 𝑎
30	16 29 17	co	⊢ ( 𝑥 𝑖 𝑎 )
31	21 30	wcel	⊢ 𝑦 ∈ ( 𝑥 𝑖 𝑎 )
32	28	cv	⊢ 𝑏
33	16 32 17	co	⊢ ( 𝑥 𝑖 𝑏 )
34	22 33	wcel	⊢ 𝑧 ∈ ( 𝑥 𝑖 𝑏 )
35	29 32 17	co	⊢ ( 𝑎 𝑖 𝑏 )
36	18 35	wcel	⊢ 𝑣 ∈ ( 𝑎 𝑖 𝑏 )
37	31 34 36	w3a	⊢ ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) )
38	37 28 10	wrex	⊢ ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) )
39	38 27 10	wrex	⊢ ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) )
40	26 39	wi	⊢ ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) )
41	40 14 10	wral	⊢ ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) )
42	41 13 10	wral	⊢ ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) )
43	42 12 10	wral	⊢ ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) )
44	43 11 10	wral	⊢ ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) )
45	44 9 10	wral	⊢ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) )
46	45 8 7	wsbc	⊢ [ ( Itv ‘ 𝑓 ) / 𝑖 ] ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) )
47	46 5 4	wsbc	⊢ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) )
48	47 1	cab	⊢ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) }
49	0 48	wceq	⊢ TarskiGE = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( 𝑢 ∈ ( 𝑥 𝑖 𝑣 ) ∧ 𝑢 ∈ ( 𝑦 𝑖 𝑧 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑎 ∈ 𝑝 ∃ 𝑏 ∈ 𝑝 ( 𝑦 ∈ ( 𝑥 𝑖 𝑎 ) ∧ 𝑧 ∈ ( 𝑥 𝑖 𝑏 ) ∧ 𝑣 ∈ ( 𝑎 𝑖 𝑏 ) ) ) }