Definition df-trkg2d

Description: Define the class of geometries fulfilling the lower dimension axiom, Axiom A8 of Schwabhauser p. 12, and the upper dimension axiom, Axiom A9 of Schwabhauser p. 13, for dimension 2. (Contributed by Thierry Arnoux, 14-Mar-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	df-trkg2d	⊢ TarskiG2D = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( dist ‘ 𝑓 ) / 𝑑 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( ( 𝑥 𝑑 𝑢 ) = ( 𝑥 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑦 𝑑 𝑣 ) ∧ ( 𝑧 𝑑 𝑢 ) = ( 𝑧 𝑑 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cstrkg2d	⊢ TarskiG2D
1		vf	⊢ 𝑓
2		cbs	⊢ Base
3	1	cv	⊢ 𝑓
4	3 2	cfv	⊢ ( Base ‘ 𝑓 )
5		vp	⊢ 𝑝
6		cds	⊢ dist
7	3 6	cfv	⊢ ( dist ‘ 𝑓 )
8		vd	⊢ 𝑑
9		citv	⊢ Itv
10	3 9	cfv	⊢ ( Itv ‘ 𝑓 )
11		vi	⊢ 𝑖
12		vx	⊢ 𝑥
13	5	cv	⊢ 𝑝
14		vy	⊢ 𝑦
15		vz	⊢ 𝑧
16	15	cv	⊢ 𝑧
17	12	cv	⊢ 𝑥
18	11	cv	⊢ 𝑖
19	14	cv	⊢ 𝑦
20	17 19 18	co	⊢ ( 𝑥 𝑖 𝑦 )
21	16 20	wcel	⊢ 𝑧 ∈ ( 𝑥 𝑖 𝑦 )
22	16 19 18	co	⊢ ( 𝑧 𝑖 𝑦 )
23	17 22	wcel	⊢ 𝑥 ∈ ( 𝑧 𝑖 𝑦 )
24	17 16 18	co	⊢ ( 𝑥 𝑖 𝑧 )
25	19 24	wcel	⊢ 𝑦 ∈ ( 𝑥 𝑖 𝑧 )
26	21 23 25	w3o	⊢ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) )
27	26	wn	⊢ ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) )
28	27 15 13	wrex	⊢ ∃ 𝑧 ∈ 𝑝 ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) )
29	28 14 13	wrex	⊢ ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) )
30	29 12 13	wrex	⊢ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) )
31		vu	⊢ 𝑢
32		vv	⊢ 𝑣
33	8	cv	⊢ 𝑑
34	31	cv	⊢ 𝑢
35	17 34 33	co	⊢ ( 𝑥 𝑑 𝑢 )
36	32	cv	⊢ 𝑣
37	17 36 33	co	⊢ ( 𝑥 𝑑 𝑣 )
38	35 37	wceq	⊢ ( 𝑥 𝑑 𝑢 ) = ( 𝑥 𝑑 𝑣 )
39	19 34 33	co	⊢ ( 𝑦 𝑑 𝑢 )
40	19 36 33	co	⊢ ( 𝑦 𝑑 𝑣 )
41	39 40	wceq	⊢ ( 𝑦 𝑑 𝑢 ) = ( 𝑦 𝑑 𝑣 )
42	16 34 33	co	⊢ ( 𝑧 𝑑 𝑢 )
43	16 36 33	co	⊢ ( 𝑧 𝑑 𝑣 )
44	42 43	wceq	⊢ ( 𝑧 𝑑 𝑢 ) = ( 𝑧 𝑑 𝑣 )
45	38 41 44	w3a	⊢ ( ( 𝑥 𝑑 𝑢 ) = ( 𝑥 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑦 𝑑 𝑣 ) ∧ ( 𝑧 𝑑 𝑢 ) = ( 𝑧 𝑑 𝑣 ) )
46	34 36	wne	⊢ 𝑢 ≠ 𝑣
47	45 46	wa	⊢ ( ( ( 𝑥 𝑑 𝑢 ) = ( 𝑥 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑦 𝑑 𝑣 ) ∧ ( 𝑧 𝑑 𝑢 ) = ( 𝑧 𝑑 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 )
48	47 26	wi	⊢ ( ( ( ( 𝑥 𝑑 𝑢 ) = ( 𝑥 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑦 𝑑 𝑣 ) ∧ ( 𝑧 𝑑 𝑢 ) = ( 𝑧 𝑑 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) )
49	48 32 13	wral	⊢ ∀ 𝑣 ∈ 𝑝 ( ( ( ( 𝑥 𝑑 𝑢 ) = ( 𝑥 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑦 𝑑 𝑣 ) ∧ ( 𝑧 𝑑 𝑢 ) = ( 𝑧 𝑑 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) )
50	49 31 13	wral	⊢ ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( ( 𝑥 𝑑 𝑢 ) = ( 𝑥 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑦 𝑑 𝑣 ) ∧ ( 𝑧 𝑑 𝑢 ) = ( 𝑧 𝑑 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) )
51	50 15 13	wral	⊢ ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( ( 𝑥 𝑑 𝑢 ) = ( 𝑥 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑦 𝑑 𝑣 ) ∧ ( 𝑧 𝑑 𝑢 ) = ( 𝑧 𝑑 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) )
52	51 14 13	wral	⊢ ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( ( 𝑥 𝑑 𝑢 ) = ( 𝑥 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑦 𝑑 𝑣 ) ∧ ( 𝑧 𝑑 𝑢 ) = ( 𝑧 𝑑 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) )
53	52 12 13	wral	⊢ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( ( 𝑥 𝑑 𝑢 ) = ( 𝑥 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑦 𝑑 𝑣 ) ∧ ( 𝑧 𝑑 𝑢 ) = ( 𝑧 𝑑 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) )
54	30 53	wa	⊢ ( ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( ( 𝑥 𝑑 𝑢 ) = ( 𝑥 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑦 𝑑 𝑣 ) ∧ ( 𝑧 𝑑 𝑢 ) = ( 𝑧 𝑑 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) )
55	54 11 10	wsbc	⊢ [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( ( 𝑥 𝑑 𝑢 ) = ( 𝑥 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑦 𝑑 𝑣 ) ∧ ( 𝑧 𝑑 𝑢 ) = ( 𝑧 𝑑 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) )
56	55 8 7	wsbc	⊢ [ ( dist ‘ 𝑓 ) / 𝑑 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( ( 𝑥 𝑑 𝑢 ) = ( 𝑥 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑦 𝑑 𝑣 ) ∧ ( 𝑧 𝑑 𝑢 ) = ( 𝑧 𝑑 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) )
57	56 5 4	wsbc	⊢ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( dist ‘ 𝑓 ) / 𝑑 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( ( 𝑥 𝑑 𝑢 ) = ( 𝑥 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑦 𝑑 𝑣 ) ∧ ( 𝑧 𝑑 𝑢 ) = ( 𝑧 𝑑 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) )
58	57 1	cab	⊢ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( dist ‘ 𝑓 ) / 𝑑 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( ( 𝑥 𝑑 𝑢 ) = ( 𝑥 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑦 𝑑 𝑣 ) ∧ ( 𝑧 𝑑 𝑢 ) = ( 𝑧 𝑑 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) ) }
59	0 58	wceq	⊢ TarskiG2D = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( dist ‘ 𝑓 ) / 𝑑 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ∃ 𝑧 ∈ 𝑝 ¬ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ∀ 𝑢 ∈ 𝑝 ∀ 𝑣 ∈ 𝑝 ( ( ( ( 𝑥 𝑑 𝑢 ) = ( 𝑥 𝑑 𝑣 ) ∧ ( 𝑦 𝑑 𝑢 ) = ( 𝑦 𝑑 𝑣 ) ∧ ( 𝑧 𝑑 𝑢 ) = ( 𝑧 𝑑 𝑣 ) ) ∧ 𝑢 ≠ 𝑣 ) → ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) ) ) }