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 e. _V
5 4 funimaex 
 |-  ( Fun H -> ( H " x ) e. _V )
6 2 3 5 3syl 
 |-  ( H Isom R , S ( A , B ) -> ( H " x ) e. _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 Isom S , R ( B , A ) )
9 isof1o 
 |-  ( `' H Isom S , R ( B , A ) -> `' H : B -1-1-onto-> A )
10 f1ofun 
 |-  ( `' H : B -1-1-onto-> A -> Fun `' H )
11 4 funimaex 
 |-  ( Fun `' H -> ( `' H " x ) e. _V )
12 8 9 10 11 4syl 
 |-  ( H Isom R , S ( A , B ) -> ( `' H " x ) e. _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 ) )