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

Metamath Proof Explorer

Theorem relresfld

Description: Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012)

Ref Expression
Assertion relresfld ( Rel 𝑅 → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = 𝑅 )

Proof

Step Hyp Ref Expression
1 relfld ⊢ ( Rel 𝑅 → ∪ ∪ 𝑅 = ( dom 𝑅 ∪ ran 𝑅 ) )
2 1 reseq2d ⊢ ( Rel 𝑅 → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = ( 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
3 resundi ⊢ ( 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( ( 𝑅 ↾ dom 𝑅 ) ∪ ( 𝑅 ↾ ran 𝑅 ) )
4 eqtr ⊢ ( ( ( 𝑅 ↾ ∪ ∪ 𝑅 ) = ( 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∧ ( 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( ( 𝑅 ↾ dom 𝑅 ) ∪ ( 𝑅 ↾ ran 𝑅 ) ) ) → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = ( ( 𝑅 ↾ dom 𝑅 ) ∪ ( 𝑅 ↾ ran 𝑅 ) ) )
5 resss ⊢ ( 𝑅 ↾ ran 𝑅 ) ⊆ 𝑅
6 resdm ⊢ ( Rel 𝑅 → ( 𝑅 ↾ dom 𝑅 ) = 𝑅 )
7 ssequn2 ⊢ ( ( 𝑅 ↾ ran 𝑅 ) ⊆ 𝑅 ↔ ( 𝑅 ∪ ( 𝑅 ↾ ran 𝑅 ) ) = 𝑅 )
8 uneq1 ⊢ ( ( 𝑅 ↾ dom 𝑅 ) = 𝑅 → ( ( 𝑅 ↾ dom 𝑅 ) ∪ ( 𝑅 ↾ ran 𝑅 ) ) = ( 𝑅 ∪ ( 𝑅 ↾ ran 𝑅 ) ) )
9 8 eqeq2d ⊢ ( ( 𝑅 ↾ dom 𝑅 ) = 𝑅 → ( ( 𝑅 ↾ ∪ ∪ 𝑅 ) = ( ( 𝑅 ↾ dom 𝑅 ) ∪ ( 𝑅 ↾ ran 𝑅 ) ) ↔ ( 𝑅 ↾ ∪ ∪ 𝑅 ) = ( 𝑅 ∪ ( 𝑅 ↾ ran 𝑅 ) ) ) )
10 eqtr ⊢ ( ( ( 𝑅 ↾ ∪ ∪ 𝑅 ) = ( 𝑅 ∪ ( 𝑅 ↾ ran 𝑅 ) ) ∧ ( 𝑅 ∪ ( 𝑅 ↾ ran 𝑅 ) ) = 𝑅 ) → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = 𝑅 )
11 10 ex ⊢ ( ( 𝑅 ↾ ∪ ∪ 𝑅 ) = ( 𝑅 ∪ ( 𝑅 ↾ ran 𝑅 ) ) → ( ( 𝑅 ∪ ( 𝑅 ↾ ran 𝑅 ) ) = 𝑅 → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = 𝑅 ) )
12 9 11 biimtrdi ⊢ ( ( 𝑅 ↾ dom 𝑅 ) = 𝑅 → ( ( 𝑅 ↾ ∪ ∪ 𝑅 ) = ( ( 𝑅 ↾ dom 𝑅 ) ∪ ( 𝑅 ↾ ran 𝑅 ) ) → ( ( 𝑅 ∪ ( 𝑅 ↾ ran 𝑅 ) ) = 𝑅 → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = 𝑅 ) ) )
13 12 com3r ⊢ ( ( 𝑅 ∪ ( 𝑅 ↾ ran 𝑅 ) ) = 𝑅 → ( ( 𝑅 ↾ dom 𝑅 ) = 𝑅 → ( ( 𝑅 ↾ ∪ ∪ 𝑅 ) = ( ( 𝑅 ↾ dom 𝑅 ) ∪ ( 𝑅 ↾ ran 𝑅 ) ) → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = 𝑅 ) ) )
14 7 13 sylbi ⊢ ( ( 𝑅 ↾ ran 𝑅 ) ⊆ 𝑅 → ( ( 𝑅 ↾ dom 𝑅 ) = 𝑅 → ( ( 𝑅 ↾ ∪ ∪ 𝑅 ) = ( ( 𝑅 ↾ dom 𝑅 ) ∪ ( 𝑅 ↾ ran 𝑅 ) ) → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = 𝑅 ) ) )
15 5 6 14 mpsyl ⊢ ( Rel 𝑅 → ( ( 𝑅 ↾ ∪ ∪ 𝑅 ) = ( ( 𝑅 ↾ dom 𝑅 ) ∪ ( 𝑅 ↾ ran 𝑅 ) ) → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = 𝑅 ) )
16 4 15 syl5com ⊢ ( ( ( 𝑅 ↾ ∪ ∪ 𝑅 ) = ( 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∧ ( 𝑅 ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) = ( ( 𝑅 ↾ dom 𝑅 ) ∪ ( 𝑅 ↾ ran 𝑅 ) ) ) → ( Rel 𝑅 → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = 𝑅 ) )
17 2 3 16 sylancl ⊢ ( Rel 𝑅 → ( Rel 𝑅 → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = 𝑅 ) )
18 17 pm2.43i ⊢ ( Rel 𝑅 → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = 𝑅 )