Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Weak dominance
relwdom
Next ⟩
brwdom
Metamath Proof Explorer
Ascii
Unicode
Theorem
relwdom
Description:
Weak dominance is a relation.
(Contributed by
Stefan O'Rear
, 11-Feb-2015)
Ref
Expression
Assertion
relwdom
⊢
Rel
⁡
≼
*
Proof
Step
Hyp
Ref
Expression
1
df-wdom
⊢
≼
*
=
x
y
|
x
=
∅
∨
∃
z
z
:
y
⟶
onto
x
2
1
relopabi
⊢
Rel
⁡
≼
*