Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  isdir Structured version   Unicode version

Theorem isdir 14677
 Description: A condition for a relation to be a direction. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
Hypothesis
Ref Expression
isdir.1
Assertion
Ref Expression
isdir

Proof of Theorem isdir
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 releq 4959 . . . 4
2 unieq 4024 . . . . . . . 8
32unieqd 4026 . . . . . . 7
4 isdir.1 . . . . . . 7
53, 4syl6eqr 2486 . . . . . 6
65reseq2d 5146 . . . . 5
7 id 20 . . . . 5
86, 7sseq12d 3377 . . . 4
91, 8anbi12d 692 . . 3
107, 7coeq12d 5037 . . . . 5
1110, 7sseq12d 3377 . . . 4
125, 5xpeq12d 4903 . . . . 5
13 cnveq 5046 . . . . . 6
1413, 7coeq12d 5037 . . . . 5
1512, 14sseq12d 3377 . . . 4
1611, 15anbi12d 692 . . 3
179, 16anbi12d 692 . 2
18 df-dir 14675 . 2
1917, 18elab2g 3084 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wceq 1652   wcel 1725   wss 3320  cuni 4015   cid 4493   cxp 4876  ccnv 4877   cres 4880   ccom 4882   wrel 4883  cdir 14673 This theorem is referenced by:  reldir  14678  dirdm  14679  dirref  14680  dirtr  14681  dirge  14682  tsrdir  14683  filnetlem3  26409 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711  df-v 2958  df-in 3327  df-ss 3334  df-uni 4016  df-br 4213  df-opab 4267  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-res 4890  df-dir 14675
 Copyright terms: Public domain W3C validator