Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Relations
somin2
Next ⟩
soltmin
Metamath Proof Explorer
Ascii
Unicode
Theorem
somin2
Description:
Property of a minimum in a strict order.
(Contributed by
Stefan O'Rear
, 17-Jan-2015)
Ref
Expression
Assertion
somin2
⊢
R
Or
X
∧
A
∈
X
∧
B
∈
X
→
if
A
R
B
A
B
R
∪
I
B
Proof
Step
Hyp
Ref
Expression
1
somincom
⊢
R
Or
X
∧
A
∈
X
∧
B
∈
X
→
if
A
R
B
A
B
=
if
B
R
A
B
A
2
somin1
⊢
R
Or
X
∧
B
∈
X
∧
A
∈
X
→
if
B
R
A
B
A
R
∪
I
B
3
2
ancom2s
⊢
R
Or
X
∧
A
∈
X
∧
B
∈
X
→
if
B
R
A
B
A
R
∪
I
B
4
1
3
eqbrtrd
⊢
R
Or
X
∧
A
∈
X
∧
B
∈
X
→
if
A
R
B
A
B
R
∪
I
B