Theorem relfld

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

	Ref	Expression
Assertion	relfld	⊢ ( Rel 𝑅 → ∪ ∪ 𝑅 = ( dom 𝑅 ∪ ran 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		relssdmrn	⊢ ( Rel 𝑅 → 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) )
2		uniss	⊢ ( 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) → ∪ 𝑅 ⊆ ∪ ( dom 𝑅 × ran 𝑅 ) )
3		uniss	⊢ ( ∪ 𝑅 ⊆ ∪ ( dom 𝑅 × ran 𝑅 ) → ∪ ∪ 𝑅 ⊆ ∪ ∪ ( dom 𝑅 × ran 𝑅 ) )
4	1 2 3	3syl	⊢ ( Rel 𝑅 → ∪ ∪ 𝑅 ⊆ ∪ ∪ ( dom 𝑅 × ran 𝑅 ) )
5		unixpss	⊢ ∪ ∪ ( dom 𝑅 × ran 𝑅 ) ⊆ ( dom 𝑅 ∪ ran 𝑅 )
6	4 5	sstrdi	⊢ ( Rel 𝑅 → ∪ ∪ 𝑅 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
7		dmrnssfld	⊢ ( dom 𝑅 ∪ ran 𝑅 ) ⊆ ∪ ∪ 𝑅
8	7	a1i	⊢ ( Rel 𝑅 → ( dom 𝑅 ∪ ran 𝑅 ) ⊆ ∪ ∪ 𝑅 )
9	6 8	eqssd	⊢ ( Rel 𝑅 → ∪ ∪ 𝑅 = ( dom 𝑅 ∪ ran 𝑅 ) )