residpr

Description: Restriction of the identity to a pair. (Contributed by AV, 11-Dec-2018)

		Ref	Expression
	Assertion	residpr	$⊢ (A \in V \land B \in W) \to {I ↾}_{\{A, B\}} = \{⟨A, A⟩, ⟨B, B⟩\}$

Step	Hyp	Ref	Expression
1		df-pr	$⊢ \{A, B\} = \{A\} \cup \{B\}$
2	1	reseq2i	$⊢ {I ↾}_{\{A, B\}} = {I ↾}_{(\{A\} \cup \{B\})}$
3		resundi	$⊢ {I ↾}_{(\{A\} \cup \{B\})} = ({I ↾}_{\{A\}}) \cup ({I ↾}_{\{B\}})$
4	2 3	eqtri	$⊢ {I ↾}_{\{A, B\}} = ({I ↾}_{\{A\}}) \cup ({I ↾}_{\{B\}})$
5		xpsng	$⊢ (A \in V \land A \in V) \to \{A\} \times \{A\} = \{⟨A, A⟩\}$
6	5	anidms	$⊢ A \in V \to \{A\} \times \{A\} = \{⟨A, A⟩\}$
7	6	adantr	$⊢ (A \in V \land B \in W) \to \{A\} \times \{A\} = \{⟨A, A⟩\}$
8		xpsng	$⊢ (B \in W \land B \in W) \to \{B\} \times \{B\} = \{⟨B, B⟩\}$
9	8	anidms	$⊢ B \in W \to \{B\} \times \{B\} = \{⟨B, B⟩\}$
10	9	adantl	$⊢ (A \in V \land B \in W) \to \{B\} \times \{B\} = \{⟨B, B⟩\}$
11	7 10	uneq12d	$⊢ (A \in V \land B \in W) \to (\{A\} \times \{A\}) \cup (\{B\} \times \{B\}) = \{⟨A, A⟩\} \cup \{⟨B, B⟩\}$
12		restidsing	$⊢ {I ↾}_{\{A\}} = \{A\} \times \{A\}$
13		restidsing	$⊢ {I ↾}_{\{B\}} = \{B\} \times \{B\}$
14	12 13	uneq12i	$⊢ ({I ↾}_{\{A\}}) \cup ({I ↾}_{\{B\}}) = (\{A\} \times \{A\}) \cup (\{B\} \times \{B\})$
15		df-pr	$⊢ \{⟨A, A⟩, ⟨B, B⟩\} = \{⟨A, A⟩\} \cup \{⟨B, B⟩\}$
16	11 14 15	3eqtr4g	$⊢ (A \in V \land B \in W) \to ({I ↾}_{\{A\}}) \cup ({I ↾}_{\{B\}}) = \{⟨A, A⟩, ⟨B, B⟩\}$
17	4 16	eqtrid	$⊢ (A \in V \land B \in W) \to {I ↾}_{\{A, B\}} = \{⟨A, A⟩, ⟨B, B⟩\}$

Metamath Proof Explorer