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 R \to {R ↾}_{⋃ ⋃ R} = R$

Proof

Step	Hyp	Ref	Expression
1		relfld	$⊢ Rel R \to ⋃ ⋃ R = dom R \cup ran R$
2	1	reseq2d	$⊢ Rel R \to {R ↾}_{⋃ ⋃ R} = {R ↾}_{(dom R \cup ran R)}$
3		resundi	$⊢ {R ↾}_{(dom R \cup ran R)} = ({R ↾}_{dom R}) \cup ({R ↾}_{ran R})$
4		eqtr	$⊢ ({R ↾}_{⋃ ⋃ R} = {R ↾}_{(dom R \cup ran R)} \land {R ↾}_{(dom R \cup ran R)} = ({R ↾}_{dom R}) \cup ({R ↾}_{ran R})) \to {R ↾}_{⋃ ⋃ R} = ({R ↾}_{dom R}) \cup ({R ↾}_{ran R})$
5		resss	$⊢ {R ↾}_{ran R} \subseteq R$
6		resdm	$⊢ Rel R \to {R ↾}_{dom R} = R$
7		ssequn2	$⊢ {R ↾}_{ran R} \subseteq R \leftrightarrow R \cup ({R ↾}_{ran R}) = R$
8		uneq1	$⊢ {R ↾}_{dom R} = R \to ({R ↾}_{dom R}) \cup ({R ↾}_{ran R}) = R \cup ({R ↾}_{ran R})$
9	8	eqeq2d	$⊢ {R ↾}_{dom R} = R \to ({R ↾}_{⋃ ⋃ R} = ({R ↾}_{dom R}) \cup ({R ↾}_{ran R}) \leftrightarrow {R ↾}_{⋃ ⋃ R} = R \cup ({R ↾}_{ran R}))$
10		eqtr	$⊢ ({R ↾}_{⋃ ⋃ R} = R \cup ({R ↾}_{ran R}) \land R \cup ({R ↾}_{ran R}) = R) \to {R ↾}_{⋃ ⋃ R} = R$
11	10	ex	$⊢ {R ↾}_{⋃ ⋃ R} = R \cup ({R ↾}_{ran R}) \to (R \cup ({R ↾}_{ran R}) = R \to {R ↾}_{⋃ ⋃ R} = R)$
12	9 11	biimtrdi	$⊢ {R ↾}_{dom R} = R \to ({R ↾}_{⋃ ⋃ R} = ({R ↾}_{dom R}) \cup ({R ↾}_{ran R}) \to (R \cup ({R ↾}_{ran R}) = R \to {R ↾}_{⋃ ⋃ R} = R))$
13	12	com3r	$⊢ R \cup ({R ↾}_{ran R}) = R \to ({R ↾}_{dom R} = R \to ({R ↾}_{⋃ ⋃ R} = ({R ↾}_{dom R}) \cup ({R ↾}_{ran R}) \to {R ↾}_{⋃ ⋃ R} = R))$
14	7 13	sylbi	$⊢ {R ↾}_{ran R} \subseteq R \to ({R ↾}_{dom R} = R \to ({R ↾}_{⋃ ⋃ R} = ({R ↾}_{dom R}) \cup ({R ↾}_{ran R}) \to {R ↾}_{⋃ ⋃ R} = R))$
15	5 6 14	mpsyl	$⊢ Rel R \to ({R ↾}_{⋃ ⋃ R} = ({R ↾}_{dom R}) \cup ({R ↾}_{ran R}) \to {R ↾}_{⋃ ⋃ R} = R)$
16	4 15	syl5com	$⊢ ({R ↾}_{⋃ ⋃ R} = {R ↾}_{(dom R \cup ran R)} \land {R ↾}_{(dom R \cup ran R)} = ({R ↾}_{dom R}) \cup ({R ↾}_{ran R})) \to (Rel R \to {R ↾}_{⋃ ⋃ R} = R)$
17	2 3 16	sylancl	$⊢ Rel R \to (Rel R \to {R ↾}_{⋃ ⋃ R} = R)$
18	17	pm2.43i	$⊢ Rel R \to {R ↾}_{⋃ ⋃ R} = R$