Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  xmetres2 Structured version   Unicode version

Theorem xmetres2 21307
 Description: Restriction of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xmetres2

Proof of Theorem xmetres2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfvdm 5907 . . . 4
3 simpr 462 . . 3
42, 3ssexd 4572 . 2
5 xmetf 21275 . . . 4
7 xpss12 4960 . . . 4
83, 7sylancom 671 . . 3
96, 8fssresd 5767 . 2
10 ovres 6450 . . . . 5
1110adantl 467 . . . 4
1211eqeq1d 2431 . . 3
13 simpll 758 . . . 4
14 simplr 760 . . . . 5
15 simprl 762 . . . . 5
1614, 15sseldd 3471 . . . 4
17 simprr 764 . . . . 5
1814, 17sseldd 3471 . . . 4
19 xmeteq0 21284 . . . 4
2013, 16, 18, 19syl3anc 1264 . . 3
2112, 20bitrd 256 . 2
22 simpll 758 . . . 4
23 simplr 760 . . . . 5
24 simpr3 1013 . . . . 5
2523, 24sseldd 3471 . . . 4
26163adantr3 1166 . . . 4
27183adantr3 1166 . . . 4
28 xmettri2 21286 . . . 4
2922, 25, 26, 27, 28syl13anc 1266 . . 3