Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jeff Madsen
Logic and set theory
supex2g
Next ⟩
supclt
Metamath Proof Explorer
Ascii
Unicode
Theorem
supex2g
Description:
Existence of supremum.
(Contributed by
Jeff Madsen
, 2-Sep-2009)
Ref
Expression
Assertion
supex2g
⊢
A
∈
C
→
sup
B
A
R
∈
V
Proof
Step
Hyp
Ref
Expression
1
df-sup
⊢
sup
B
A
R
=
⋃
x
∈
A
|
∀
y
∈
B
¬
x
R
y
∧
∀
y
∈
A
y
R
x
→
∃
z
∈
B
y
R
z
2
rabexg
⊢
A
∈
C
→
x
∈
A
|
∀
y
∈
B
¬
x
R
y
∧
∀
y
∈
A
y
R
x
→
∃
z
∈
B
y
R
z
∈
V
3
2
uniexd
⊢
A
∈
C
→
⋃
x
∈
A
|
∀
y
∈
B
¬
x
R
y
∧
∀
y
∈
A
y
R
x
→
∃
z
∈
B
y
R
z
∈
V
4
1
3
eqeltrid
⊢
A
∈
C
→
sup
B
A
R
∈
V