ptrescn

Description: Restriction is a continuous function on product topologies. (Contributed by Mario Carneiro, 7-Feb-2015)

	Ref	Expression
Hypotheses	ptrescn.1	$⊢ X = ⋃ J$
	ptrescn.2	$⊢ J = \prod_{𝑡} (F)$
	ptrescn.3	$⊢ K = \prod_{𝑡} ({F ↾}_{B})$
Assertion	ptrescn	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to (x \in X ⟼ {x ↾}_{B}) \in (J Cn K)$

Proof

Step	Hyp	Ref	Expression
1		ptrescn.1	$⊢ X = ⋃ J$
2		ptrescn.2	$⊢ J = \prod_{𝑡} (F)$
3		ptrescn.3	$⊢ K = \prod_{𝑡} ({F ↾}_{B})$
4		simpl3	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land x \in X) \to B \subseteq A$
5	2	ptuni	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{k \in A}{⨉} ⋃ F (k) = ⋃ J$
6	5	3adant3	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to \underset{k \in A}{⨉} ⋃ F (k) = ⋃ J$
7	6 1	eqtr4di	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to \underset{k \in A}{⨉} ⋃ F (k) = X$
8	7	eleq2d	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to (x \in \underset{k \in A}{⨉} ⋃ F (k) \leftrightarrow x \in X)$
9	8	biimpar	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land x \in X) \to x \in \underset{k \in A}{⨉} ⋃ F (k)$
10		resixp	$⊢ (B \subseteq A \land x \in \underset{k \in A}{⨉} ⋃ F (k)) \to {x ↾}_{B} \in \underset{k \in B}{⨉} ⋃ F (k)$
11	4 9 10	syl2anc	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land x \in X) \to {x ↾}_{B} \in \underset{k \in B}{⨉} ⋃ F (k)$
12		ixpeq2	$⊢ \forall k \in B ⋃ ({F ↾}_{B}) (k) = ⋃ F (k) \to \underset{k \in B}{⨉} ⋃ ({F ↾}_{B}) (k) = \underset{k \in B}{⨉} ⋃ F (k)$
13		fvres	$⊢ k \in B \to ({F ↾}_{B}) (k) = F (k)$
14	13	unieqd	$⊢ k \in B \to ⋃ ({F ↾}_{B}) (k) = ⋃ F (k)$
15	12 14	mprg	$⊢ \underset{k \in B}{⨉} ⋃ ({F ↾}_{B}) (k) = \underset{k \in B}{⨉} ⋃ F (k)$
16		ssexg	$⊢ (B \subseteq A \land A \in V) \to B \in V$
17	16	ancoms	$⊢ (A \in V \land B \subseteq A) \to B \in V$
18	17	3adant2	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to B \in V$
19		fssres	$⊢ (F : A ⟶ Top \land B \subseteq A) \to ({F ↾}_{B}) : B ⟶ Top$
20	19	3adant1	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to ({F ↾}_{B}) : B ⟶ Top$
21	3	ptuni	$⊢ (B \in V \land ({F ↾}_{B}) : B ⟶ Top) \to \underset{k \in B}{⨉} ⋃ ({F ↾}_{B}) (k) = ⋃ K$
22	18 20 21	syl2anc	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to \underset{k \in B}{⨉} ⋃ ({F ↾}_{B}) (k) = ⋃ K$
23	15 22	eqtr3id	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to \underset{k \in B}{⨉} ⋃ F (k) = ⋃ K$
24	23	adantr	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land x \in X) \to \underset{k \in B}{⨉} ⋃ F (k) = ⋃ K$
25	11 24	eleqtrd	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land x \in X) \to {x ↾}_{B} \in ⋃ K$
26	25	fmpttd	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to (x \in X ⟼ {x ↾}_{B}) : X ⟶ ⋃ K$
27		fimacnv	$⊢ (x \in X ⟼ {x ↾}_{B}) : X ⟶ ⋃ K \to {(x \in X ⟼ {x ↾}_{B})}^{-1} [⋃ K] = X$
28	26 27	syl	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to {(x \in X ⟼ {x ↾}_{B})}^{-1} [⋃ K] = X$
29		pttop	$⊢ (A \in V \land F : A ⟶ Top) \to \prod_{𝑡} (F) \in Top$
30	2 29	eqeltrid	$⊢ (A \in V \land F : A ⟶ Top) \to J \in Top$
31	30	3adant3	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to J \in Top$
32	1	topopn	$⊢ J \in Top \to X \in J$
33	31 32	syl	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to X \in J$
34	28 33	eqeltrd	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to {(x \in X ⟼ {x ↾}_{B})}^{-1} [⋃ K] \in J$
35		elsni	$⊢ v \in \{⋃ K\} \to v = ⋃ K$
36	35	imaeq2d	$⊢ v \in \{⋃ K\} \to {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] = {(x \in X ⟼ {x ↾}_{B})}^{-1} [⋃ K]$
37	36	eleq1d	$⊢ v \in \{⋃ K\} \to ({(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J \leftrightarrow {(x \in X ⟼ {x ↾}_{B})}^{-1} [⋃ K] \in J)$
38	34 37	syl5ibrcom	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to (v \in \{⋃ K\} \to {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J)$
39	38	ralrimiv	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to \forall v \in \{⋃ K\} {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J$
40		imaco	$⊢ ({(x \in X ⟼ {x ↾}_{B})}^{-1} \circ {(z \in ⋃ K ⟼ z (k))}^{-1}) [u] = {(x \in X ⟼ {x ↾}_{B})}^{-1} [{(z \in ⋃ K ⟼ z (k))}^{-1} [u]]$
41		cnvco	$⊢ {((z \in ⋃ K ⟼ z (k)) \circ (x \in X ⟼ {x ↾}_{B}))}^{-1} = {(x \in X ⟼ {x ↾}_{B})}^{-1} \circ {(z \in ⋃ K ⟼ z (k))}^{-1}$
42	25	adantlr	$⊢ (((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \land x \in X) \to {x ↾}_{B} \in ⋃ K$
43		eqidd	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to (x \in X ⟼ {x ↾}_{B}) = (x \in X ⟼ {x ↾}_{B})$
44		eqidd	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to (z \in ⋃ K ⟼ z (k)) = (z \in ⋃ K ⟼ z (k))$
45		fveq1	$⊢ z = {x ↾}_{B} \to z (k) = ({x ↾}_{B}) (k)$
46	42 43 44 45	fmptco	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to (z \in ⋃ K ⟼ z (k)) \circ (x \in X ⟼ {x ↾}_{B}) = (x \in X ⟼ ({x ↾}_{B}) (k))$
47		fvres	$⊢ k \in B \to ({x ↾}_{B}) (k) = x (k)$
48	47	ad2antrl	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to ({x ↾}_{B}) (k) = x (k)$
49	48	mpteq2dv	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to (x \in X ⟼ ({x ↾}_{B}) (k)) = (x \in X ⟼ x (k))$
50	46 49	eqtrd	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to (z \in ⋃ K ⟼ z (k)) \circ (x \in X ⟼ {x ↾}_{B}) = (x \in X ⟼ x (k))$
51	50	cnveqd	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to {((z \in ⋃ K ⟼ z (k)) \circ (x \in X ⟼ {x ↾}_{B}))}^{-1} = {(x \in X ⟼ x (k))}^{-1}$
52	41 51	eqtr3id	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to {(x \in X ⟼ {x ↾}_{B})}^{-1} \circ {(z \in ⋃ K ⟼ z (k))}^{-1} = {(x \in X ⟼ x (k))}^{-1}$
53	52	imaeq1d	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to ({(x \in X ⟼ {x ↾}_{B})}^{-1} \circ {(z \in ⋃ K ⟼ z (k))}^{-1}) [u] = {(x \in X ⟼ x (k))}^{-1} [u]$
54	40 53	eqtr3id	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to {(x \in X ⟼ {x ↾}_{B})}^{-1} [{(z \in ⋃ K ⟼ z (k))}^{-1} [u]] = {(x \in X ⟼ x (k))}^{-1} [u]$
55		simpl1	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to A \in V$
56		simpl2	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to F : A ⟶ Top$
57		simpl3	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to B \subseteq A$
58		simprl	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to k \in B$
59	57 58	sseldd	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to k \in A$
60	1 2	ptpjcn	$⊢ (A \in V \land F : A ⟶ Top \land k \in A) \to (x \in X ⟼ x (k)) \in (J Cn F (k))$
61	55 56 59 60	syl3anc	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to (x \in X ⟼ x (k)) \in (J Cn F (k))$
62		simprr	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to u \in F (k)$
63		cnima	$⊢ ((x \in X ⟼ x (k)) \in (J Cn F (k)) \land u \in F (k)) \to {(x \in X ⟼ x (k))}^{-1} [u] \in J$
64	61 62 63	syl2anc	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to {(x \in X ⟼ x (k))}^{-1} [u] \in J$
65	54 64	eqeltrd	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to {(x \in X ⟼ {x ↾}_{B})}^{-1} [{(z \in ⋃ K ⟼ z (k))}^{-1} [u]] \in J$
66		imaeq2	$⊢ v = {(z \in ⋃ K ⟼ z (k))}^{-1} [u] \to {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] = {(x \in X ⟼ {x ↾}_{B})}^{-1} [{(z \in ⋃ K ⟼ z (k))}^{-1} [u]]$
67	66	eleq1d	$⊢ v = {(z \in ⋃ K ⟼ z (k))}^{-1} [u] \to ({(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J \leftrightarrow {(x \in X ⟼ {x ↾}_{B})}^{-1} [{(z \in ⋃ K ⟼ z (k))}^{-1} [u]] \in J)$
68	65 67	syl5ibrcom	$⊢ ((A \in V \land F : A ⟶ Top \land B \subseteq A) \land (k \in B \land u \in F (k))) \to (v = {(z \in ⋃ K ⟼ z (k))}^{-1} [u] \to {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J)$
69	68	rexlimdvva	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to (\exists k \in B \exists u \in F (k) v = {(z \in ⋃ K ⟼ z (k))}^{-1} [u] \to {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J)$
70	69	alrimiv	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to \forall v (\exists k \in B \exists u \in F (k) v = {(z \in ⋃ K ⟼ z (k))}^{-1} [u] \to {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J)$
71		eqid	$⊢ (k \in B, u \in ({F ↾}_{B}) (k) ⟼ {(z \in ⋃ K ⟼ z (k))}^{-1} [u]) = (k \in B, u \in ({F ↾}_{B}) (k) ⟼ {(z \in ⋃ K ⟼ z (k))}^{-1} [u])$
72	71	rnmpo	$⊢ ran (k \in B, u \in ({F ↾}_{B}) (k) ⟼ {(z \in ⋃ K ⟼ z (k))}^{-1} [u]) = \{y \| \exists k \in B \exists u \in ({F ↾}_{B}) (k) y = {(z \in ⋃ K ⟼ z (k))}^{-1} [u]\}$
73	72	raleqi	$⊢ \forall v \in ran (k \in B, u \in ({F ↾}_{B}) (k) ⟼ {(z \in ⋃ K ⟼ z (k))}^{-1} [u]) {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J \leftrightarrow \forall v \in \{y \| \exists k \in B \exists u \in ({F ↾}_{B}) (k) y = {(z \in ⋃ K ⟼ z (k))}^{-1} [u]\} {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J$
74	13	rexeqdv	$⊢ k \in B \to (\exists u \in ({F ↾}_{B}) (k) y = {(z \in ⋃ K ⟼ z (k))}^{-1} [u] \leftrightarrow \exists u \in F (k) y = {(z \in ⋃ K ⟼ z (k))}^{-1} [u])$
75		eqeq1	$⊢ y = v \to (y = {(z \in ⋃ K ⟼ z (k))}^{-1} [u] \leftrightarrow v = {(z \in ⋃ K ⟼ z (k))}^{-1} [u])$
76	75	rexbidv	$⊢ y = v \to (\exists u \in F (k) y = {(z \in ⋃ K ⟼ z (k))}^{-1} [u] \leftrightarrow \exists u \in F (k) v = {(z \in ⋃ K ⟼ z (k))}^{-1} [u])$
77	74 76	sylan9bbr	$⊢ (y = v \land k \in B) \to (\exists u \in ({F ↾}_{B}) (k) y = {(z \in ⋃ K ⟼ z (k))}^{-1} [u] \leftrightarrow \exists u \in F (k) v = {(z \in ⋃ K ⟼ z (k))}^{-1} [u])$
78	77	rexbidva	$⊢ y = v \to (\exists k \in B \exists u \in ({F ↾}_{B}) (k) y = {(z \in ⋃ K ⟼ z (k))}^{-1} [u] \leftrightarrow \exists k \in B \exists u \in F (k) v = {(z \in ⋃ K ⟼ z (k))}^{-1} [u])$
79	78	ralab	$⊢ \forall v \in \{y \| \exists k \in B \exists u \in ({F ↾}_{B}) (k) y = {(z \in ⋃ K ⟼ z (k))}^{-1} [u]\} {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J \leftrightarrow \forall v (\exists k \in B \exists u \in F (k) v = {(z \in ⋃ K ⟼ z (k))}^{-1} [u] \to {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J)$
80	73 79	bitri	$⊢ \forall v \in ran (k \in B, u \in ({F ↾}_{B}) (k) ⟼ {(z \in ⋃ K ⟼ z (k))}^{-1} [u]) {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J \leftrightarrow \forall v (\exists k \in B \exists u \in F (k) v = {(z \in ⋃ K ⟼ z (k))}^{-1} [u] \to {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J)$
81	70 80	sylibr	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to \forall v \in ran (k \in B, u \in ({F ↾}_{B}) (k) ⟼ {(z \in ⋃ K ⟼ z (k))}^{-1} [u]) {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J$
82		ralunb	$⊢ \forall v \in (\{⋃ K\} \cup ran (k \in B, u \in ({F ↾}_{B}) (k) ⟼ {(z \in ⋃ K ⟼ z (k))}^{-1} [u])) {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J \leftrightarrow (\forall v \in \{⋃ K\} {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J \land \forall v \in ran (k \in B, u \in ({F ↾}_{B}) (k) ⟼ {(z \in ⋃ K ⟼ z (k))}^{-1} [u]) {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J)$
83	39 81 82	sylanbrc	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to \forall v \in (\{⋃ K\} \cup ran (k \in B, u \in ({F ↾}_{B}) (k) ⟼ {(z \in ⋃ K ⟼ z (k))}^{-1} [u])) {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J$
84	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
85	31 84	sylib	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to J \in TopOn (X)$
86		snex	$⊢ \{⋃ K\} \in V$
87		fvex	$⊢ ({F ↾}_{B}) (k) \in V$
88	87	abrexex	$⊢ \{y \| \exists u \in ({F ↾}_{B}) (k) y = {(z \in ⋃ K ⟼ z (k))}^{-1} [u]\} \in V$
89	88	rgenw	$⊢ \forall k \in B \{y \| \exists u \in ({F ↾}_{B}) (k) y = {(z \in ⋃ K ⟼ z (k))}^{-1} [u]\} \in V$
90		abrexex2g	$⊢ (B \in V \land \forall k \in B \{y \| \exists u \in ({F ↾}_{B}) (k) y = {(z \in ⋃ K ⟼ z (k))}^{-1} [u]\} \in V) \to \{y \| \exists k \in B \exists u \in ({F ↾}_{B}) (k) y = {(z \in ⋃ K ⟼ z (k))}^{-1} [u]\} \in V$
91	18 89 90	sylancl	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to \{y \| \exists k \in B \exists u \in ({F ↾}_{B}) (k) y = {(z \in ⋃ K ⟼ z (k))}^{-1} [u]\} \in V$
92	72 91	eqeltrid	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to ran (k \in B, u \in ({F ↾}_{B}) (k) ⟼ {(z \in ⋃ K ⟼ z (k))}^{-1} [u]) \in V$
93		unexg	$⊢ (\{⋃ K\} \in V \land ran (k \in B, u \in ({F ↾}_{B}) (k) ⟼ {(z \in ⋃ K ⟼ z (k))}^{-1} [u]) \in V) \to \{⋃ K\} \cup ran (k \in B, u \in ({F ↾}_{B}) (k) ⟼ {(z \in ⋃ K ⟼ z (k))}^{-1} [u]) \in V$
94	86 92 93	sylancr	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to \{⋃ K\} \cup ran (k \in B, u \in ({F ↾}_{B}) (k) ⟼ {(z \in ⋃ K ⟼ z (k))}^{-1} [u]) \in V$
95		eqid	$⊢ ⋃ K = ⋃ K$
96	3 95 71	ptval2	$⊢ (B \in V \land ({F ↾}_{B}) : B ⟶ Top) \to K = topGen (fi (\{⋃ K\} \cup ran (k \in B, u \in ({F ↾}_{B}) (k) ⟼ {(z \in ⋃ K ⟼ z (k))}^{-1} [u])))$
97	18 20 96	syl2anc	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to K = topGen (fi (\{⋃ K\} \cup ran (k \in B, u \in ({F ↾}_{B}) (k) ⟼ {(z \in ⋃ K ⟼ z (k))}^{-1} [u])))$
98		pttop	$⊢ (B \in V \land ({F ↾}_{B}) : B ⟶ Top) \to \prod_{𝑡} ({F ↾}_{B}) \in Top$
99	18 20 98	syl2anc	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to \prod_{𝑡} ({F ↾}_{B}) \in Top$
100	3 99	eqeltrid	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to K \in Top$
101	95	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
102	100 101	sylib	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to K \in TopOn (⋃ K)$
103	85 94 97 102	subbascn	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to ((x \in X ⟼ {x ↾}_{B}) \in (J Cn K) \leftrightarrow ((x \in X ⟼ {x ↾}_{B}) : X ⟶ ⋃ K \land \forall v \in (\{⋃ K\} \cup ran (k \in B, u \in ({F ↾}_{B}) (k) ⟼ {(z \in ⋃ K ⟼ z (k))}^{-1} [u])) {(x \in X ⟼ {x ↾}_{B})}^{-1} [v] \in J))$
104	26 83 103	mpbir2and	$⊢ (A \in V \land F : A ⟶ Top \land B \subseteq A) \to (x \in X ⟼ {x ↾}_{B}) \in (J Cn K)$

Metamath Proof Explorer

Theorem ptrescn

Proof