xkoptsub

Description: The compact-open topology is finer than the product topology restricted to continuous functions. (Contributed by Mario Carneiro, 19-Mar-2015)

	Ref	Expression
Hypotheses	xkoptsub.x	$⊢ X = ⋃ R$
	xkoptsub.j	$⊢ J = \prod_{𝑡} (X \times \{S\})$
Assertion	xkoptsub	$⊢ (R \in Top \land S \in Top) \to J ↾_{𝑡} (R Cn S) \subseteq S^_{ko} R$

Proof

Step	Hyp	Ref	Expression
1		xkoptsub.x	$⊢ X = ⋃ R$
2		xkoptsub.j	$⊢ J = \prod_{𝑡} (X \times \{S\})$
3	1	topopn	$⊢ R \in Top \to X \in R$
4	3	adantr	$⊢ (R \in Top \land S \in Top) \to X \in R$
5		fconstg	$⊢ S \in Top \to (X \times \{S\}) : X ⟶ \{S\}$
6	5	adantl	$⊢ (R \in Top \land S \in Top) \to (X \times \{S\}) : X ⟶ \{S\}$
7	6	ffnd	$⊢ (R \in Top \land S \in Top) \to (X \times \{S\}) Fn X$
8		eqid	$⊢ \{x \| \exists g ((g Fn X \land \forall y \in X g (y) \in (X \times \{S\}) (y) \land \exists z \in Fin \forall y \in (X ∖ z) g (y) = ⋃ (X \times \{S\}) (y)) \land x = \underset{y \in X}{⨉} g (y))\} = \{x \| \exists g ((g Fn X \land \forall y \in X g (y) \in (X \times \{S\}) (y) \land \exists z \in Fin \forall y \in (X ∖ z) g (y) = ⋃ (X \times \{S\}) (y)) \land x = \underset{y \in X}{⨉} g (y))\}$
9	8	ptval	$⊢ (X \in R \land (X \times \{S\}) Fn X) \to \prod_{𝑡} (X \times \{S\}) = topGen (\{x \| \exists g ((g Fn X \land \forall y \in X g (y) \in (X \times \{S\}) (y) \land \exists z \in Fin \forall y \in (X ∖ z) g (y) = ⋃ (X \times \{S\}) (y)) \land x = \underset{y \in X}{⨉} g (y))\})$
10	4 7 9	syl2anc	$⊢ (R \in Top \land S \in Top) \to \prod_{𝑡} (X \times \{S\}) = topGen (\{x \| \exists g ((g Fn X \land \forall y \in X g (y) \in (X \times \{S\}) (y) \land \exists z \in Fin \forall y \in (X ∖ z) g (y) = ⋃ (X \times \{S\}) (y)) \land x = \underset{y \in X}{⨉} g (y))\})$
11		simpr	$⊢ (R \in Top \land S \in Top) \to S \in Top$
12	11	snssd	$⊢ (R \in Top \land S \in Top) \to \{S\} \subseteq Top$
13	6 12	fssd	$⊢ (R \in Top \land S \in Top) \to (X \times \{S\}) : X ⟶ Top$
14		eqid	$⊢ \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) = \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n)$
15	8 14	ptbasfi	$⊢ (X \in R \land (X \times \{S\}) : X ⟶ Top) \to \{x \| \exists g ((g Fn X \land \forall y \in X g (y) \in (X \times \{S\}) (y) \land \exists z \in Fin \forall y \in (X ∖ z) g (y) = ⋃ (X \times \{S\}) (y)) \land x = \underset{y \in X}{⨉} g (y))\} = fi (\{\underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n)\} \cup ran (k \in X, u \in (X \times \{S\}) (k) ⟼ {(w \in \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) ⟼ w (k))}^{-1} [u]))$
16	4 13 15	syl2anc	$⊢ (R \in Top \land S \in Top) \to \{x \| \exists g ((g Fn X \land \forall y \in X g (y) \in (X \times \{S\}) (y) \land \exists z \in Fin \forall y \in (X ∖ z) g (y) = ⋃ (X \times \{S\}) (y)) \land x = \underset{y \in X}{⨉} g (y))\} = fi (\{\underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n)\} \cup ran (k \in X, u \in (X \times \{S\}) (k) ⟼ {(w \in \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) ⟼ w (k))}^{-1} [u]))$
17		fvconst2g	$⊢ (S \in Top \land n \in X) \to (X \times \{S\}) (n) = S$
18	17	adantll	$⊢ ((R \in Top \land S \in Top) \land n \in X) \to (X \times \{S\}) (n) = S$
19	18	unieqd	$⊢ ((R \in Top \land S \in Top) \land n \in X) \to ⋃ (X \times \{S\}) (n) = ⋃ S$
20	19	ixpeq2dva	$⊢ (R \in Top \land S \in Top) \to \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) = \underset{n \in X}{⨉} ⋃ S$
21		eqid	$⊢ ⋃ S = ⋃ S$
22	21	topopn	$⊢ S \in Top \to ⋃ S \in S$
23		ixpconstg	$⊢ (X \in R \land ⋃ S \in S) \to \underset{n \in X}{⨉} ⋃ S = {⋃ S}^{X}$
24	3 22 23	syl2an	$⊢ (R \in Top \land S \in Top) \to \underset{n \in X}{⨉} ⋃ S = {⋃ S}^{X}$
25	20 24	eqtrd	$⊢ (R \in Top \land S \in Top) \to \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) = {⋃ S}^{X}$
26	25	sneqd	$⊢ (R \in Top \land S \in Top) \to \{\underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n)\} = \{{⋃ S}^{X}\}$
27		eqid	$⊢ X = X$
28		fvconst2g	$⊢ (S \in Top \land k \in X) \to (X \times \{S\}) (k) = S$
29	28	adantll	$⊢ ((R \in Top \land S \in Top) \land k \in X) \to (X \times \{S\}) (k) = S$
30	25	adantr	$⊢ ((R \in Top \land S \in Top) \land k \in X) \to \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) = {⋃ S}^{X}$
31	30	mpteq1d	$⊢ ((R \in Top \land S \in Top) \land k \in X) \to (w \in \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) ⟼ w (k)) = (w \in ({⋃ S}^{X}) ⟼ w (k))$
32	31	cnveqd	$⊢ ((R \in Top \land S \in Top) \land k \in X) \to {(w \in \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) ⟼ w (k))}^{-1} = {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1}$
33	32	imaeq1d	$⊢ ((R \in Top \land S \in Top) \land k \in X) \to {(w \in \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) ⟼ w (k))}^{-1} [u] = {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]$
34	33	ralrimivw	$⊢ ((R \in Top \land S \in Top) \land k \in X) \to \forall u \in (X \times \{S\}) (k) {(w \in \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) ⟼ w (k))}^{-1} [u] = {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]$
35	29 34	jca	$⊢ ((R \in Top \land S \in Top) \land k \in X) \to ((X \times \{S\}) (k) = S \land \forall u \in (X \times \{S\}) (k) {(w \in \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) ⟼ w (k))}^{-1} [u] = {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])$
36	35	ralrimiva	$⊢ (R \in Top \land S \in Top) \to \forall k \in X ((X \times \{S\}) (k) = S \land \forall u \in (X \times \{S\}) (k) {(w \in \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) ⟼ w (k))}^{-1} [u] = {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])$
37		mpoeq123	$⊢ (X = X \land \forall k \in X ((X \times \{S\}) (k) = S \land \forall u \in (X \times \{S\}) (k) {(w \in \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) ⟼ w (k))}^{-1} [u] = {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) \to (k \in X, u \in (X \times \{S\}) (k) ⟼ {(w \in \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) ⟼ w (k))}^{-1} [u]) = (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])$
38	27 36 37	sylancr	$⊢ (R \in Top \land S \in Top) \to (k \in X, u \in (X \times \{S\}) (k) ⟼ {(w \in \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) ⟼ w (k))}^{-1} [u]) = (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])$
39	38	rneqd	$⊢ (R \in Top \land S \in Top) \to ran (k \in X, u \in (X \times \{S\}) (k) ⟼ {(w \in \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) ⟼ w (k))}^{-1} [u]) = ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])$
40	26 39	uneq12d	$⊢ (R \in Top \land S \in Top) \to \{\underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n)\} \cup ran (k \in X, u \in (X \times \{S\}) (k) ⟼ {(w \in \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) ⟼ w (k))}^{-1} [u]) = \{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])$
41	40	fveq2d	$⊢ (R \in Top \land S \in Top) \to fi (\{\underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n)\} \cup ran (k \in X, u \in (X \times \{S\}) (k) ⟼ {(w \in \underset{n \in X}{⨉} ⋃ (X \times \{S\}) (n) ⟼ w (k))}^{-1} [u])) = fi (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]))$
42	16 41	eqtrd	$⊢ (R \in Top \land S \in Top) \to \{x \| \exists g ((g Fn X \land \forall y \in X g (y) \in (X \times \{S\}) (y) \land \exists z \in Fin \forall y \in (X ∖ z) g (y) = ⋃ (X \times \{S\}) (y)) \land x = \underset{y \in X}{⨉} g (y))\} = fi (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]))$
43	42	fveq2d	$⊢ (R \in Top \land S \in Top) \to topGen (\{x \| \exists g ((g Fn X \land \forall y \in X g (y) \in (X \times \{S\}) (y) \land \exists z \in Fin \forall y \in (X ∖ z) g (y) = ⋃ (X \times \{S\}) (y)) \land x = \underset{y \in X}{⨉} g (y))\}) = topGen (fi (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])))$
44	10 43	eqtrd	$⊢ (R \in Top \land S \in Top) \to \prod_{𝑡} (X \times \{S\}) = topGen (fi (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])))$
45	2 44	eqtrid	$⊢ (R \in Top \land S \in Top) \to J = topGen (fi (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])))$
46	45	oveq1d	$⊢ (R \in Top \land S \in Top) \to J ↾_{𝑡} (R Cn S) = topGen (fi (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]))) ↾_{𝑡} (R Cn S)$
47		firest	$⊢ fi ((\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ↾_{𝑡} (R Cn S)) = fi (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ↾_{𝑡} (R Cn S)$
48	47	fveq2i	$⊢ topGen (fi ((\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ↾_{𝑡} (R Cn S))) = topGen (fi (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ↾_{𝑡} (R Cn S))$
49		fvex	$⊢ fi (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) \in V$
50		ovex	$⊢ R Cn S \in V$
51		tgrest	$⊢ (fi (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) \in V \land R Cn S \in V) \to topGen (fi (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ↾_{𝑡} (R Cn S)) = topGen (fi (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]))) ↾_{𝑡} (R Cn S)$
52	49 50 51	mp2an	$⊢ topGen (fi (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ↾_{𝑡} (R Cn S)) = topGen (fi (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]))) ↾_{𝑡} (R Cn S)$
53	48 52	eqtri	$⊢ topGen (fi ((\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ↾_{𝑡} (R Cn S))) = topGen (fi (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]))) ↾_{𝑡} (R Cn S)$
54	46 53	eqtr4di	$⊢ (R \in Top \land S \in Top) \to J ↾_{𝑡} (R Cn S) = topGen (fi ((\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ↾_{𝑡} (R Cn S)))$
55		xkotop	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R \in Top$
56		snex	$⊢ \{{⋃ S}^{X}\} \in V$
57		mpoexga	$⊢ (X \in R \land S \in Top) \to (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]) \in V$
58	3 57	sylan	$⊢ (R \in Top \land S \in Top) \to (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]) \in V$
59		rnexg	$⊢ (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]) \in V \to ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]) \in V$
60	58 59	syl	$⊢ (R \in Top \land S \in Top) \to ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]) \in V$
61		unexg	$⊢ (\{{⋃ S}^{X}\} \in V \land ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]) \in V) \to \{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]) \in V$
62	56 60 61	sylancr	$⊢ (R \in Top \land S \in Top) \to \{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]) \in V$
63		restval	$⊢ (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]) \in V \land R Cn S \in V) \to (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ↾_{𝑡} (R Cn S) = ran (x \in (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ⟼ x \cap (R Cn S))$
64	62 50 63	sylancl	$⊢ (R \in Top \land S \in Top) \to (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ↾_{𝑡} (R Cn S) = ran (x \in (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ⟼ x \cap (R Cn S))$
65		elun	$⊢ x \in (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) \leftrightarrow (x \in \{{⋃ S}^{X}\} \lor x \in ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]))$
66	1 21	cnf	$⊢ x \in (R Cn S) \to x : X ⟶ ⋃ S$
67		elmapg	$⊢ (⋃ S \in S \land X \in R) \to (x \in ({⋃ S}^{X}) \leftrightarrow x : X ⟶ ⋃ S)$
68	22 3 67	syl2anr	$⊢ (R \in Top \land S \in Top) \to (x \in ({⋃ S}^{X}) \leftrightarrow x : X ⟶ ⋃ S)$
69	66 68	imbitrrid	$⊢ (R \in Top \land S \in Top) \to (x \in (R Cn S) \to x \in ({⋃ S}^{X}))$
70	69	ssrdv	$⊢ (R \in Top \land S \in Top) \to R Cn S \subseteq {⋃ S}^{X}$
71	70	adantr	$⊢ ((R \in Top \land S \in Top) \land x \in \{{⋃ S}^{X}\}) \to R Cn S \subseteq {⋃ S}^{X}$
72		elsni	$⊢ x \in \{{⋃ S}^{X}\} \to x = {⋃ S}^{X}$
73	72	adantl	$⊢ ((R \in Top \land S \in Top) \land x \in \{{⋃ S}^{X}\}) \to x = {⋃ S}^{X}$
74	71 73	sseqtrrd	$⊢ ((R \in Top \land S \in Top) \land x \in \{{⋃ S}^{X}\}) \to R Cn S \subseteq x$
75		sseqin2	$⊢ R Cn S \subseteq x \leftrightarrow x \cap (R Cn S) = R Cn S$
76	74 75	sylib	$⊢ ((R \in Top \land S \in Top) \land x \in \{{⋃ S}^{X}\}) \to x \cap (R Cn S) = R Cn S$
77		eqid	$⊢ S^_{ko} R = S^_{ko} R$
78	77	xkouni	$⊢ (R \in Top \land S \in Top) \to R Cn S = ⋃ (S^_{ko} R)$
79		eqid	$⊢ ⋃ (S^_{ko} R) = ⋃ (S^_{ko} R)$
80	79	topopn	$⊢ S^_{ko} R \in Top \to ⋃ (S^_{ko} R) \in (S^_{ko} R)$
81	55 80	syl	$⊢ (R \in Top \land S \in Top) \to ⋃ (S^_{ko} R) \in (S^_{ko} R)$
82	78 81	eqeltrd	$⊢ (R \in Top \land S \in Top) \to R Cn S \in (S^_{ko} R)$
83	82	adantr	$⊢ ((R \in Top \land S \in Top) \land x \in \{{⋃ S}^{X}\}) \to R Cn S \in (S^_{ko} R)$
84	76 83	eqeltrd	$⊢ ((R \in Top \land S \in Top) \land x \in \{{⋃ S}^{X}\}) \to x \cap (R Cn S) \in (S^_{ko} R)$
85		eqid	$⊢ (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]) = (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])$
86	85	rnmpo	$⊢ ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]) = \{x \| \exists k \in X \exists u \in S x = {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]\}$
87	86	eqabri	$⊢ x \in ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]) \leftrightarrow \exists k \in X \exists u \in S x = {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]$
88		cnvresima	$⊢ {({(w \in ({⋃ S}^{X}) ⟼ w (k)) ↾}_{(R Cn S)})}^{-1} [u] = {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u] \cap (R Cn S)$
89	70	adantr	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to R Cn S \subseteq {⋃ S}^{X}$
90	89	resmptd	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to {(w \in ({⋃ S}^{X}) ⟼ w (k)) ↾}_{(R Cn S)} = (w \in (R Cn S) ⟼ w (k))$
91	90	cnveqd	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to {({(w \in ({⋃ S}^{X}) ⟼ w (k)) ↾}_{(R Cn S)})}^{-1} = {(w \in (R Cn S) ⟼ w (k))}^{-1}$
92	91	imaeq1d	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to {({(w \in ({⋃ S}^{X}) ⟼ w (k)) ↾}_{(R Cn S)})}^{-1} [u] = {(w \in (R Cn S) ⟼ w (k))}^{-1} [u]$
93	88 92	eqtr3id	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u] \cap (R Cn S) = {(w \in (R Cn S) ⟼ w (k))}^{-1} [u]$
94		fvex	$⊢ w (k) \in V$
95	94	rgenw	$⊢ \forall w \in (R Cn S) w (k) \in V$
96		eqid	$⊢ (w \in (R Cn S) ⟼ w (k)) = (w \in (R Cn S) ⟼ w (k))$
97	96	fnmpt	$⊢ \forall w \in (R Cn S) w (k) \in V \to (w \in (R Cn S) ⟼ w (k)) Fn (R Cn S)$
98	95 97	mp1i	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to (w \in (R Cn S) ⟼ w (k)) Fn (R Cn S)$
99		elpreima	$⊢ (w \in (R Cn S) ⟼ w (k)) Fn (R Cn S) \to (f \in {(w \in (R Cn S) ⟼ w (k))}^{-1} [u] \leftrightarrow (f \in (R Cn S) \land (w \in (R Cn S) ⟼ w (k)) (f) \in u))$
100	98 99	syl	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to (f \in {(w \in (R Cn S) ⟼ w (k))}^{-1} [u] \leftrightarrow (f \in (R Cn S) \land (w \in (R Cn S) ⟼ w (k)) (f) \in u))$
101		fveq1	$⊢ w = f \to w (k) = f (k)$
102		fvex	$⊢ f (k) \in V$
103	101 96 102	fvmpt	$⊢ f \in (R Cn S) \to (w \in (R Cn S) ⟼ w (k)) (f) = f (k)$
104	103	adantl	$⊢ (((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \land f \in (R Cn S)) \to (w \in (R Cn S) ⟼ w (k)) (f) = f (k)$
105	104	eleq1d	$⊢ (((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \land f \in (R Cn S)) \to ((w \in (R Cn S) ⟼ w (k)) (f) \in u \leftrightarrow f (k) \in u)$
106	102	snss	$⊢ f (k) \in u \leftrightarrow \{f (k)\} \subseteq u$
107	89	sselda	$⊢ (((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \land f \in (R Cn S)) \to f \in ({⋃ S}^{X})$
108		elmapi	$⊢ f \in ({⋃ S}^{X}) \to f : X ⟶ ⋃ S$
109		ffn	$⊢ f : X ⟶ ⋃ S \to f Fn X$
110	107 108 109	3syl	$⊢ (((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \land f \in (R Cn S)) \to f Fn X$
111		simplrl	$⊢ (((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \land f \in (R Cn S)) \to k \in X$
112		fnsnfv	$⊢ (f Fn X \land k \in X) \to \{f (k)\} = f [\{k\}]$
113	110 111 112	syl2anc	$⊢ (((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \land f \in (R Cn S)) \to \{f (k)\} = f [\{k\}]$
114	113	sseq1d	$⊢ (((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \land f \in (R Cn S)) \to (\{f (k)\} \subseteq u \leftrightarrow f [\{k\}] \subseteq u)$
115	106 114	bitrid	$⊢ (((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \land f \in (R Cn S)) \to (f (k) \in u \leftrightarrow f [\{k\}] \subseteq u)$
116	105 115	bitrd	$⊢ (((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \land f \in (R Cn S)) \to ((w \in (R Cn S) ⟼ w (k)) (f) \in u \leftrightarrow f [\{k\}] \subseteq u)$
117	116	pm5.32da	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to ((f \in (R Cn S) \land (w \in (R Cn S) ⟼ w (k)) (f) \in u) \leftrightarrow (f \in (R Cn S) \land f [\{k\}] \subseteq u))$
118	100 117	bitrd	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to (f \in {(w \in (R Cn S) ⟼ w (k))}^{-1} [u] \leftrightarrow (f \in (R Cn S) \land f [\{k\}] \subseteq u))$
119	118	eqabdv	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to {(w \in (R Cn S) ⟼ w (k))}^{-1} [u] = \{f \| (f \in (R Cn S) \land f [\{k\}] \subseteq u)\}$
120		df-rab	$⊢ \{f \in (R Cn S) \| f [\{k\}] \subseteq u\} = \{f \| (f \in (R Cn S) \land f [\{k\}] \subseteq u)\}$
121	119 120	eqtr4di	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to {(w \in (R Cn S) ⟼ w (k))}^{-1} [u] = \{f \in (R Cn S) \| f [\{k\}] \subseteq u\}$
122	93 121	eqtrd	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u] \cap (R Cn S) = \{f \in (R Cn S) \| f [\{k\}] \subseteq u\}$
123		simpll	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to R \in Top$
124	11	adantr	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to S \in Top$
125		simprl	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to k \in X$
126	125	snssd	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to \{k\} \subseteq X$
127	1	toptopon	$⊢ R \in Top \leftrightarrow R \in TopOn (X)$
128	123 127	sylib	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to R \in TopOn (X)$
129		restsn2	$⊢ (R \in TopOn (X) \land k \in X) \to R ↾_{𝑡} \{k\} = 𝒫 \{k\}$
130	128 125 129	syl2anc	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to R ↾_{𝑡} \{k\} = 𝒫 \{k\}$
131		snfi	$⊢ \{k\} \in Fin$
132		discmp	$⊢ \{k\} \in Fin \leftrightarrow 𝒫 \{k\} \in Comp$
133	131 132	mpbi	$⊢ 𝒫 \{k\} \in Comp$
134	130 133	eqeltrdi	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to R ↾_{𝑡} \{k\} \in Comp$
135		simprr	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to u \in S$
136	1 123 124 126 134 135	xkoopn	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to \{f \in (R Cn S) \| f [\{k\}] \subseteq u\} \in (S^_{ko} R)$
137	122 136	eqeltrd	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u] \cap (R Cn S) \in (S^_{ko} R)$
138		ineq1	$⊢ x = {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u] \to x \cap (R Cn S) = {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u] \cap (R Cn S)$
139	138	eleq1d	$⊢ x = {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u] \to (x \cap (R Cn S) \in (S^_{ko} R) \leftrightarrow {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u] \cap (R Cn S) \in (S^_{ko} R))$
140	137 139	syl5ibrcom	$⊢ ((R \in Top \land S \in Top) \land (k \in X \land u \in S)) \to (x = {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u] \to x \cap (R Cn S) \in (S^_{ko} R))$
141	140	rexlimdvva	$⊢ (R \in Top \land S \in Top) \to (\exists k \in X \exists u \in S x = {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u] \to x \cap (R Cn S) \in (S^_{ko} R))$
142	141	imp	$⊢ ((R \in Top \land S \in Top) \land \exists k \in X \exists u \in S x = {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]) \to x \cap (R Cn S) \in (S^_{ko} R)$
143	87 142	sylan2b	$⊢ ((R \in Top \land S \in Top) \land x \in ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) \to x \cap (R Cn S) \in (S^_{ko} R)$
144	84 143	jaodan	$⊢ ((R \in Top \land S \in Top) \land (x \in \{{⋃ S}^{X}\} \lor x \in ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]))) \to x \cap (R Cn S) \in (S^_{ko} R)$
145	65 144	sylan2b	$⊢ ((R \in Top \land S \in Top) \land x \in (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]))) \to x \cap (R Cn S) \in (S^_{ko} R)$
146	145	fmpttd	$⊢ (R \in Top \land S \in Top) \to (x \in (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ⟼ x \cap (R Cn S)) : \{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u]) ⟶ S^_{ko} R$
147	146	frnd	$⊢ (R \in Top \land S \in Top) \to ran (x \in (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ⟼ x \cap (R Cn S)) \subseteq S^_{ko} R$
148	64 147	eqsstrd	$⊢ (R \in Top \land S \in Top) \to (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ↾_{𝑡} (R Cn S) \subseteq S^_{ko} R$
149		tgfiss	$⊢ (S^_{ko} R \in Top \land (\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ↾_{𝑡} (R Cn S) \subseteq S^_{ko} R) \to topGen (fi ((\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ↾_{𝑡} (R Cn S))) \subseteq S^_{ko} R$
150	55 148 149	syl2anc	$⊢ (R \in Top \land S \in Top) \to topGen (fi ((\{{⋃ S}^{X}\} \cup ran (k \in X, u \in S ⟼ {(w \in ({⋃ S}^{X}) ⟼ w (k))}^{-1} [u])) ↾_{𝑡} (R Cn S))) \subseteq S^_{ko} R$
151	54 150	eqsstrd	$⊢ (R \in Top \land S \in Top) \to J ↾_{𝑡} (R Cn S) \subseteq S^_{ko} R$

Metamath Proof Explorer

Theorem xkoptsub

Proof