This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ∧ C ∈ A ∧ D ∈ A → C R D ↔ H ⁡ C S H ⁡ D

Proof

Step Hyp Ref Expression
1 df-isom ⊢ H Isom R , S A B ↔ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y
2 1 simprbi ⊢ H Isom R , S A B → ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y
3 breq1 ⊢ x = C → x R y ↔ C R y
4 fveq2 ⊢ x = C → H ⁡ x = H ⁡ C
5 4 breq1d ⊢ x = C → H ⁡ x S H ⁡ y ↔ H ⁡ C S H ⁡ y
6 3 5 bibi12d ⊢ x = C → x R y ↔ H ⁡ x S H ⁡ y ↔ C R y ↔ H ⁡ C S H ⁡ y
7 breq2 ⊢ y = D → C R y ↔ C R D
8 fveq2 ⊢ y = D → H ⁡ y = H ⁡ D
9 8 breq2d ⊢ y = D → H ⁡ C S H ⁡ y ↔ H ⁡ C S H ⁡ D
10 7 9 bibi12d ⊢ y = D → C R y ↔ H ⁡ C S H ⁡ y ↔ C R D ↔ H ⁡ C S H ⁡ D
11 6 10 rspc2v ⊢ C ∈ A ∧ D ∈ A → ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y → C R D ↔ H ⁡ C S H ⁡ D
12 2 11 mpan9 ⊢ H Isom R , S A B ∧ C ∈ A ∧ D ∈ A → C R D ↔ H ⁡ C S H ⁡ D