Metamath Proof Explorer


Theorem relfld

Description: The double union of a relation is its field. (Contributed by NM, 17-Sep-2006)

Ref Expression
Assertion relfld RelRR=domRranR

Proof

Step Hyp Ref Expression
1 relssdmrn RelRRdomR×ranR
2 uniss RdomR×ranRRdomR×ranR
3 uniss RdomR×ranRRdomR×ranR
4 1 2 3 3syl RelRRdomR×ranR
5 unixpss domR×ranRdomRranR
6 4 5 sstrdi RelRRdomRranR
7 dmrnssfld domRranRR
8 7 a1i RelRdomRranRR
9 6 8 eqssd RelRR=domRranR