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

Theorem dirge 15713
 Description: For any two elements of a directed set, there exists a third element greater than or equal to both. (Note that this does not say that the two elements have a least upper bound.) (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.)
Hypothesis
Ref Expression
dirge.1
Assertion
Ref Expression
dirge
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem dirge
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dirge.1 . . . . . . 7
2 dirdm 15710 . . . . . . 7
31, 2syl5eq 2513 . . . . . 6
43eleq2d 2530 . . . . 5
53eleq2d 2530 . . . . 5
64, 5anbi12d 710 . . . 4
7 eqid 2460 . . . . . . . . . 10
87isdir 15708 . . . . . . . . 9
98ibi 241 . . . . . . . 8
109simprd 463 . . . . . . 7
1110simprd 463 . . . . . 6
12 codir 5378 . . . . . 6
1311, 12sylib 196 . . . . 5
14 breq1 4443 . . . . . . . 8
1514anbi1d 704 . . . . . . 7
1615exbidv 1685 . . . . . 6
17 breq1 4443 . . . . . . . 8
1817anbi2d 703 . . . . . . 7
1918exbidv 1685 . . . . . 6
2016, 19rspc2v 3216 . . . . 5
2113, 20syl5com 30 . . . 4
226, 21sylbid 215 . . 3
23 reldir 15709 . . . . . . . . . 10
24 relelrn 5227 . . . . . . . . . 10
2523, 24sylan 471 . . . . . . . . 9
2625ex 434 . . . . . . . 8
27 ssun2 3661 . . . . . . . . . . 11
28 dmrnssfld 5252 . . . . . . . . . . 11
2927, 28sstri 3506 . . . . . . . . . 10
3029, 3syl5sseqr 3546 . . . . . . . . 9
3130sseld 3496 . . . . . . . 8
3226, 31syld 44 . . . . . . 7
3332adantrd 468 . . . . . 6
3433ancrd 554 . . . . 5
3534eximdv 1681 . . . 4
36 df-rex 2813 . . . 4
3735, 36syl6ibr 227 . . 3
3822, 37syld 44 . 2
39383impib 1189 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   w3a 968   wceq 1374  wex 1591   wcel 1762  wral 2807  wrex 2808   cun 3467   wss 3469  cuni 4238   class class class wbr 4440   cid 4783   cxp 4990  ccnv 4991   cdm 4992   crn 4993   cres 4994   ccom 4996   wrel 4997  cdir 15704 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-dir 15706 This theorem is referenced by:  tailfb  29785
 Copyright terms: Public domain W3C validator