cnpresti

Description: One direction of cnprest under the weaker condition that the point is in the subset rather than the interior of the subset. (Contributed by Mario Carneiro, 9-Feb-2015) (Revised by Mario Carneiro, 1-May-2015)

		Ref	Expression
	Hypothesis	cnprest.1	$⊢ X = ⋃ J$
	Assertion	cnpresti	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to {F ↾}_{A} \in ((J ↾_{𝑡} A) CnP K) (P)$

Proof

Step	Hyp	Ref	Expression
1		cnprest.1	$⊢ X = ⋃ J$
2		eqid	$⊢ ⋃ K = ⋃ K$
3	1 2	cnpf	$⊢ F \in (J CnP K) (P) \to F : X ⟶ ⋃ K$
4	3	3ad2ant3	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to F : X ⟶ ⋃ K$
5		simp1	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to A \subseteq X$
6	4 5	fssresd	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to ({F ↾}_{A}) : A ⟶ ⋃ K$
7		simpl2	$⊢ ((A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \land y \in K) \to P \in A$
8	7	fvresd	$⊢ ((A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \land y \in K) \to ({F ↾}_{A}) (P) = F (P)$
9	8	eleq1d	$⊢ ((A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \land y \in K) \to (({F ↾}_{A}) (P) \in y \leftrightarrow F (P) \in y)$
10		cnpimaex	$⊢ (F \in (J CnP K) (P) \land y \in K \land F (P) \in y) \to \exists x \in J (P \in x \land F [x] \subseteq y)$
11	10	3expia	$⊢ (F \in (J CnP K) (P) \land y \in K) \to (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))$
12	11	3ad2antl3	$⊢ ((A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \land y \in K) \to (F (P) \in y \to \exists x \in J (P \in x \land F [x] \subseteq y))$
13		idd	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to (P \in x \to P \in x)$
14		simp2	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to P \in A$
15	13 14	jctird	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to (P \in x \to (P \in x \land P \in A))$
16		elin	$⊢ P \in (x \cap A) \leftrightarrow (P \in x \land P \in A)$
17	15 16	imbitrrdi	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to (P \in x \to P \in (x \cap A))$
18		inss1	$⊢ x \cap A \subseteq x$
19		imass2	$⊢ x \cap A \subseteq x \to F [x \cap A] \subseteq F [x]$
20	18 19	ax-mp	$⊢ F [x \cap A] \subseteq F [x]$
21		id	$⊢ F [x] \subseteq y \to F [x] \subseteq y$
22	20 21	sstrid	$⊢ F [x] \subseteq y \to F [x \cap A] \subseteq y$
23	17 22	anim12d1	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to ((P \in x \land F [x] \subseteq y) \to (P \in (x \cap A) \land F [x \cap A] \subseteq y))$
24	23	reximdv	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to (\exists x \in J (P \in x \land F [x] \subseteq y) \to \exists x \in J (P \in (x \cap A) \land F [x \cap A] \subseteq y))$
25		vex	$⊢ x \in V$
26	25	inex1	$⊢ x \cap A \in V$
27	26	a1i	$⊢ ((A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \land x \in J) \to x \cap A \in V$
28		cnptop1	$⊢ F \in (J CnP K) (P) \to J \in Top$
29	28	3ad2ant3	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to J \in Top$
30	29	uniexd	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to ⋃ J \in V$
31	5 1	sseqtrdi	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to A \subseteq ⋃ J$
32	30 31	ssexd	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to A \in V$
33		elrest	$⊢ (J \in Top \land A \in V) \to (z \in (J ↾_{𝑡} A) \leftrightarrow \exists x \in J z = x \cap A)$
34	29 32 33	syl2anc	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to (z \in (J ↾_{𝑡} A) \leftrightarrow \exists x \in J z = x \cap A)$
35		simpr	$⊢ ((A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \land z = x \cap A) \to z = x \cap A$
36	35	eleq2d	$⊢ ((A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \land z = x \cap A) \to (P \in z \leftrightarrow P \in (x \cap A))$
37	35	imaeq2d	$⊢ ((A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \land z = x \cap A) \to ({F ↾}_{A}) [z] = ({F ↾}_{A}) [x \cap A]$
38		inss2	$⊢ x \cap A \subseteq A$
39		resima2	$⊢ x \cap A \subseteq A \to ({F ↾}_{A}) [x \cap A] = F [x \cap A]$
40	38 39	ax-mp	$⊢ ({F ↾}_{A}) [x \cap A] = F [x \cap A]$
41	37 40	eqtrdi	$⊢ ((A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \land z = x \cap A) \to ({F ↾}_{A}) [z] = F [x \cap A]$
42	41	sseq1d	$⊢ ((A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \land z = x \cap A) \to (({F ↾}_{A}) [z] \subseteq y \leftrightarrow F [x \cap A] \subseteq y)$
43	36 42	anbi12d	$⊢ ((A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \land z = x \cap A) \to ((P \in z \land ({F ↾}_{A}) [z] \subseteq y) \leftrightarrow (P \in (x \cap A) \land F [x \cap A] \subseteq y))$
44	27 34 43	rexxfr2d	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to (\exists z \in (J ↾_{𝑡} A) (P \in z \land ({F ↾}_{A}) [z] \subseteq y) \leftrightarrow \exists x \in J (P \in (x \cap A) \land F [x \cap A] \subseteq y))$
45	24 44	sylibrd	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to (\exists x \in J (P \in x \land F [x] \subseteq y) \to \exists z \in (J ↾_{𝑡} A) (P \in z \land ({F ↾}_{A}) [z] \subseteq y))$
46	45	adantr	$⊢ ((A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \land y \in K) \to (\exists x \in J (P \in x \land F [x] \subseteq y) \to \exists z \in (J ↾_{𝑡} A) (P \in z \land ({F ↾}_{A}) [z] \subseteq y))$
47	12 46	syld	$⊢ ((A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \land y \in K) \to (F (P) \in y \to \exists z \in (J ↾_{𝑡} A) (P \in z \land ({F ↾}_{A}) [z] \subseteq y))$
48	9 47	sylbid	$⊢ ((A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \land y \in K) \to (({F ↾}_{A}) (P) \in y \to \exists z \in (J ↾_{𝑡} A) (P \in z \land ({F ↾}_{A}) [z] \subseteq y))$
49	48	ralrimiva	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to \forall y \in K (({F ↾}_{A}) (P) \in y \to \exists z \in (J ↾_{𝑡} A) (P \in z \land ({F ↾}_{A}) [z] \subseteq y))$
50	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
51	29 50	sylib	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to J \in TopOn (X)$
52		resttopon	$⊢ (J \in TopOn (X) \land A \subseteq X) \to J ↾_{𝑡} A \in TopOn (A)$
53	51 5 52	syl2anc	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to J ↾_{𝑡} A \in TopOn (A)$
54		cnptop2	$⊢ F \in (J CnP K) (P) \to K \in Top$
55	54	3ad2ant3	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to K \in Top$
56	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
57	55 56	sylib	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to K \in TopOn (⋃ K)$
58		iscnp	$⊢ (J ↾_{𝑡} A \in TopOn (A) \land K \in TopOn (⋃ K) \land P \in A) \to ({F ↾}_{A} \in ((J ↾_{𝑡} A) CnP K) (P) \leftrightarrow (({F ↾}_{A}) : A ⟶ ⋃ K \land \forall y \in K (({F ↾}_{A}) (P) \in y \to \exists z \in (J ↾_{𝑡} A) (P \in z \land ({F ↾}_{A}) [z] \subseteq y))))$
59	53 57 14 58	syl3anc	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to ({F ↾}_{A} \in ((J ↾_{𝑡} A) CnP K) (P) \leftrightarrow (({F ↾}_{A}) : A ⟶ ⋃ K \land \forall y \in K (({F ↾}_{A}) (P) \in y \to \exists z \in (J ↾_{𝑡} A) (P \in z \land ({F ↾}_{A}) [z] \subseteq y))))$
60	6 49 59	mpbir2and	$⊢ (A \subseteq X \land P \in A \land F \in (J CnP K) (P)) \to {F ↾}_{A} \in ((J ↾_{𝑡} A) CnP K) (P)$

Metamath Proof Explorer

Theorem cnpresti

Proof