Metamath Proof Explorer

Theorem isofr2

Description: A weak form of isofr that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014)

Ref Expression
Assertion isofr2 
|- ( ( H Isom R , S ( A , B ) /\ B e. V ) -> ( S Fr B -> R Fr A ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( H Isom R , S ( A , B ) /\ B e. V ) -> H Isom R , S ( A , B ) )
2 imassrn 
 |-  ( H " x ) C_ ran H
3 isof1o 
 |-  ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B )
4 f1of 
 |-  ( H : A -1-1-onto-> B -> H : A --> B )
5 frn 
 |-  ( H : A --> B -> ran H C_ B )
6 3 4 5 3syl 
 |-  ( H Isom R , S ( A , B ) -> ran H C_ B )
7 2 6 sstrid 
 |-  ( H Isom R , S ( A , B ) -> ( H " x ) C_ B )
8 ssexg 
 |-  ( ( ( H " x ) C_ B /\ B e. V ) -> ( H " x ) e. _V )
9 7 8 sylan 
 |-  ( ( H Isom R , S ( A , B ) /\ B e. V ) -> ( H " x ) e. _V )
10 1 9 isofrlem 
 |-  ( ( H Isom R , S ( A , B ) /\ B e. V ) -> ( S Fr B -> R Fr A ) )