Metamath Proof Explorer


Theorem cnprest2

Description: Equivalence of point-continuity in the parent topology and point-continuity in a subspace. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypotheses cnprest.1 X = J
cnprest.2 Y = K
Assertion cnprest2 K Top F : X B B Y F J CnP K P F J CnP K 𝑡 B P

Proof

Step Hyp Ref Expression
1 cnprest.1 X = J
2 cnprest.2 Y = K
3 cnptop1 F J CnP K P J Top
4 1 cnprcl F J CnP K P P X
5 3 4 jca F J CnP K P J Top P X
6 5 a1i K Top F : X B B Y F J CnP K P J Top P X
7 cnptop1 F J CnP K 𝑡 B P J Top
8 1 cnprcl F J CnP K 𝑡 B P P X
9 7 8 jca F J CnP K 𝑡 B P J Top P X
10 9 a1i K Top F : X B B Y F J CnP K 𝑡 B P J Top P X
11 simpl2 K Top F : X B B Y J Top P X F : X B
12 simprr K Top F : X B B Y J Top P X P X
13 11 12 ffvelrnd K Top F : X B B Y J Top P X F P B
14 13 biantrud K Top F : X B B Y J Top P X F P x F P x F P B
15 elin F P x B F P x F P B
16 14 15 bitr4di K Top F : X B B Y J Top P X F P x F P x B
17 imassrn F y ran F
18 11 frnd K Top F : X B B Y J Top P X ran F B
19 17 18 sstrid K Top F : X B B Y J Top P X F y B
20 19 biantrud K Top F : X B B Y J Top P X F y x F y x F y B
21 ssin F y x F y B F y x B
22 20 21 bitrdi K Top F : X B B Y J Top P X F y x F y x B
23 22 anbi2d K Top F : X B B Y J Top P X P y F y x P y F y x B
24 23 rexbidv K Top F : X B B Y J Top P X y J P y F y x y J P y F y x B
25 16 24 imbi12d K Top F : X B B Y J Top P X F P x y J P y F y x F P x B y J P y F y x B
26 25 ralbidv K Top F : X B B Y J Top P X x K F P x y J P y F y x x K F P x B y J P y F y x B
27 vex x V
28 27 inex1 x B V
29 28 a1i K Top F : X B B Y J Top P X x K x B V
30 simpl1 K Top F : X B B Y J Top P X K Top
31 uniexg K Top K V
32 2 31 eqeltrid K Top Y V
33 30 32 syl K Top F : X B B Y J Top P X Y V
34 simpl3 K Top F : X B B Y J Top P X B Y
35 33 34 ssexd K Top F : X B B Y J Top P X B V
36 elrest K Top B V z K 𝑡 B x K z = x B
37 30 35 36 syl2anc K Top F : X B B Y J Top P X z K 𝑡 B x K z = x B
38 eleq2 z = x B F P z F P x B
39 sseq2 z = x B F y z F y x B
40 39 anbi2d z = x B P y F y z P y F y x B
41 40 rexbidv z = x B y J P y F y z y J P y F y x B
42 38 41 imbi12d z = x B F P z y J P y F y z F P x B y J P y F y x B
43 42 adantl K Top F : X B B Y J Top P X z = x B F P z y J P y F y z F P x B y J P y F y x B
44 29 37 43 ralxfr2d K Top F : X B B Y J Top P X z K 𝑡 B F P z y J P y F y z x K F P x B y J P y F y x B
45 26 44 bitr4d K Top F : X B B Y J Top P X x K F P x y J P y F y x z K 𝑡 B F P z y J P y F y z
46 11 34 fssd K Top F : X B B Y J Top P X F : X Y
47 simprl K Top F : X B B Y J Top P X J Top
48 1 2 iscnp2 F J CnP K P J Top K Top P X F : X Y x K F P x y J P y F y x
49 48 baib J Top K Top P X F J CnP K P F : X Y x K F P x y J P y F y x
50 47 30 12 49 syl3anc K Top F : X B B Y J Top P X F J CnP K P F : X Y x K F P x y J P y F y x
51 46 50 mpbirand K Top F : X B B Y J Top P X F J CnP K P x K F P x y J P y F y x
52 1 toptopon J Top J TopOn X
53 47 52 sylib K Top F : X B B Y J Top P X J TopOn X
54 2 toptopon K Top K TopOn Y
55 30 54 sylib K Top F : X B B Y J Top P X K TopOn Y
56 resttopon K TopOn Y B Y K 𝑡 B TopOn B
57 55 34 56 syl2anc K Top F : X B B Y J Top P X K 𝑡 B TopOn B
58 iscnp J TopOn X K 𝑡 B TopOn B P X F J CnP K 𝑡 B P F : X B z K 𝑡 B F P z y J P y F y z
59 53 57 12 58 syl3anc K Top F : X B B Y J Top P X F J CnP K 𝑡 B P F : X B z K 𝑡 B F P z y J P y F y z
60 11 59 mpbirand K Top F : X B B Y J Top P X F J CnP K 𝑡 B P z K 𝑡 B F P z y J P y F y z
61 45 51 60 3bitr4d K Top F : X B B Y J Top P X F J CnP K P F J CnP K 𝑡 B P
62 61 ex K Top F : X B B Y J Top P X F J CnP K P F J CnP K 𝑡 B P
63 6 10 62 pm5.21ndd K Top F : X B B Y F J CnP K P F J CnP K 𝑡 B P