Metamath Proof Explorer

Theorem mspropd

Description: Property deduction for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses xmspropd.1 ⊢φ→B=BaseK
xmspropd.2 ⊢φ→B=BaseL
xmspropd.3 ⊢φ→dist⁡K↾B×B=dist⁡L↾B×B
xmspropd.4 ⊢φ→TopOpen⁡K=TopOpen⁡L
Assertion mspropd ⊢φ→K∈MetSp↔L∈MetSp

Proof

Step Hyp Ref Expression
1 xmspropd.1 ⊢φ→B=BaseK
2 xmspropd.2 ⊢φ→B=BaseL
3 xmspropd.3 ⊢φ→dist⁡K↾B×B=dist⁡L↾B×B
4 xmspropd.4 ⊢φ→TopOpen⁡K=TopOpen⁡L
5 1 2 3 4 xmspropd ⊢φ→K∈∞MetSp↔L∈∞MetSp
6 1 sqxpeqd ⊢φ→B×B=BaseK×BaseK
7 6 reseq2d ⊢φ→dist⁡K↾B×B=dist⁡K↾BaseK×BaseK
8 3 7 eqtr3d ⊢φ→dist⁡L↾B×B=dist⁡K↾BaseK×BaseK
9 2 sqxpeqd ⊢φ→B×B=BaseL×BaseL
10 9 reseq2d ⊢φ→dist⁡L↾B×B=dist⁡L↾BaseL×BaseL
11 8 10 eqtr3d ⊢φ→dist⁡K↾BaseK×BaseK=dist⁡L↾BaseL×BaseL
12 1 2 eqtr3d ⊢φ→BaseK=BaseL
13 12 fveq2d ⊢φ→Met⁡BaseK=Met⁡BaseL
14 11 13 eleq12d ⊢φ→dist⁡K↾BaseK×BaseK∈Met⁡BaseK↔dist⁡L↾BaseL×BaseL∈Met⁡BaseL
15 5 14 anbi12d ⊢φ→K∈∞MetSp∧dist⁡K↾BaseK×BaseK∈Met⁡BaseK↔L∈∞MetSp∧dist⁡L↾BaseL×BaseL∈Met⁡BaseL
16 eqid ⊢TopOpen⁡K=TopOpen⁡K
17 eqid ⊢BaseK=BaseK
18 eqid ⊢dist⁡K↾BaseK×BaseK=dist⁡K↾BaseK×BaseK
19 16 17 18 isms ⊢K∈MetSp↔K∈∞MetSp∧dist⁡K↾BaseK×BaseK∈Met⁡BaseK
20 eqid ⊢TopOpen⁡L=TopOpen⁡L
21 eqid ⊢BaseL=BaseL
22 eqid ⊢dist⁡L↾BaseL×BaseL=dist⁡L↾BaseL×BaseL
23 20 21 22 isms ⊢L∈MetSp↔L∈∞MetSp∧dist⁡L↾BaseL×BaseL∈Met⁡BaseL
24 15 19 23 3bitr4g ⊢φ→K∈MetSp↔L∈MetSp