# 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}=\bigcup {J}$
cnprest.2 ${⊢}{Y}=\bigcup {K}$
Assertion cnprest2 ${⊢}\left({K}\in \mathrm{Top}\wedge {F}:{X}⟶{B}\wedge {B}\subseteq {Y}\right)\to \left({F}\in \left({J}\mathrm{CnP}{K}\right)\left({P}\right)↔{F}\in \left({J}\mathrm{CnP}\left({K}{↾}_{𝑡}{B}\right)\right)\left({P}\right)\right)$

### Proof

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