Metamath Proof Explorer

Theorem bnd2lem

Description: Lemma for equivbnd2 and similar theorems. (Contributed by Jeff Madsen, 16-Sep-2015)

Ref Expression
Hypothesis bnd2lem.1 
|- D = ( M |` ( Y X. Y ) )
Assertion bnd2lem 
|- ( ( M e. ( Met ` X ) /\ D e. ( Bnd ` Y ) ) -> Y C_ X )

Proof

Step Hyp Ref Expression
1 bnd2lem.1 
 |-  D = ( M |` ( Y X. Y ) )
2 resss 
 |-  ( M |` ( Y X. Y ) ) C_ M
3 1 2 eqsstri 
 |-  D C_ M
4 dmss 
 |-  ( D C_ M -> dom D C_ dom M )
5 3 4 mp1i 
 |-  ( ( M e. ( Met ` X ) /\ D e. ( Bnd ` Y ) ) -> dom D C_ dom M )
6 bndmet 
 |-  ( D e. ( Bnd ` Y ) -> D e. ( Met ` Y ) )
7 metf 
 |-  ( D e. ( Met ` Y ) -> D : ( Y X. Y ) --> RR )
8 fdm 
 |-  ( D : ( Y X. Y ) --> RR -> dom D = ( Y X. Y ) )
9 6 7 8 3syl 
 |-  ( D e. ( Bnd ` Y ) -> dom D = ( Y X. Y ) )
10 9 adantl 
 |-  ( ( M e. ( Met ` X ) /\ D e. ( Bnd ` Y ) ) -> dom D = ( Y X. Y ) )
11 metf 
 |-  ( M e. ( Met ` X ) -> M : ( X X. X ) --> RR )
12 11 fdmd 
 |-  ( M e. ( Met ` X ) -> dom M = ( X X. X ) )
13 12 adantr 
 |-  ( ( M e. ( Met ` X ) /\ D e. ( Bnd ` Y ) ) -> dom M = ( X X. X ) )
14 5 10 13 3sstr3d 
 |-  ( ( M e. ( Met ` X ) /\ D e. ( Bnd ` Y ) ) -> ( Y X. Y ) C_ ( X X. X ) )
15 dmss 
 |-  ( ( Y X. Y ) C_ ( X X. X ) -> dom ( Y X. Y ) C_ dom ( X X. X ) )
16 14 15 syl 
 |-  ( ( M e. ( Met ` X ) /\ D e. ( Bnd ` Y ) ) -> dom ( Y X. Y ) C_ dom ( X X. X ) )
17 dmxpid 
 |-  dom ( Y X. Y ) = Y
18 dmxpid 
 |-  dom ( X X. X ) = X
19 16 17 18 3sstr3g 
 |-  ( ( M e. ( Met ` X ) /\ D e. ( Bnd ` Y ) ) -> Y C_ X )