Metamath Proof Explorer

Theorem isores3

Description: Induced isomorphism on a subset. (Contributed by Stefan O'Rear, 5-Nov-2014)

Ref Expression
Assertion isores3 
|- ( ( H Isom R , S ( A , B ) /\ K C_ A /\ X = ( H " K ) ) -> ( H |` K ) Isom R , S ( K , X ) )

Proof

Step Hyp Ref Expression
1 f1of1 
 |-  ( H : A -1-1-onto-> B -> H : A -1-1-> B )
2 f1ores 
 |-  ( ( H : A -1-1-> B /\ K C_ A ) -> ( H |` K ) : K -1-1-onto-> ( H " K ) )
3 2 expcom 
 |-  ( K C_ A -> ( H : A -1-1-> B -> ( H |` K ) : K -1-1-onto-> ( H " K ) ) )
4 1 3 syl5 
 |-  ( K C_ A -> ( H : A -1-1-onto-> B -> ( H |` K ) : K -1-1-onto-> ( H " K ) ) )
5 ssralv 
 |-  ( K C_ A -> ( A. a e. A A. b e. A ( a R b <-> ( H ` a ) S ( H ` b ) ) -> A. a e. K A. b e. A ( a R b <-> ( H ` a ) S ( H ` b ) ) ) )
6 ssralv 
 |-  ( K C_ A -> ( A. b e. A ( a R b <-> ( H ` a ) S ( H ` b ) ) -> A. b e. K ( a R b <-> ( H ` a ) S ( H ` b ) ) ) )
7 6 adantr 
 |-  ( ( K C_ A /\ a e. K ) -> ( A. b e. A ( a R b <-> ( H ` a ) S ( H ` b ) ) -> A. b e. K ( a R b <-> ( H ` a ) S ( H ` b ) ) ) )
8 fvres 
 |-  ( a e. K -> ( ( H |` K ) ` a ) = ( H ` a ) )
9 fvres 
 |-  ( b e. K -> ( ( H |` K ) ` b ) = ( H ` b ) )
10 8 9 breqan12d 
 |-  ( ( a e. K /\ b e. K ) -> ( ( ( H |` K ) ` a ) S ( ( H |` K ) ` b ) <-> ( H ` a ) S ( H ` b ) ) )
11 10 adantll 
 |-  ( ( ( K C_ A /\ a e. K ) /\ b e. K ) -> ( ( ( H |` K ) ` a ) S ( ( H |` K ) ` b ) <-> ( H ` a ) S ( H ` b ) ) )
12 11 bibi2d 
 |-  ( ( ( K C_ A /\ a e. K ) /\ b e. K ) -> ( ( a R b <-> ( ( H |` K ) ` a ) S ( ( H |` K ) ` b ) ) <-> ( a R b <-> ( H ` a ) S ( H ` b ) ) ) )
13 12 biimprd 
 |-  ( ( ( K C_ A /\ a e. K ) /\ b e. K ) -> ( ( a R b <-> ( H ` a ) S ( H ` b ) ) -> ( a R b <-> ( ( H |` K ) ` a ) S ( ( H |` K ) ` b ) ) ) )
14 13 ralimdva 
 |-  ( ( K C_ A /\ a e. K ) -> ( A. b e. K ( a R b <-> ( H ` a ) S ( H ` b ) ) -> A. b e. K ( a R b <-> ( ( H |` K ) ` a ) S ( ( H |` K ) ` b ) ) ) )
15 7 14 syld 
 |-  ( ( K C_ A /\ a e. K ) -> ( A. b e. A ( a R b <-> ( H ` a ) S ( H ` b ) ) -> A. b e. K ( a R b <-> ( ( H |` K ) ` a ) S ( ( H |` K ) ` b ) ) ) )
16 15 ralimdva 
 |-  ( K C_ A -> ( A. a e. K A. b e. A ( a R b <-> ( H ` a ) S ( H ` b ) ) -> A. a e. K A. b e. K ( a R b <-> ( ( H |` K ) ` a ) S ( ( H |` K ) ` b ) ) ) )
17 5 16 syld 
 |-  ( K C_ A -> ( A. a e. A A. b e. A ( a R b <-> ( H ` a ) S ( H ` b ) ) -> A. a e. K A. b e. K ( a R b <-> ( ( H |` K ) ` a ) S ( ( H |` K ) ` b ) ) ) )
18 4 17 anim12d 
 |-  ( K C_ A -> ( ( H : A -1-1-onto-> B /\ A. a e. A A. b e. A ( a R b <-> ( H ` a ) S ( H ` b ) ) ) -> ( ( H |` K ) : K -1-1-onto-> ( H " K ) /\ A. a e. K A. b e. K ( a R b <-> ( ( H |` K ) ` a ) S ( ( H |` K ) ` b ) ) ) ) )
19 df-isom 
 |-  ( H Isom R , S ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. a e. A A. b e. A ( a R b <-> ( H ` a ) S ( H ` b ) ) ) )
20 df-isom 
 |-  ( ( H |` K ) Isom R , S ( K , ( H " K ) ) <-> ( ( H |` K ) : K -1-1-onto-> ( H " K ) /\ A. a e. K A. b e. K ( a R b <-> ( ( H |` K ) ` a ) S ( ( H |` K ) ` b ) ) ) )
21 18 19 20 3imtr4g 
 |-  ( K C_ A -> ( H Isom R , S ( A , B ) -> ( H |` K ) Isom R , S ( K , ( H " K ) ) ) )
22 21 impcom 
 |-  ( ( H Isom R , S ( A , B ) /\ K C_ A ) -> ( H |` K ) Isom R , S ( K , ( H " K ) ) )
23 isoeq5 
 |-  ( X = ( H " K ) -> ( ( H |` K ) Isom R , S ( K , X ) <-> ( H |` K ) Isom R , S ( K , ( H " K ) ) ) )
24 22 23 syl5ibrcom 
 |-  ( ( H Isom R , S ( A , B ) /\ K C_ A ) -> ( X = ( H " K ) -> ( H |` K ) Isom R , S ( K , X ) ) )
25 24 3impia 
 |-  ( ( H Isom R , S ( A , B ) /\ K C_ A /\ X = ( H " K ) ) -> ( H |` K ) Isom R , S ( K , X ) )