xkoccn

Description: The "constant function" function which maps x e. Y to the constant function z e. X |-> x is a continuous function from X into the space of continuous functions from Y to X . This can also be understood as the currying of the first projection function. (The currying of the second projection function is x e. Y |-> ( z e. X |-> z ) , which we already know is continuous because it is a constant function.) (Contributed by Mario Carneiro, 19-Mar-2015)

		Ref	Expression
	Assertion	xkoccn	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to (x \in Y ⟼ X \times \{x\}) \in (S Cn (S^_{ko} R))$

Proof

Step	Hyp	Ref	Expression
1		cnconst2	$⊢ (R \in TopOn (X) \land S \in TopOn (Y) \land x \in Y) \to X \times \{x\} \in (R Cn S)$
2	1	3expa	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land x \in Y) \to X \times \{x\} \in (R Cn S)$
3	2	fmpttd	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to (x \in Y ⟼ X \times \{x\}) : Y ⟶ R Cn S$
4		eqid	$⊢ ⋃ R = ⋃ R$
5		eqid	$⊢ \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\} = \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\}$
6		eqid	$⊢ (k \in \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) = (k \in \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})$
7	4 5 6	xkobval	$⊢ ran (k \in \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) = \{y \| \exists k \in 𝒫 ⋃ R \exists v \in S (R ↾_{𝑡} k \in Comp \land y = \{f \in (R Cn S) \| f [k] \subseteq v\})\}$
8	7	eqabri	$⊢ y \in ran (k \in \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \leftrightarrow \exists k \in 𝒫 ⋃ R \exists v \in S (R ↾_{𝑡} k \in Comp \land y = \{f \in (R Cn S) \| f [k] \subseteq v\})$
9	2	ad5ant15	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k = \emptyset) \land x \in Y) \to X \times \{x\} \in (R Cn S)$
10		simplr	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k = \emptyset) \land x \in Y) \to k = \emptyset$
11	10	imaeq2d	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k = \emptyset) \land x \in Y) \to (X \times \{x\}) [k] = (X \times \{x\}) [\emptyset]$
12		ima0	$⊢ (X \times \{x\}) [\emptyset] = \emptyset$
13		0ss	$⊢ \emptyset \subseteq v$
14	12 13	eqsstri	$⊢ (X \times \{x\}) [\emptyset] \subseteq v$
15	11 14	eqsstrdi	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k = \emptyset) \land x \in Y) \to (X \times \{x\}) [k] \subseteq v$
16		imaeq1	$⊢ f = X \times \{x\} \to f [k] = (X \times \{x\}) [k]$
17	16	sseq1d	$⊢ f = X \times \{x\} \to (f [k] \subseteq v \leftrightarrow (X \times \{x\}) [k] \subseteq v)$
18	17	elrab	$⊢ X \times \{x\} \in \{f \in (R Cn S) \| f [k] \subseteq v\} \leftrightarrow (X \times \{x\} \in (R Cn S) \land (X \times \{x\}) [k] \subseteq v)$
19	9 15 18	sylanbrc	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k = \emptyset) \land x \in Y) \to X \times \{x\} \in \{f \in (R Cn S) \| f [k] \subseteq v\}$
20	19	ralrimiva	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k = \emptyset) \to \forall x \in Y X \times \{x\} \in \{f \in (R Cn S) \| f [k] \subseteq v\}$
21		rabid2	$⊢ Y = \{x \in Y \| X \times \{x\} \in \{f \in (R Cn S) \| f [k] \subseteq v\}\} \leftrightarrow \forall x \in Y X \times \{x\} \in \{f \in (R Cn S) \| f [k] \subseteq v\}$
22	20 21	sylibr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k = \emptyset) \to Y = \{x \in Y \| X \times \{x\} \in \{f \in (R Cn S) \| f [k] \subseteq v\}\}$
23		simpllr	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \to S \in TopOn (Y)$
24		toponmax	$⊢ S \in TopOn (Y) \to Y \in S$
25	23 24	syl	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \to Y \in S$
26	25	adantr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k = \emptyset) \to Y \in S$
27	22 26	eqeltrrd	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k = \emptyset) \to \{x \in Y \| X \times \{x\} \in \{f \in (R Cn S) \| f [k] \subseteq v\}\} \in S$
28		ifnefalse	$⊢ k \neq \emptyset \to if (k = \emptyset, Y, v) = v$
29	28	ad2antlr	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to if (k = \emptyset, Y, v) = v$
30	29	eleq2d	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to (x \in if (k = \emptyset, Y, v) \leftrightarrow x \in v)$
31		vex	$⊢ x \in V$
32	31	snss	$⊢ x \in v \leftrightarrow \{x\} \subseteq v$
33	30 32	bitrdi	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to (x \in if (k = \emptyset, Y, v) \leftrightarrow \{x\} \subseteq v)$
34		df-ima	$⊢ (X \times \{x\}) [k] = ran ({(X \times \{x\}) ↾}_{k})$
35		simplrl	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \to k \in 𝒫 ⋃ R$
36	35	ad2antrr	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to k \in 𝒫 ⋃ R$
37	36	elpwid	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to k \subseteq ⋃ R$
38		toponuni	$⊢ R \in TopOn (X) \to X = ⋃ R$
39	38	ad5antr	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to X = ⋃ R$
40	37 39	sseqtrrd	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to k \subseteq X$
41		xpssres	$⊢ k \subseteq X \to {(X \times \{x\}) ↾}_{k} = k \times \{x\}$
42	40 41	syl	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to {(X \times \{x\}) ↾}_{k} = k \times \{x\}$
43	42	rneqd	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to ran ({(X \times \{x\}) ↾}_{k}) = ran (k \times \{x\})$
44	34 43	eqtrid	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to (X \times \{x\}) [k] = ran (k \times \{x\})$
45		rnxp	$⊢ k \neq \emptyset \to ran (k \times \{x\}) = \{x\}$
46	45	ad2antlr	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to ran (k \times \{x\}) = \{x\}$
47	44 46	eqtrd	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to (X \times \{x\}) [k] = \{x\}$
48	47	sseq1d	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to ((X \times \{x\}) [k] \subseteq v \leftrightarrow \{x\} \subseteq v)$
49	2	ad5ant15	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to X \times \{x\} \in (R Cn S)$
50	49	biantrurd	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to ((X \times \{x\}) [k] \subseteq v \leftrightarrow (X \times \{x\} \in (R Cn S) \land (X \times \{x\}) [k] \subseteq v))$
51	33 48 50	3bitr2d	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to (x \in if (k = \emptyset, Y, v) \leftrightarrow (X \times \{x\} \in (R Cn S) \land (X \times \{x\}) [k] \subseteq v))$
52	30 51	bitr3d	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to (x \in v \leftrightarrow (X \times \{x\} \in (R Cn S) \land (X \times \{x\}) [k] \subseteq v))$
53	52 18	bitr4di	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \land x \in Y) \to (x \in v \leftrightarrow X \times \{x\} \in \{f \in (R Cn S) \| f [k] \subseteq v\})$
54	53	rabbi2dva	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \to Y \cap v = \{x \in Y \| X \times \{x\} \in \{f \in (R Cn S) \| f [k] \subseteq v\}\}$
55		simplrr	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \to v \in S$
56		toponss	$⊢ (S \in TopOn (Y) \land v \in S) \to v \subseteq Y$
57	23 55 56	syl2anc	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \to v \subseteq Y$
58	57	adantr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \to v \subseteq Y$
59		sseqin2	$⊢ v \subseteq Y \leftrightarrow Y \cap v = v$
60	58 59	sylib	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \to Y \cap v = v$
61	54 60	eqtr3d	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \to \{x \in Y \| X \times \{x\} \in \{f \in (R Cn S) \| f [k] \subseteq v\}\} = v$
62	55	adantr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \to v \in S$
63	61 62	eqeltrd	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \land k \neq \emptyset) \to \{x \in Y \| X \times \{x\} \in \{f \in (R Cn S) \| f [k] \subseteq v\}\} \in S$
64	27 63	pm2.61dane	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \to \{x \in Y \| X \times \{x\} \in \{f \in (R Cn S) \| f [k] \subseteq v\}\} \in S$
65		imaeq2	$⊢ y = \{f \in (R Cn S) \| f [k] \subseteq v\} \to {(x \in Y ⟼ X \times \{x\})}^{-1} [y] = {(x \in Y ⟼ X \times \{x\})}^{-1} [\{f \in (R Cn S) \| f [k] \subseteq v\}]$
66		eqid	$⊢ (x \in Y ⟼ X \times \{x\}) = (x \in Y ⟼ X \times \{x\})$
67	66	mptpreima	$⊢ {(x \in Y ⟼ X \times \{x\})}^{-1} [\{f \in (R Cn S) \| f [k] \subseteq v\}] = \{x \in Y \| X \times \{x\} \in \{f \in (R Cn S) \| f [k] \subseteq v\}\}$
68	65 67	eqtrdi	$⊢ y = \{f \in (R Cn S) \| f [k] \subseteq v\} \to {(x \in Y ⟼ X \times \{x\})}^{-1} [y] = \{x \in Y \| X \times \{x\} \in \{f \in (R Cn S) \| f [k] \subseteq v\}\}$
69	68	eleq1d	$⊢ y = \{f \in (R Cn S) \| f [k] \subseteq v\} \to ({(x \in Y ⟼ X \times \{x\})}^{-1} [y] \in S \leftrightarrow \{x \in Y \| X \times \{x\} \in \{f \in (R Cn S) \| f [k] \subseteq v\}\} \in S)$
70	64 69	syl5ibrcom	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \land R ↾_{𝑡} k \in Comp) \to (y = \{f \in (R Cn S) \| f [k] \subseteq v\} \to {(x \in Y ⟼ X \times \{x\})}^{-1} [y] \in S)$
71	70	expimpd	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ R \land v \in S)) \to ((R ↾_{𝑡} k \in Comp \land y = \{f \in (R Cn S) \| f [k] \subseteq v\}) \to {(x \in Y ⟼ X \times \{x\})}^{-1} [y] \in S)$
72	71	rexlimdvva	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to (\exists k \in 𝒫 ⋃ R \exists v \in S (R ↾_{𝑡} k \in Comp \land y = \{f \in (R Cn S) \| f [k] \subseteq v\}) \to {(x \in Y ⟼ X \times \{x\})}^{-1} [y] \in S)$
73	8 72	biimtrid	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to (y \in ran (k \in \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \to {(x \in Y ⟼ X \times \{x\})}^{-1} [y] \in S)$
74	73	ralrimiv	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to \forall y \in ran (k \in \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) {(x \in Y ⟼ X \times \{x\})}^{-1} [y] \in S$
75		simpr	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to S \in TopOn (Y)$
76		ovex	$⊢ R Cn S \in V$
77	76	pwex	$⊢ 𝒫 (R Cn S) \in V$
78	4 5 6	xkotf	$⊢ (k \in \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) : \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\} \times S ⟶ 𝒫 (R Cn S)$
79		frn	$⊢ (k \in \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) : \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\} \times S ⟶ 𝒫 (R Cn S) \to ran (k \in \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \subseteq 𝒫 (R Cn S)$
80	78 79	ax-mp	$⊢ ran (k \in \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \subseteq 𝒫 (R Cn S)$
81	77 80	ssexi	$⊢ ran (k \in \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \in V$
82	81	a1i	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to ran (k \in \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) \in V$
83		topontop	$⊢ R \in TopOn (X) \to R \in Top$
84		topontop	$⊢ S \in TopOn (Y) \to S \in Top$
85	4 5 6	xkoval	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R = topGen (fi (ran (k \in \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})))$
86	83 84 85	syl2an	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to S^_{ko} R = topGen (fi (ran (k \in \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\})))$
87		eqid	$⊢ S^_{ko} R = S^_{ko} R$
88	87	xkotopon	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R \in TopOn (R Cn S)$
89	83 84 88	syl2an	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to S^_{ko} R \in TopOn (R Cn S)$
90	75 82 86 89	subbascn	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to ((x \in Y ⟼ X \times \{x\}) \in (S Cn (S^_{ko} R)) \leftrightarrow ((x \in Y ⟼ X \times \{x\}) : Y ⟶ R Cn S \land \forall y \in ran (k \in \{z \in 𝒫 ⋃ R \| R ↾_{𝑡} z \in Comp\}, v \in S ⟼ \{f \in (R Cn S) \| f [k] \subseteq v\}) {(x \in Y ⟼ X \times \{x\})}^{-1} [y] \in S))$
91	3 74 90	mpbir2and	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to (x \in Y ⟼ X \times \{x\}) \in (S Cn (S^_{ko} R))$

Metamath Proof Explorer

Theorem xkoccn

Proof