isoid

Description: Identity law for isomorphism. Proposition 6.30(1) of TakeutiZaring p. 33. (Contributed by NM, 27-Apr-2004)

		Ref	Expression
	Assertion	isoid	$⊢ ({I ↾}_{A}) {Isom}_{R, R} (A, A)$

Step	Hyp	Ref	Expression
1		f1oi	$⊢ ({I ↾}_{A}) : A \underset{1-1 onto}{⟶} A$
2		fvresi	$⊢ x \in A \to ({I ↾}_{A}) (x) = x$
3		fvresi	$⊢ y \in A \to ({I ↾}_{A}) (y) = y$
4	2 3	breqan12d	$⊢ (x \in A \land y \in A) \to (({I ↾}_{A}) (x) R ({I ↾}_{A}) (y) \leftrightarrow x R y)$
5	4	bicomd	$⊢ (x \in A \land y \in A) \to (x R y \leftrightarrow ({I ↾}_{A}) (x) R ({I ↾}_{A}) (y))$
6	5	rgen2	$⊢ \forall x \in A \forall y \in A (x R y \leftrightarrow ({I ↾}_{A}) (x) R ({I ↾}_{A}) (y))$
7		df-isom	$⊢ ({I ↾}_{A}) {Isom}_{R, R} (A, A) \leftrightarrow (({I ↾}_{A}) : A \underset{1-1 onto}{⟶} A \land \forall x \in A \forall y \in A (x R y \leftrightarrow ({I ↾}_{A}) (x) R ({I ↾}_{A}) (y)))$
8	1 6 7	mpbir2an	$⊢ ({I ↾}_{A}) {Isom}_{R, R} (A, A)$

Metamath Proof Explorer