Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  xmetres2 Unicode version

Theorem xmetres2 12587
 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 xmetrel 12551 . . . . 5
2 relelfvdm 5461 . . . . 5
31, 2mpan 421 . . . 4
5 simpr 109 . . 3
64, 5ssexd 4076 . 2
7 xmetf 12558 . . . 4
9 xpss12 4654 . . . 4
105, 9sylancom 417 . . 3
118, 10fssresd 5307 . 2
12 ovres 5918 . . . . 5
1312adantl 275 . . . 4
1413eqeq1d 2149 . . 3
15 simpll 519 . . . 4
16 simplr 520 . . . . 5
17 simprl 521 . . . . 5
1816, 17sseldd 3103 . . . 4
19 simprr 522 . . . . 5
2016, 19sseldd 3103 . . . 4
21 xmeteq0 12567 . . . 4
2215, 18, 20, 21syl3anc 1217 . . 3
2314, 22bitrd 187 . 2
24 simpll 519 . . . 4
25 simplr 520 . . . . 5
26 simpr3 990 . . . . 5
2725, 26sseldd 3103 . . . 4
28183adantr3 1143 . . . 4
29203adantr3 1143 . . . 4
30 xmettri2 12569 . . . 4
3124, 27, 28, 29, 30syl13anc 1219 . . 3