Metamath Proof Explorer

Theorem resthauslem

Description: Lemma for resthaus and similar theorems. If the topological property A is preserved under injective preimages, then property A passes to subspaces. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypotheses resthauslem.1 
|- ( J e. A -> J e. Top )
resthauslem.2 
|- ( ( J e. A /\ ( _I |` ( S i^i U. J ) ) : ( S i^i U. J ) -1-1-> ( S i^i U. J ) /\ ( _I |` ( S i^i U. J ) ) e. ( ( J |`t S ) Cn J ) ) -> ( J |`t S ) e. A )
Assertion resthauslem 
|- ( ( J e. A /\ S e. V ) -> ( J |`t S ) e. A )

Proof

Step Hyp Ref Expression
1 resthauslem.1 
 |-  ( J e. A -> J e. Top )
2 resthauslem.2 
 |-  ( ( J e. A /\ ( _I |` ( S i^i U. J ) ) : ( S i^i U. J ) -1-1-> ( S i^i U. J ) /\ ( _I |` ( S i^i U. J ) ) e. ( ( J |`t S ) Cn J ) ) -> ( J |`t S ) e. A )
3 simpl 
 |-  ( ( J e. A /\ S e. V ) -> J e. A )
4 f1oi 
 |-  ( _I |` ( S i^i U. J ) ) : ( S i^i U. J ) -1-1-onto-> ( S i^i U. J )
5 f1of1 
 |-  ( ( _I |` ( S i^i U. J ) ) : ( S i^i U. J ) -1-1-onto-> ( S i^i U. J ) -> ( _I |` ( S i^i U. J ) ) : ( S i^i U. J ) -1-1-> ( S i^i U. J ) )
6 4 5 mp1i 
 |-  ( ( J e. A /\ S e. V ) -> ( _I |` ( S i^i U. J ) ) : ( S i^i U. J ) -1-1-> ( S i^i U. J ) )
7 inss2 
 |-  ( S i^i U. J ) C_ U. J
8 resabs1 
 |-  ( ( S i^i U. J ) C_ U. J -> ( ( _I |` U. J ) |` ( S i^i U. J ) ) = ( _I |` ( S i^i U. J ) ) )
9 7 8 ax-mp 
 |-  ( ( _I |` U. J ) |` ( S i^i U. J ) ) = ( _I |` ( S i^i U. J ) )
10 1 adantr 
 |-  ( ( J e. A /\ S e. V ) -> J e. Top )
11 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
12 10 11 sylib 
 |-  ( ( J e. A /\ S e. V ) -> J e. ( TopOn ` U. J ) )
13 idcn 
 |-  ( J e. ( TopOn ` U. J ) -> ( _I |` U. J ) e. ( J Cn J ) )
14 12 13 syl 
 |-  ( ( J e. A /\ S e. V ) -> ( _I |` U. J ) e. ( J Cn J ) )
15 eqid 
 |-  U. J = U. J
16 15 cnrest 
 |-  ( ( ( _I |` U. J ) e. ( J Cn J ) /\ ( S i^i U. J ) C_ U. J ) -> ( ( _I |` U. J ) |` ( S i^i U. J ) ) e. ( ( J |`t ( S i^i U. J ) ) Cn J ) )
17 14 7 16 sylancl 
 |-  ( ( J e. A /\ S e. V ) -> ( ( _I |` U. J ) |` ( S i^i U. J ) ) e. ( ( J |`t ( S i^i U. J ) ) Cn J ) )
18 9 17 eqeltrrid 
 |-  ( ( J e. A /\ S e. V ) -> ( _I |` ( S i^i U. J ) ) e. ( ( J |`t ( S i^i U. J ) ) Cn J ) )
19 15 restin 
 |-  ( ( J e. A /\ S e. V ) -> ( J |`t S ) = ( J |`t ( S i^i U. J ) ) )
20 19 oveq1d 
 |-  ( ( J e. A /\ S e. V ) -> ( ( J |`t S ) Cn J ) = ( ( J |`t ( S i^i U. J ) ) Cn J ) )
21 18 20 eleqtrrd 
 |-  ( ( J e. A /\ S e. V ) -> ( _I |` ( S i^i U. J ) ) e. ( ( J |`t S ) Cn J ) )
22 3 6 21 2 syl3anc 
 |-  ( ( J e. A /\ S e. V ) -> ( J |`t S ) e. A )