Definition df-sup 2154

Description: Define the supremum of class B. It is meaningful when R is a relation that strictly orders A and when the supremum exists. For example, R could be 'less than', A could be the set of real numbers, and B could be the set of all positive reals whose square is less than 2; in this case the supremum is defined as the square root of 2 per sqrval 4729.

Assertion

Ref	Expression
df-sup	⊢ sup(B, A, R) = ∪{x ∈ A∣(∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz))}

Distinct variable group(s):   x,y,z,R   x,A,y,z   x,B,y,z

Detailed syntax breakdown of Definition df-sup

Step	Hyp	Ref	Expression
1		cB	. . 3 class B
2		cA	. . 3 class A
3		cR	. . 3 class R
4	1, 2, 3	csup 2060	. 2 class sup(B, A, R)
5		vx	. . . . . . . . 9 set x
6	5	cv 1089	. . . . . . . 8 class x
7		vy	. . . . . . . . 9 set y
8	7	cv 1089	. . . . . . . 8 class y
9	6, 8, 3	wbr 2054	. . . . . . 7 wff xRy
10	9	wn 1	. . . . . 6 wff ¬ xRy
11	10, 7, 1	wral 1201	. . . . 5 wff ∀y ∈ B ¬ xRy
12	8, 6, 3	wbr 2054	. . . . . . 7 wff yRx
13		vz	. . . . . . . . . 10 set z
14	13	cv 1089	. . . . . . . . 9 class z
15	8, 14, 3	wbr 2054	. . . . . . . 8 wff yRz
16	15, 13, 1	wrex 1202	. . . . . . 7 wff ∃z ∈ B yRz
17	12, 16	wi 2	. . . . . 6 wff (yRx → ∃z ∈ B yRz)
18	17, 7, 2	wral 1201	. . . . 5 wff ∀y ∈ A (yRx → ∃z ∈ B yRz)
19	11, 18	wa 196	. . . 4 wff (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz))
20	19, 5, 2	crab 1204	. . 3 class {x ∈ A∣(∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz))}
21	20	cuni 1919	. 2 class ∪{x ∈ A∣(∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz))}
22	4, 21	wceq 1091	1 wff sup(B, A, R) = ∪{x ∈ A∣(∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz))}

This definition is referenced by:  supeq1 2155  supex 2157  supcl 2159  supub 2160  suplub 2161  supsn 2168

metamath.org