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

Definition df-spw 14636
 Description: Define suprema under weak orderings. Unlike df-sup 7449 for strong orderings, is evaluates to a member of the field of iff the supremum exists. Read as the -supremum of set . (Contributed by NM, 13-May-2008.)
Assertion
Ref Expression
df-spw
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-spw
StepHypRef Expression
1 cspw 14631 . 2
2 vr . . 3
3 vx . . 3
4 cps 14629 . . 3
5 cvv 2958 . . 3
6 vz . . . . . . . 8
76cv 1652 . . . . . . 7
8 vy . . . . . . . 8
98cv 1652 . . . . . . 7
102cv 1652 . . . . . . 7
117, 9, 10wbr 4215 . . . . . 6
123cv 1652 . . . . . 6
1311, 6, 12wral 2707 . . . . 5
14 vw . . . . . . . . . 10
1514cv 1652 . . . . . . . . 9
1615, 7, 10wbr 4215 . . . . . . . 8
1716, 14, 12wral 2707 . . . . . . 7
189, 7, 10wbr 4215 . . . . . . 7
1917, 18wi 4 . . . . . 6
2010cuni 4017 . . . . . . 7
2120cuni 4017 . . . . . 6
2219, 6, 21wral 2707 . . . . 5
2313, 22wa 360 . . . 4
2423, 8, 21crio 6545 . . 3
252, 3, 4, 5, 24cmpt2 6086 . 2
261, 25wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  spwval2  14661
 Copyright terms: Public domain W3C validator