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

Definition df-dir 17053
 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 17051 . 2 class DirRel
2 vr . . . . . . 7 setvar 𝑟
32cv 1474 . . . . . 6 class 𝑟
43wrel 5043 . . . . 5 wff Rel 𝑟
5 cid 4948 . . . . . . 7 class I
63cuni 4372 . . . . . . . 8 class 𝑟
76cuni 4372 . . . . . . 7 class 𝑟
85, 7cres 5040 . . . . . 6 class ( I ↾ 𝑟)
98, 3wss 3540 . . . . 5 wff ( I ↾ 𝑟) ⊆ 𝑟
104, 9wa 383 . . . 4 wff (Rel 𝑟 ∧ ( I ↾ 𝑟) ⊆ 𝑟)
113, 3ccom 5042 . . . . . 6 class (𝑟𝑟)
1211, 3wss 3540 . . . . 5 wff (𝑟𝑟) ⊆ 𝑟
137, 7cxp 5036 . . . . . 6 class ( 𝑟 × 𝑟)
143ccnv 5037 . . . . . . 7 class 𝑟
1514, 3ccom 5042 . . . . . 6 class (𝑟𝑟)
1613, 15wss 3540 . . . . 5 wff ( 𝑟 × 𝑟) ⊆ (𝑟𝑟)
1712, 16wa 383 . . . 4 wff ((𝑟𝑟) ⊆ 𝑟 ∧ ( 𝑟 × 𝑟) ⊆ (𝑟𝑟))
1810, 17wa 383 . . 3 wff ((Rel 𝑟 ∧ ( I ↾ 𝑟) ⊆ 𝑟) ∧ ((𝑟𝑟) ⊆ 𝑟 ∧ ( 𝑟 × 𝑟) ⊆ (𝑟𝑟)))
1918, 2cab 2596 . 2 class {𝑟 ∣ ((Rel 𝑟 ∧ ( I ↾ 𝑟) ⊆ 𝑟) ∧ ((𝑟𝑟) ⊆ 𝑟 ∧ ( 𝑟 × 𝑟) ⊆ (𝑟𝑟)))}
201, 19wceq 1475 1 wff DirRel = {𝑟 ∣ ((Rel 𝑟 ∧ ( I ↾ 𝑟) ⊆ 𝑟) ∧ ((𝑟𝑟) ⊆ 𝑟 ∧ ( 𝑟 × 𝑟) ⊆ (𝑟𝑟)))}
 Colors of variables: wff setvar class This definition is referenced by:  isdir  17055
 Copyright terms: Public domain W3C validator