isorel

Description: An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004)

		Ref	Expression
	Assertion	isorel	$⊢ (H {Isom}_{R, S} (A, B) \land (C \in A \land D \in A)) \to (C R D \leftrightarrow H (C) S H (D))$

Step	Hyp	Ref	Expression
1		df-isom	$⊢ H {Isom}_{R, S} (A, B) \leftrightarrow (H : A \underset{1-1 onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \leftrightarrow H (x) S H (y)))$
2	1	simprbi	$⊢ H {Isom}_{R, S} (A, B) \to \forall x \in A \forall y \in A (x R y \leftrightarrow H (x) S H (y))$
3		breq1	$⊢ x = C \to (x R y \leftrightarrow C R y)$
4		fveq2	$⊢ x = C \to H (x) = H (C)$
5	4	breq1d	$⊢ x = C \to (H (x) S H (y) \leftrightarrow H (C) S H (y))$
6	3 5	bibi12d	$⊢ x = C \to ((x R y \leftrightarrow H (x) S H (y)) \leftrightarrow (C R y \leftrightarrow H (C) S H (y)))$
7		breq2	$⊢ y = D \to (C R y \leftrightarrow C R D)$
8		fveq2	$⊢ y = D \to H (y) = H (D)$
9	8	breq2d	$⊢ y = D \to (H (C) S H (y) \leftrightarrow H (C) S H (D))$
10	7 9	bibi12d	$⊢ y = D \to ((C R y \leftrightarrow H (C) S H (y)) \leftrightarrow (C R D \leftrightarrow H (C) S H (D)))$
11	6 10	rspc2v	$⊢ (C \in A \land D \in A) \to (\forall x \in A \forall y \in A (x R y \leftrightarrow H (x) S H (y)) \to (C R D \leftrightarrow H (C) S H (D)))$
12	2 11	mpan9	$⊢ (H {Isom}_{R, S} (A, B) \land (C \in A \land D \in A)) \to (C R D \leftrightarrow H (C) S H (D))$

Metamath Proof Explorer