Metamath Proof Explorer


Theorem xpstopnlem2

Description: Lemma for xpstopn . (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypotheses xpstps.t T = R × 𝑠 S
xpstopn.j J = TopOpen R
xpstopn.k K = TopOpen S
xpstopn.o O = TopOpen T
xpstopnlem.x X = Base R
xpstopnlem.y Y = Base S
xpstopnlem.f F = x X , y Y x 1 𝑜 y
Assertion xpstopnlem2 R TopSp S TopSp O = J × t K

Proof

Step Hyp Ref Expression
1 xpstps.t T = R × 𝑠 S
2 xpstopn.j J = TopOpen R
3 xpstopn.k K = TopOpen S
4 xpstopn.o O = TopOpen T
5 xpstopnlem.x X = Base R
6 xpstopnlem.y Y = Base S
7 xpstopnlem.f F = x X , y Y x 1 𝑜 y
8 eqid Scalar R 𝑠 R 1 𝑜 S = Scalar R 𝑠 R 1 𝑜 S
9 fvexd R TopSp S TopSp Scalar R V
10 2on 2 𝑜 On
11 10 a1i R TopSp S TopSp 2 𝑜 On
12 fnpr2o R TopSp S TopSp R 1 𝑜 S Fn 2 𝑜
13 eqid TopOpen Scalar R 𝑠 R 1 𝑜 S = TopOpen Scalar R 𝑠 R 1 𝑜 S
14 8 9 11 12 13 prdstopn R TopSp S TopSp TopOpen Scalar R 𝑠 R 1 𝑜 S = 𝑡 TopOpen R 1 𝑜 S
15 topnfn TopOpen Fn V
16 dffn2 R 1 𝑜 S Fn 2 𝑜 R 1 𝑜 S : 2 𝑜 V
17 12 16 sylib R TopSp S TopSp R 1 𝑜 S : 2 𝑜 V
18 fnfco TopOpen Fn V R 1 𝑜 S : 2 𝑜 V TopOpen R 1 𝑜 S Fn 2 𝑜
19 15 17 18 sylancr R TopSp S TopSp TopOpen R 1 𝑜 S Fn 2 𝑜
20 xpsfeq TopOpen R 1 𝑜 S Fn 2 𝑜 TopOpen R 1 𝑜 S 1 𝑜 TopOpen R 1 𝑜 S 1 𝑜 = TopOpen R 1 𝑜 S
21 19 20 syl R TopSp S TopSp TopOpen R 1 𝑜 S 1 𝑜 TopOpen R 1 𝑜 S 1 𝑜 = TopOpen R 1 𝑜 S
22 0ex V
23 22 prid1 1 𝑜
24 df2o3 2 𝑜 = 1 𝑜
25 23 24 eleqtrri 2 𝑜
26 fvco2 R 1 𝑜 S Fn 2 𝑜 2 𝑜 TopOpen R 1 𝑜 S = TopOpen R 1 𝑜 S
27 12 25 26 sylancl R TopSp S TopSp TopOpen R 1 𝑜 S = TopOpen R 1 𝑜 S
28 fvpr0o R TopSp R 1 𝑜 S = R
29 28 adantr R TopSp S TopSp R 1 𝑜 S = R
30 29 fveq2d R TopSp S TopSp TopOpen R 1 𝑜 S = TopOpen R
31 30 2 syl6eqr R TopSp S TopSp TopOpen R 1 𝑜 S = J
32 27 31 eqtrd R TopSp S TopSp TopOpen R 1 𝑜 S = J
33 32 opeq2d R TopSp S TopSp TopOpen R 1 𝑜 S = J
34 1oex 1 𝑜 V
35 34 prid2 1 𝑜 1 𝑜
36 35 24 eleqtrri 1 𝑜 2 𝑜
37 fvco2 R 1 𝑜 S Fn 2 𝑜 1 𝑜 2 𝑜 TopOpen R 1 𝑜 S 1 𝑜 = TopOpen R 1 𝑜 S 1 𝑜
38 12 36 37 sylancl R TopSp S TopSp TopOpen R 1 𝑜 S 1 𝑜 = TopOpen R 1 𝑜 S 1 𝑜
39 fvpr1o S TopSp R 1 𝑜 S 1 𝑜 = S
40 39 adantl R TopSp S TopSp R 1 𝑜 S 1 𝑜 = S
41 40 fveq2d R TopSp S TopSp TopOpen R 1 𝑜 S 1 𝑜 = TopOpen S
42 41 3 syl6eqr R TopSp S TopSp TopOpen R 1 𝑜 S 1 𝑜 = K
43 38 42 eqtrd R TopSp S TopSp TopOpen R 1 𝑜 S 1 𝑜 = K
44 43 opeq2d R TopSp S TopSp 1 𝑜 TopOpen R 1 𝑜 S 1 𝑜 = 1 𝑜 K
45 33 44 preq12d R TopSp S TopSp TopOpen R 1 𝑜 S 1 𝑜 TopOpen R 1 𝑜 S 1 𝑜 = J 1 𝑜 K
46 21 45 eqtr3d R TopSp S TopSp TopOpen R 1 𝑜 S = J 1 𝑜 K
47 46 fveq2d R TopSp S TopSp 𝑡 TopOpen R 1 𝑜 S = 𝑡 J 1 𝑜 K
48 14 47 eqtrd R TopSp S TopSp TopOpen Scalar R 𝑠 R 1 𝑜 S = 𝑡 J 1 𝑜 K
49 48 oveq1d R TopSp S TopSp TopOpen Scalar R 𝑠 R 1 𝑜 S qTop F -1 = 𝑡 J 1 𝑜 K qTop F -1
50 simpl R TopSp S TopSp R TopSp
51 simpr R TopSp S TopSp S TopSp
52 eqid Scalar R = Scalar R
53 1 5 6 50 51 7 52 8 xpsval R TopSp S TopSp T = F -1 𝑠 Scalar R 𝑠 R 1 𝑜 S
54 1 5 6 50 51 7 52 8 xpsrnbas R TopSp S TopSp ran F = Base Scalar R 𝑠 R 1 𝑜 S
55 7 xpsff1o2 F : X × Y 1-1 onto ran F
56 f1ocnv F : X × Y 1-1 onto ran F F -1 : ran F 1-1 onto X × Y
57 55 56 mp1i R TopSp S TopSp F -1 : ran F 1-1 onto X × Y
58 f1ofo F -1 : ran F 1-1 onto X × Y F -1 : ran F onto X × Y
59 57 58 syl R TopSp S TopSp F -1 : ran F onto X × Y
60 ovexd R TopSp S TopSp Scalar R 𝑠 R 1 𝑜 S V
61 53 54 59 60 13 4 imastopn R TopSp S TopSp O = TopOpen Scalar R 𝑠 R 1 𝑜 S qTop F -1
62 5 2 istps R TopSp J TopOn X
63 50 62 sylib R TopSp S TopSp J TopOn X
64 6 3 istps S TopSp K TopOn Y
65 51 64 sylib R TopSp S TopSp K TopOn Y
66 7 63 65 xpstopnlem1 R TopSp S TopSp F J × t K Homeo 𝑡 J 1 𝑜 K
67 hmeocnv F J × t K Homeo 𝑡 J 1 𝑜 K F -1 𝑡 J 1 𝑜 K Homeo J × t K
68 hmeoqtop F -1 𝑡 J 1 𝑜 K Homeo J × t K J × t K = 𝑡 J 1 𝑜 K qTop F -1
69 66 67 68 3syl R TopSp S TopSp J × t K = 𝑡 J 1 𝑜 K qTop F -1
70 49 61 69 3eqtr4d R TopSp S TopSp O = J × t K