MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dir Structured version   Visualization version   GIF version

Definition df-dir 17452
Description: Define the class of all directed sets/directions. (Contributed by Jeff Hankins, 25-Nov-2009.)
Assertion
Ref Expression
df-dir DirRel = {𝑟 ∣ ((Rel 𝑟 ∧ ( I ↾ 𝑟) ⊆ 𝑟) ∧ ((𝑟𝑟) ⊆ 𝑟 ∧ ( 𝑟 × 𝑟) ⊆ (𝑟𝑟)))}

Detailed syntax breakdown of Definition df-dir
StepHypRef Expression
1 cdir 17450 . 2 class DirRel
2 vr . . . . . . 7 setvar 𝑟
32cv 1631 . . . . . 6 class 𝑟
43wrel 5272 . . . . 5 wff Rel 𝑟
5 cid 5174 . . . . . . 7 class I
63cuni 4589 . . . . . . . 8 class 𝑟
76cuni 4589 . . . . . . 7 class 𝑟
85, 7cres 5269 . . . . . 6 class ( I ↾ 𝑟)
98, 3wss 3716 . . . . 5 wff ( I ↾ 𝑟) ⊆ 𝑟
104, 9wa 383 . . . 4 wff (Rel 𝑟 ∧ ( I ↾ 𝑟) ⊆ 𝑟)
113, 3ccom 5271 . . . . . 6 class (𝑟𝑟)
1211, 3wss 3716 . . . . 5 wff (𝑟𝑟) ⊆ 𝑟
137, 7cxp 5265 . . . . . 6 class ( 𝑟 × 𝑟)
143ccnv 5266 . . . . . . 7 class 𝑟
1514, 3ccom 5271 . . . . . 6 class (𝑟𝑟)
1613, 15wss 3716 . . . . 5 wff ( 𝑟 × 𝑟) ⊆ (𝑟𝑟)
1712, 16wa 383 . . . 4 wff ((𝑟𝑟) ⊆ 𝑟 ∧ ( 𝑟 × 𝑟) ⊆ (𝑟𝑟))
1810, 17wa 383 . . 3 wff ((Rel 𝑟 ∧ ( I ↾ 𝑟) ⊆ 𝑟) ∧ ((𝑟𝑟) ⊆ 𝑟 ∧ ( 𝑟 × 𝑟) ⊆ (𝑟𝑟)))
1918, 2cab 2747 . 2 class {𝑟 ∣ ((Rel 𝑟 ∧ ( I ↾ 𝑟) ⊆ 𝑟) ∧ ((𝑟𝑟) ⊆ 𝑟 ∧ ( 𝑟 × 𝑟) ⊆ (𝑟𝑟)))}
201, 19wceq 1632 1 wff DirRel = {𝑟 ∣ ((Rel 𝑟 ∧ ( I ↾ 𝑟) ⊆ 𝑟) ∧ ((𝑟𝑟) ⊆ 𝑟 ∧ ( 𝑟 × 𝑟) ⊆ (𝑟𝑟)))}
Colors of variables: wff setvar class
This definition is referenced by:  isdir  17454
  Copyright terms: Public domain W3C validator