Metamath Proof Explorer

Theorem metres2

Description: Lemma for metres . (Contributed by FL, 12-Oct-2006) (Proof shortened by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion metres2 
|- ( ( D e. ( Met ` X ) /\ R C_ X ) -> ( D |` ( R X. R ) ) e. ( Met ` R ) )

Proof

Step Hyp Ref Expression
1 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
2 xmetres2 
 |-  ( ( D e. ( *Met ` X ) /\ R C_ X ) -> ( D |` ( R X. R ) ) e. ( *Met ` R ) )
3 1 2 sylan 
 |-  ( ( D e. ( Met ` X ) /\ R C_ X ) -> ( D |` ( R X. R ) ) e. ( *Met ` R ) )
4 metf 
 |-  ( D e. ( Met ` X ) -> D : ( X X. X ) --> RR )
5 4 adantr 
 |-  ( ( D e. ( Met ` X ) /\ R C_ X ) -> D : ( X X. X ) --> RR )
6 simpr 
 |-  ( ( D e. ( Met ` X ) /\ R C_ X ) -> R C_ X )
7 xpss12 
 |-  ( ( R C_ X /\ R C_ X ) -> ( R X. R ) C_ ( X X. X ) )
8 6 7 sylancom 
 |-  ( ( D e. ( Met ` X ) /\ R C_ X ) -> ( R X. R ) C_ ( X X. X ) )
9 5 8 fssresd 
 |-  ( ( D e. ( Met ` X ) /\ R C_ X ) -> ( D |` ( R X. R ) ) : ( R X. R ) --> RR )
10 ismet2 
 |-  ( ( D |` ( R X. R ) ) e. ( Met ` R ) <-> ( ( D |` ( R X. R ) ) e. ( *Met ` R ) /\ ( D |` ( R X. R ) ) : ( R X. R ) --> RR ) )
11 3 9 10 sylanbrc 
 |-  ( ( D e. ( Met ` X ) /\ R C_ X ) -> ( D |` ( R X. R ) ) e. ( Met ` R ) )