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

Metamath Proof Explorer

Theorem isose

Description: An isomorphism preserves set-like relations. (Contributed by Mario Carneiro, 23-Jun-2015)

Ref Expression
Assertion isose ⊢ H Isom R , S A B → R Se A ↔ S Se B

Proof

Step Hyp Ref Expression
1 id ⊢ H Isom R , S A B → H Isom R , S A B
2 isof1o ⊢ H Isom R , S A B → H : A ⟶ 1-1 onto B
3 f1ofun ⊢ H : A ⟶ 1-1 onto B → Fun ⁡ H
4 vex ⊢ x ∈ V
5 4 funimaex ⊢ Fun ⁡ H → H x ∈ V
6 2 3 5 3syl ⊢ H Isom R , S A B → H x ∈ V
7 1 6 isoselem ⊢ H Isom R , S A B → R Se A → S Se B
8 isocnv ⊢ H Isom R , S A B → H -1 Isom S , R B A
9 isof1o ⊢ H -1 Isom S , R B A → H -1 : B ⟶ 1-1 onto A
10 f1ofun ⊢ H -1 : B ⟶ 1-1 onto A → Fun ⁡ H -1
11 4 funimaex ⊢ Fun ⁡ H -1 → H -1 x ∈ V
12 8 9 10 11 4syl ⊢ H Isom R , S A B → H -1 x ∈ V
13 8 12 isoselem ⊢ H Isom R , S A B → S Se B → R Se A
14 7 13 impbid ⊢ H Isom R , S A B → R Se A ↔ S Se B