This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 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 𝑅 ) )