Metamath Proof Explorer

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 ⊢ 𝒢 Tarski E = f | [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ v ∈ p u ∈ x i v ∧ u ∈ y i z ∧ x ≠ u → ∃ a ∈ p ∃ b ∈ p y ∈ x i a ∧ z ∈ x i b ∧ v ∈ a i b

Detailed syntax breakdown

Step Hyp Ref Expression
0 cstrkge class 𝒢 Tarski E
1 vf setvar f
2 cbs class Base
3 1 cv setvar f
4 3 2 cfv class Base f
5 vp setvar p
6 citv class Itv
7 3 6 cfv class Itv ⁡ f
8 vi setvar i
9 vx setvar x
10 5 cv setvar p
11 vy setvar y
12 vz setvar z
13 vu setvar u
14 vv setvar v
15 13 cv setvar u
16 9 cv setvar x
17 8 cv setvar i
18 14 cv setvar v
19 16 18 17 co class x i v
20 15 19 wcel wff u ∈ x i v
21 11 cv setvar y
22 12 cv setvar z
23 21 22 17 co class y i z
24 15 23 wcel wff u ∈ y i z
25 16 15 wne wff x ≠ u
26 20 24 25 w3a wff u ∈ x i v ∧ u ∈ y i z ∧ x ≠ u
27 va setvar a
28 vb setvar b
29 27 cv setvar a
30 16 29 17 co class x i a
31 21 30 wcel wff y ∈ x i a
32 28 cv setvar b
33 16 32 17 co class x i b
34 22 33 wcel wff z ∈ x i b
35 29 32 17 co class a i b
36 18 35 wcel wff v ∈ a i b
37 31 34 36 w3a wff y ∈ x i a ∧ z ∈ x i b ∧ v ∈ a i b
38 37 28 10 wrex wff ∃ b ∈ p y ∈ x i a ∧ z ∈ x i b ∧ v ∈ a i b
39 38 27 10 wrex wff ∃ a ∈ p ∃ b ∈ p y ∈ x i a ∧ z ∈ x i b ∧ v ∈ a i b
40 26 39 wi wff u ∈ x i v ∧ u ∈ y i z ∧ x ≠ u → ∃ a ∈ p ∃ b ∈ p y ∈ x i a ∧ z ∈ x i b ∧ v ∈ a i b
41 40 14 10 wral wff ∀ v ∈ p u ∈ x i v ∧ u ∈ y i z ∧ x ≠ u → ∃ a ∈ p ∃ b ∈ p y ∈ x i a ∧ z ∈ x i b ∧ v ∈ a i b
42 41 13 10 wral wff ∀ u ∈ p ∀ v ∈ p u ∈ x i v ∧ u ∈ y i z ∧ x ≠ u → ∃ a ∈ p ∃ b ∈ p y ∈ x i a ∧ z ∈ x i b ∧ v ∈ a i b
43 42 12 10 wral wff ∀ z ∈ p ∀ u ∈ p ∀ v ∈ p u ∈ x i v ∧ u ∈ y i z ∧ x ≠ u → ∃ a ∈ p ∃ b ∈ p y ∈ x i a ∧ z ∈ x i b ∧ v ∈ a i b
44 43 11 10 wral wff ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ v ∈ p u ∈ x i v ∧ u ∈ y i z ∧ x ≠ u → ∃ a ∈ p ∃ b ∈ p y ∈ x i a ∧ z ∈ x i b ∧ v ∈ a i b
45 44 9 10 wral wff ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ v ∈ p u ∈ x i v ∧ u ∈ y i z ∧ x ≠ u → ∃ a ∈ p ∃ b ∈ p y ∈ x i a ∧ z ∈ x i b ∧ v ∈ a i b
46 45 8 7 wsbc wff [˙ Itv ⁡ f / i]˙ ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ v ∈ p u ∈ x i v ∧ u ∈ y i z ∧ x ≠ u → ∃ a ∈ p ∃ b ∈ p y ∈ x i a ∧ z ∈ x i b ∧ v ∈ a i b
47 46 5 4 wsbc wff [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ v ∈ p u ∈ x i v ∧ u ∈ y i z ∧ x ≠ u → ∃ a ∈ p ∃ b ∈ p y ∈ x i a ∧ z ∈ x i b ∧ v ∈ a i b
48 47 1 cab class f | [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ v ∈ p u ∈ x i v ∧ u ∈ y i z ∧ x ≠ u → ∃ a ∈ p ∃ b ∈ p y ∈ x i a ∧ z ∈ x i b ∧ v ∈ a i b
49 0 48 wceq wff 𝒢 Tarski E = f | [˙Base f / p]˙ [˙ Itv ⁡ f / i]˙ ∀ x ∈ p ∀ y ∈ p ∀ z ∈ p ∀ u ∈ p ∀ v ∈ p u ∈ x i v ∧ u ∈ y i z ∧ x ≠ u → ∃ a ∈ p ∃ b ∈ p y ∈ x i a ∧ z ∈ x i b ∧ v ∈ a i b