Metamath Proof Explorer

Definition df-perpg

Description: Define the "perpendicular" relation. Definition 8.11 of Schwabhauser p. 59. See isperp . (Contributed by Thierry Arnoux, 8-Sep-2019)

Ref Expression
Assertion df-perpg ⊢ ⟂ 𝒢 = g ∈ V ⟼ a b | a ∈ ran ⁡ Line 𝒢 ⁡ g ∧ b ∈ ran ⁡ Line 𝒢 ⁡ g ∧ ∃ x ∈ a ∩ b ∀ u ∈ a ∀ v ∈ b ⟨“ uxv ”⟩ ∈ ∟ 𝒢 ⁡ g

Detailed syntax breakdown

Step Hyp Ref Expression
0 cperpg class ⟂ 𝒢
1 vg setvar g
2 cvv class V
3 va setvar a
4 vb setvar b
5 3 cv setvar a
6 clng class Line 𝒢
7 1 cv setvar g
8 7 6 cfv class Line 𝒢 ⁡ g
9 8 crn class ran ⁡ Line 𝒢 ⁡ g
10 5 9 wcel wff a ∈ ran ⁡ Line 𝒢 ⁡ g
11 4 cv setvar b
12 11 9 wcel wff b ∈ ran ⁡ Line 𝒢 ⁡ g
13 10 12 wa wff a ∈ ran ⁡ Line 𝒢 ⁡ g ∧ b ∈ ran ⁡ Line 𝒢 ⁡ g
14 vx setvar x
15 5 11 cin class a ∩ b
16 vu setvar u
17 vv setvar v
18 16 cv setvar u
19 14 cv setvar x
20 17 cv setvar v
21 18 19 20 cs3 class ⟨“ uxv ”⟩
22 crag class ∟ 𝒢
23 7 22 cfv class ∟ 𝒢 ⁡ g
24 21 23 wcel wff ⟨“ uxv ”⟩ ∈ ∟ 𝒢 ⁡ g
25 24 17 11 wral wff ∀ v ∈ b ⟨“ uxv ”⟩ ∈ ∟ 𝒢 ⁡ g
26 25 16 5 wral wff ∀ u ∈ a ∀ v ∈ b ⟨“ uxv ”⟩ ∈ ∟ 𝒢 ⁡ g
27 26 14 15 wrex wff ∃ x ∈ a ∩ b ∀ u ∈ a ∀ v ∈ b ⟨“ uxv ”⟩ ∈ ∟ 𝒢 ⁡ g
28 13 27 wa wff a ∈ ran ⁡ Line 𝒢 ⁡ g ∧ b ∈ ran ⁡ Line 𝒢 ⁡ g ∧ ∃ x ∈ a ∩ b ∀ u ∈ a ∀ v ∈ b ⟨“ uxv ”⟩ ∈ ∟ 𝒢 ⁡ g
29 28 3 4 copab class a b | a ∈ ran ⁡ Line 𝒢 ⁡ g ∧ b ∈ ran ⁡ Line 𝒢 ⁡ g ∧ ∃ x ∈ a ∩ b ∀ u ∈ a ∀ v ∈ b ⟨“ uxv ”⟩ ∈ ∟ 𝒢 ⁡ g
30 1 2 29 cmpt class g ∈ V ⟼ a b | a ∈ ran ⁡ Line 𝒢 ⁡ g ∧ b ∈ ran ⁡ Line 𝒢 ⁡ g ∧ ∃ x ∈ a ∩ b ∀ u ∈ a ∀ v ∈ b ⟨“ uxv ”⟩ ∈ ∟ 𝒢 ⁡ g
31 0 30 wceq wff ⟂ 𝒢 = g ∈ V ⟼ a b | a ∈ ran ⁡ Line 𝒢 ⁡ g ∧ b ∈ ran ⁡ Line 𝒢 ⁡ g ∧ ∃ x ∈ a ∩ b ∀ u ∈ a ∀ v ∈ b ⟨“ uxv ”⟩ ∈ ∟ 𝒢 ⁡ g