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 17224
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 17222 . 2 class DirRel
2 vr . . . . . . 7 setvar 𝑟
32cv 1481 . . . . . 6 class 𝑟
43wrel 5117 . . . . 5 wff Rel 𝑟
5 cid 5021 . . . . . . 7 class I
63cuni 4434 . . . . . . . 8 class 𝑟
76cuni 4434 . . . . . . 7 class 𝑟
85, 7cres 5114 . . . . . 6 class ( I ↾ 𝑟)
98, 3wss 3572 . . . . 5 wff ( I ↾ 𝑟) ⊆ 𝑟
104, 9wa 384 . . . 4 wff (Rel 𝑟 ∧ ( I ↾ 𝑟) ⊆ 𝑟)
113, 3ccom 5116 . . . . . 6 class (𝑟𝑟)
1211, 3wss 3572 . . . . 5 wff (𝑟𝑟) ⊆ 𝑟
137, 7cxp 5110 . . . . . 6 class ( 𝑟 × 𝑟)
143ccnv 5111 . . . . . . 7 class 𝑟
1514, 3ccom 5116 . . . . . 6 class (𝑟𝑟)
1613, 15wss 3572 . . . . 5 wff ( 𝑟 × 𝑟) ⊆ (𝑟𝑟)
1712, 16wa 384 . . . 4 wff ((𝑟𝑟) ⊆ 𝑟 ∧ ( 𝑟 × 𝑟) ⊆ (𝑟𝑟))
1810, 17wa 384 . . 3 wff ((Rel 𝑟 ∧ ( I ↾ 𝑟) ⊆ 𝑟) ∧ ((𝑟𝑟) ⊆ 𝑟 ∧ ( 𝑟 × 𝑟) ⊆ (𝑟𝑟)))
1918, 2cab 2607 . 2 class {𝑟 ∣ ((Rel 𝑟 ∧ ( I ↾ 𝑟) ⊆ 𝑟) ∧ ((𝑟𝑟) ⊆ 𝑟 ∧ ( 𝑟 × 𝑟) ⊆ (𝑟𝑟)))}
201, 19wceq 1482 1 wff DirRel = {𝑟 ∣ ((Rel 𝑟 ∧ ( I ↾ 𝑟) ⊆ 𝑟) ∧ ((𝑟𝑟) ⊆ 𝑟 ∧ ( 𝑟 × 𝑟) ⊆ (𝑟𝑟)))}
Colors of variables: wff setvar class
This definition is referenced by:  isdir  17226
  Copyright terms: Public domain W3C validator