Metamath Proof Explorer

Definition df-sup

Description: Define the supremum of class A . It is meaningful when R is a relation that strictly orders B and when the supremum exists. For example, R could be 'less than', B could be the set of real numbers, and A 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 sqrtval . See dfsup2 for alternate definition not requiring dummy variables. (Contributed by NM, 22-May-1999)

Ref Expression
Assertion df-sup ⊢ sup A B R = ⋃ x ∈ B | ∀ y ∈ A ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ A y R z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cB class B
2 cR class R
3 0 1 2 csup class sup A B R
4 vx setvar x
5 vy setvar y
6 4 cv setvar x
7 5 cv setvar y
8 6 7 2 wbr wff x R y
9 8 wn wff ¬ x R y
10 9 5 0 wral wff ∀ y ∈ A ¬ x R y
11 7 6 2 wbr wff y R x
12 vz setvar z
13 12 cv setvar z
14 7 13 2 wbr wff y R z
15 14 12 0 wrex wff ∃ z ∈ A y R z
16 11 15 wi wff y R x → ∃ z ∈ A y R z
17 16 5 1 wral wff ∀ y ∈ B y R x → ∃ z ∈ A y R z
18 10 17 wa wff ∀ y ∈ A ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ A y R z
19 18 4 1 crab class x ∈ B | ∀ y ∈ A ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ A y R z
20 19 cuni class ⋃ x ∈ B | ∀ y ∈ A ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ A y R z
21 3 20 wceq wff sup A B R = ⋃ x ∈ B | ∀ y ∈ A ¬ x R y ∧ ∀ y ∈ B y R x → ∃ z ∈ A y R z