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 𝑅 → ( 𝑅 ↾ ∪ ∪ 𝑅 ) = 𝑅 )