Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Supremum and infimum
infnlb
Next ⟩
infex
Metamath Proof Explorer
Ascii
Unicode
Theorem
infnlb
Description:
A lower bound is not greater than the infimum.
(Contributed by
AV
, 3-Sep-2020)
Ref
Expression
Hypotheses
infcl.1
⊢
φ
→
R
Or
A
infcl.2
⊢
φ
→
∃
x
∈
A
∀
y
∈
B
¬
y
R
x
∧
∀
y
∈
A
x
R
y
→
∃
z
∈
B
z
R
y
Assertion
infnlb
⊢
φ
→
C
∈
A
∧
∀
z
∈
B
¬
z
R
C
→
¬
sup
B
A
R
R
C
Proof
Step
Hyp
Ref
Expression
1
infcl.1
⊢
φ
→
R
Or
A
2
infcl.2
⊢
φ
→
∃
x
∈
A
∀
y
∈
B
¬
y
R
x
∧
∀
y
∈
A
x
R
y
→
∃
z
∈
B
z
R
y
3
1
2
infglb
⊢
φ
→
C
∈
A
∧
sup
B
A
R
R
C
→
∃
z
∈
B
z
R
C
4
3
expdimp
⊢
φ
∧
C
∈
A
→
sup
B
A
R
R
C
→
∃
z
∈
B
z
R
C
5
dfrex2
⊢
∃
z
∈
B
z
R
C
↔
¬
∀
z
∈
B
¬
z
R
C
6
4
5
syl6ib
⊢
φ
∧
C
∈
A
→
sup
B
A
R
R
C
→
¬
∀
z
∈
B
¬
z
R
C
7
6
con2d
⊢
φ
∧
C
∈
A
→
∀
z
∈
B
¬
z
R
C
→
¬
sup
B
A
R
R
C
8
7
expimpd
⊢
φ
→
C
∈
A
∧
∀
z
∈
B
¬
z
R
C
→
¬
sup
B
A
R
R
C