Metamath Proof Explorer


Theorem ismtybndlem

Description: Lemma for ismtybnd . (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 19-Jan-2014)

Ref Expression
Assertion ismtybndlem N ∞Met Y F M Ismty N M Bnd X N Bnd Y

Proof

Step Hyp Ref Expression
1 isismty M ∞Met X N ∞Met Y F M Ismty N F : X 1-1 onto Y z X w X z M w = F z N F w
2 1 biimp3a M ∞Met X N ∞Met Y F M Ismty N F : X 1-1 onto Y z X w X z M w = F z N F w
3 2 simpld M ∞Met X N ∞Met Y F M Ismty N F : X 1-1 onto Y
4 f1ocnv F : X 1-1 onto Y F -1 : Y 1-1 onto X
5 f1of F -1 : Y 1-1 onto X F -1 : Y X
6 3 4 5 3syl M ∞Met X N ∞Met Y F M Ismty N F -1 : Y X
7 6 ffvelrnda M ∞Met X N ∞Met Y F M Ismty N y Y F -1 y X
8 oveq1 x = F -1 y x ball M r = F -1 y ball M r
9 8 eqeq2d x = F -1 y X = x ball M r X = F -1 y ball M r
10 9 rexbidv x = F -1 y r + X = x ball M r r + X = F -1 y ball M r
11 10 rspcv F -1 y X x X r + X = x ball M r r + X = F -1 y ball M r
12 7 11 syl M ∞Met X N ∞Met Y F M Ismty N y Y x X r + X = x ball M r r + X = F -1 y ball M r
13 imaeq2 X = F -1 y ball M r F X = F F -1 y ball M r
14 f1ofo F : X 1-1 onto Y F : X onto Y
15 foima F : X onto Y F X = Y
16 3 14 15 3syl M ∞Met X N ∞Met Y F M Ismty N F X = Y
17 16 adantr M ∞Met X N ∞Met Y F M Ismty N y Y r + F X = Y
18 rpxr r + r *
19 18 adantl M ∞Met X N ∞Met Y F M Ismty N r + r *
20 7 19 anim12dan M ∞Met X N ∞Met Y F M Ismty N y Y r + F -1 y X r *
21 ismtyima M ∞Met X N ∞Met Y F M Ismty N F -1 y X r * F F -1 y ball M r = F F -1 y ball N r
22 20 21 syldan M ∞Met X N ∞Met Y F M Ismty N y Y r + F F -1 y ball M r = F F -1 y ball N r
23 simpl y Y r + y Y
24 f1ocnvfv2 F : X 1-1 onto Y y Y F F -1 y = y
25 3 23 24 syl2an M ∞Met X N ∞Met Y F M Ismty N y Y r + F F -1 y = y
26 25 oveq1d M ∞Met X N ∞Met Y F M Ismty N y Y r + F F -1 y ball N r = y ball N r
27 22 26 eqtrd M ∞Met X N ∞Met Y F M Ismty N y Y r + F F -1 y ball M r = y ball N r
28 17 27 eqeq12d M ∞Met X N ∞Met Y F M Ismty N y Y r + F X = F F -1 y ball M r Y = y ball N r
29 13 28 syl5ib M ∞Met X N ∞Met Y F M Ismty N y Y r + X = F -1 y ball M r Y = y ball N r
30 29 anassrs M ∞Met X N ∞Met Y F M Ismty N y Y r + X = F -1 y ball M r Y = y ball N r
31 30 reximdva M ∞Met X N ∞Met Y F M Ismty N y Y r + X = F -1 y ball M r r + Y = y ball N r
32 12 31 syld M ∞Met X N ∞Met Y F M Ismty N y Y x X r + X = x ball M r r + Y = y ball N r
33 32 ralrimdva M ∞Met X N ∞Met Y F M Ismty N x X r + X = x ball M r y Y r + Y = y ball N r
34 simp2 M ∞Met X N ∞Met Y F M Ismty N N ∞Met Y
35 33 34 jctild M ∞Met X N ∞Met Y F M Ismty N x X r + X = x ball M r N ∞Met Y y Y r + Y = y ball N r
36 35 3expib M ∞Met X N ∞Met Y F M Ismty N x X r + X = x ball M r N ∞Met Y y Y r + Y = y ball N r
37 36 com12 N ∞Met Y F M Ismty N M ∞Met X x X r + X = x ball M r N ∞Met Y y Y r + Y = y ball N r
38 37 impd N ∞Met Y F M Ismty N M ∞Met X x X r + X = x ball M r N ∞Met Y y Y r + Y = y ball N r
39 isbndx M Bnd X M ∞Met X x X r + X = x ball M r
40 isbndx N Bnd Y N ∞Met Y y Y r + Y = y ball N r
41 38 39 40 3imtr4g N ∞Met Y F M Ismty N M Bnd X N Bnd Y