xkoinjcn

Description: Continuity of "injection", i.e. currying, as a function on continuous function spaces. (Contributed by Mario Carneiro, 23-Mar-2015)

		Ref	Expression
	Hypothesis	xkoinjcn.3	$⊢ F = (x \in X ⟼ (y \in Y ⟼ ⟨y, x⟩))$
	Assertion	xkoinjcn	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to F \in (R Cn ((S \times_{t} R)^_{ko} S))$

Proof

Step	Hyp	Ref	Expression
1		xkoinjcn.3	$⊢ F = (x \in X ⟼ (y \in Y ⟼ ⟨y, x⟩))$
2		simplr	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land x \in X) \to S \in TopOn (Y)$
3	2	cnmptid	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land x \in X) \to (y \in Y ⟼ y) \in (S Cn S)$
4		simpll	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land x \in X) \to R \in TopOn (X)$
5		simpr	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land x \in X) \to x \in X$
6	2 4 5	cnmptc	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land x \in X) \to (y \in Y ⟼ x) \in (S Cn R)$
7	2 3 6	cnmpt1t	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land x \in X) \to (y \in Y ⟼ ⟨y, x⟩) \in (S Cn (S \times_{t} R))$
8	7 1	fmptd	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to F : X ⟶ S Cn (S \times_{t} R)$
9		eqid	$⊢ ⋃ S = ⋃ S$
10		eqid	$⊢ \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\} = \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\}$
11		eqid	$⊢ (k \in \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\}, v \in (S \times_{t} R) ⟼ \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}) = (k \in \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\}, v \in (S \times_{t} R) ⟼ \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\})$
12	9 10 11	xkobval	$⊢ ran (k \in \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\}, v \in (S \times_{t} R) ⟼ \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}) = \{z \| \exists k \in 𝒫 ⋃ S \exists v \in (S \times_{t} R) (S ↾_{𝑡} k \in Comp \land z = \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\})\}$
13	12	abeq2i	$⊢ z \in ran (k \in \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\}, v \in (S \times_{t} R) ⟼ \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}) \leftrightarrow \exists k \in 𝒫 ⋃ S \exists v \in (S \times_{t} R) (S ↾_{𝑡} k \in Comp \land z = \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\})$
14		simpll	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \to (R \in TopOn (X) \land S \in TopOn (Y))$
15	14 7	sylan	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land x \in X) \to (y \in Y ⟼ ⟨y, x⟩) \in (S Cn (S \times_{t} R))$
16		imaeq1	$⊢ f = (y \in Y ⟼ ⟨y, x⟩) \to f [k] = (y \in Y ⟼ ⟨y, x⟩) [k]$
17	16	sseq1d	$⊢ f = (y \in Y ⟼ ⟨y, x⟩) \to (f [k] \subseteq v \leftrightarrow (y \in Y ⟼ ⟨y, x⟩) [k] \subseteq v)$
18	17	elrab3	$⊢ (y \in Y ⟼ ⟨y, x⟩) \in (S Cn (S \times_{t} R)) \to ((y \in Y ⟼ ⟨y, x⟩) \in \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\} \leftrightarrow (y \in Y ⟼ ⟨y, x⟩) [k] \subseteq v)$
19	15 18	syl	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land x \in X) \to ((y \in Y ⟼ ⟨y, x⟩) \in \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\} \leftrightarrow (y \in Y ⟼ ⟨y, x⟩) [k] \subseteq v)$
20		funmpt	$⊢ Fun (y \in Y ⟼ ⟨y, x⟩)$
21		simplrl	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \to k \in 𝒫 ⋃ S$
22	21	elpwid	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \to k \subseteq ⋃ S$
23	14	simprd	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \to S \in TopOn (Y)$
24		toponuni	$⊢ S \in TopOn (Y) \to Y = ⋃ S$
25	23 24	syl	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \to Y = ⋃ S$
26	22 25	sseqtrrd	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \to k \subseteq Y$
27	26	adantr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land x \in X) \to k \subseteq Y$
28		dmmptg	$⊢ \forall y \in Y ⟨y, x⟩ \in V \to dom (y \in Y ⟼ ⟨y, x⟩) = Y$
29		opex	$⊢ ⟨y, x⟩ \in V$
30	29	a1i	$⊢ y \in Y \to ⟨y, x⟩ \in V$
31	28 30	mprg	$⊢ dom (y \in Y ⟼ ⟨y, x⟩) = Y$
32	27 31	sseqtrrdi	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land x \in X) \to k \subseteq dom (y \in Y ⟼ ⟨y, x⟩)$
33		funimass4	$⊢ (Fun (y \in Y ⟼ ⟨y, x⟩) \land k \subseteq dom (y \in Y ⟼ ⟨y, x⟩)) \to ((y \in Y ⟼ ⟨y, x⟩) [k] \subseteq v \leftrightarrow \forall z \in k (y \in Y ⟼ ⟨y, x⟩) (z) \in v)$
34	20 32 33	sylancr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land x \in X) \to ((y \in Y ⟼ ⟨y, x⟩) [k] \subseteq v \leftrightarrow \forall z \in k (y \in Y ⟼ ⟨y, x⟩) (z) \in v)$
35	27	sselda	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land x \in X) \land z \in k) \to z \in Y$
36		opeq1	$⊢ y = z \to ⟨y, x⟩ = ⟨z, x⟩$
37		eqid	$⊢ (y \in Y ⟼ ⟨y, x⟩) = (y \in Y ⟼ ⟨y, x⟩)$
38		opex	$⊢ ⟨z, x⟩ \in V$
39	36 37 38	fvmpt	$⊢ z \in Y \to (y \in Y ⟼ ⟨y, x⟩) (z) = ⟨z, x⟩$
40	35 39	syl	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land x \in X) \land z \in k) \to (y \in Y ⟼ ⟨y, x⟩) (z) = ⟨z, x⟩$
41	40	eleq1d	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land x \in X) \land z \in k) \to ((y \in Y ⟼ ⟨y, x⟩) (z) \in v \leftrightarrow ⟨z, x⟩ \in v)$
42		vex	$⊢ x \in V$
43		opeq2	$⊢ w = x \to ⟨z, w⟩ = ⟨z, x⟩$
44	43	eleq1d	$⊢ w = x \to (⟨z, w⟩ \in v \leftrightarrow ⟨z, x⟩ \in v)$
45	42 44	ralsn	$⊢ \forall w \in \{x\} ⟨z, w⟩ \in v \leftrightarrow ⟨z, x⟩ \in v$
46	41 45	bitr4di	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land x \in X) \land z \in k) \to ((y \in Y ⟼ ⟨y, x⟩) (z) \in v \leftrightarrow \forall w \in \{x\} ⟨z, w⟩ \in v)$
47	46	ralbidva	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land x \in X) \to (\forall z \in k (y \in Y ⟼ ⟨y, x⟩) (z) \in v \leftrightarrow \forall z \in k \forall w \in \{x\} ⟨z, w⟩ \in v)$
48		dfss3	$⊢ k \times \{x\} \subseteq v \leftrightarrow \forall t \in (k \times \{x\}) t \in v$
49		eleq1	$⊢ t = ⟨z, w⟩ \to (t \in v \leftrightarrow ⟨z, w⟩ \in v)$
50	49	ralxp	$⊢ \forall t \in (k \times \{x\}) t \in v \leftrightarrow \forall z \in k \forall w \in \{x\} ⟨z, w⟩ \in v$
51	48 50	bitri	$⊢ k \times \{x\} \subseteq v \leftrightarrow \forall z \in k \forall w \in \{x\} ⟨z, w⟩ \in v$
52	47 51	bitr4di	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land x \in X) \to (\forall z \in k (y \in Y ⟼ ⟨y, x⟩) (z) \in v \leftrightarrow k \times \{x\} \subseteq v)$
53	19 34 52	3bitrd	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land x \in X) \to ((y \in Y ⟼ ⟨y, x⟩) \in \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\} \leftrightarrow k \times \{x\} \subseteq v)$
54	53	rabbidva	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \to \{x \in X \| (y \in Y ⟼ ⟨y, x⟩) \in \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}\} = \{x \in X \| k \times \{x\} \subseteq v\}$
55		sneq	$⊢ x = w \to \{x\} = \{w\}$
56	55	xpeq2d	$⊢ x = w \to k \times \{x\} = k \times \{w\}$
57	56	sseq1d	$⊢ x = w \to (k \times \{x\} \subseteq v \leftrightarrow k \times \{w\} \subseteq v)$
58	57	elrab	$⊢ w \in \{x \in X \| k \times \{x\} \subseteq v\} \leftrightarrow (w \in X \land k \times \{w\} \subseteq v)$
59		eqid	$⊢ ⋃ (S ↾_{𝑡} k) = ⋃ (S ↾_{𝑡} k)$
60		eqid	$⊢ ⋃ R = ⋃ R$
61		simplr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to S ↾_{𝑡} k \in Comp$
62		simpll	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \to R \in TopOn (X)$
63	62	ad2antrr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to R \in TopOn (X)$
64		topontop	$⊢ R \in TopOn (X) \to R \in Top$
65	63 64	syl	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to R \in Top$
66		topontop	$⊢ S \in TopOn (Y) \to S \in Top$
67	66	adantl	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to S \in Top$
68	64	adantr	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to R \in Top$
69		txtop	$⊢ (S \in Top \land R \in Top) \to S \times_{t} R \in Top$
70	67 68 69	syl2anc	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to S \times_{t} R \in Top$
71	70	ad3antrrr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to S \times_{t} R \in Top$
72		vex	$⊢ k \in V$
73		toponmax	$⊢ R \in TopOn (X) \to X \in R$
74	63 73	syl	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to X \in R$
75		xpexg	$⊢ (k \in V \land X \in R) \to k \times X \in V$
76	72 74 75	sylancr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to k \times X \in V$
77		simprr	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \to v \in (S \times_{t} R)$
78	77	ad2antrr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to v \in (S \times_{t} R)$
79		elrestr	$⊢ (S \times_{t} R \in Top \land k \times X \in V \land v \in (S \times_{t} R)) \to v \cap (k \times X) \in ((S \times_{t} R) ↾_{𝑡} (k \times X))$
80	71 76 78 79	syl3anc	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to v \cap (k \times X) \in ((S \times_{t} R) ↾_{𝑡} (k \times X))$
81	67	ad3antrrr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to S \in Top$
82	72	a1i	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to k \in V$
83		txrest	$⊢ ((S \in Top \land R \in Top) \land (k \in V \land X \in R)) \to (S \times_{t} R) ↾_{𝑡} (k \times X) = (S ↾_{𝑡} k) \times_{t} (R ↾_{𝑡} X)$
84	81 65 82 74 83	syl22anc	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to (S \times_{t} R) ↾_{𝑡} (k \times X) = (S ↾_{𝑡} k) \times_{t} (R ↾_{𝑡} X)$
85		toponuni	$⊢ R \in TopOn (X) \to X = ⋃ R$
86	63 85	syl	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to X = ⋃ R$
87	86	oveq2d	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to R ↾_{𝑡} X = R ↾_{𝑡} ⋃ R$
88	60	restid	$⊢ R \in TopOn (X) \to R ↾_{𝑡} ⋃ R = R$
89	63 88	syl	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to R ↾_{𝑡} ⋃ R = R$
90	87 89	eqtrd	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to R ↾_{𝑡} X = R$
91	90	oveq2d	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to (S ↾_{𝑡} k) \times_{t} (R ↾_{𝑡} X) = (S ↾_{𝑡} k) \times_{t} R$
92	84 91	eqtrd	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to (S \times_{t} R) ↾_{𝑡} (k \times X) = (S ↾_{𝑡} k) \times_{t} R$
93	80 92	eleqtrd	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to v \cap (k \times X) \in ((S ↾_{𝑡} k) \times_{t} R)$
94	23	adantr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to S \in TopOn (Y)$
95	26	adantr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to k \subseteq Y$
96		resttopon	$⊢ (S \in TopOn (Y) \land k \subseteq Y) \to S ↾_{𝑡} k \in TopOn (k)$
97	94 95 96	syl2anc	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to S ↾_{𝑡} k \in TopOn (k)$
98		toponuni	$⊢ S ↾_{𝑡} k \in TopOn (k) \to k = ⋃ (S ↾_{𝑡} k)$
99	97 98	syl	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to k = ⋃ (S ↾_{𝑡} k)$
100	99	xpeq1d	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to k \times \{w\} = ⋃ (S ↾_{𝑡} k) \times \{w\}$
101		simprr	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to k \times \{w\} \subseteq v$
102		simprl	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to w \in X$
103	102	snssd	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to \{w\} \subseteq X$
104		xpss2	$⊢ \{w\} \subseteq X \to k \times \{w\} \subseteq k \times X$
105	103 104	syl	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to k \times \{w\} \subseteq k \times X$
106	101 105	ssind	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to k \times \{w\} \subseteq v \cap (k \times X)$
107	100 106	eqsstrrd	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to ⋃ (S ↾_{𝑡} k) \times \{w\} \subseteq v \cap (k \times X)$
108	102 86	eleqtrd	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to w \in ⋃ R$
109	59 60 61 65 93 107 108	txtube	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to \exists r \in R (w \in r \land ⋃ (S ↾_{𝑡} k) \times r \subseteq v \cap (k \times X))$
110		toponss	$⊢ (R \in TopOn (X) \land r \in R) \to r \subseteq X$
111	63 110	sylan	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \land r \in R) \to r \subseteq X$
112		ssrab	$⊢ r \subseteq \{x \in X \| k \times \{x\} \subseteq v\} \leftrightarrow (r \subseteq X \land \forall x \in r k \times \{x\} \subseteq v)$
113	112	baib	$⊢ r \subseteq X \to (r \subseteq \{x \in X \| k \times \{x\} \subseteq v\} \leftrightarrow \forall x \in r k \times \{x\} \subseteq v)$
114	111 113	syl	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \land r \in R) \to (r \subseteq \{x \in X \| k \times \{x\} \subseteq v\} \leftrightarrow \forall x \in r k \times \{x\} \subseteq v)$
115		xpss2	$⊢ r \subseteq X \to k \times r \subseteq k \times X$
116	111 115	syl	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \land r \in R) \to k \times r \subseteq k \times X$
117	116	biantrud	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \land r \in R) \to (k \times r \subseteq v \leftrightarrow (k \times r \subseteq v \land k \times r \subseteq k \times X))$
118		iunid	$⊢ ⋃_{x \in r} \{x\} = r$
119	118	xpeq2i	$⊢ k \times ⋃_{x \in r} \{x\} = k \times r$
120		xpiundi	$⊢ k \times ⋃_{x \in r} \{x\} = ⋃_{x \in r} (k \times \{x\})$
121	119 120	eqtr3i	$⊢ k \times r = ⋃_{x \in r} (k \times \{x\})$
122	121	sseq1i	$⊢ k \times r \subseteq v \leftrightarrow ⋃_{x \in r} (k \times \{x\}) \subseteq v$
123		iunss	$⊢ ⋃_{x \in r} (k \times \{x\}) \subseteq v \leftrightarrow \forall x \in r k \times \{x\} \subseteq v$
124	122 123	bitri	$⊢ k \times r \subseteq v \leftrightarrow \forall x \in r k \times \{x\} \subseteq v$
125		ssin	$⊢ (k \times r \subseteq v \land k \times r \subseteq k \times X) \leftrightarrow k \times r \subseteq v \cap (k \times X)$
126	117 124 125	3bitr3g	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \land r \in R) \to (\forall x \in r k \times \{x\} \subseteq v \leftrightarrow k \times r \subseteq v \cap (k \times X))$
127	99	adantr	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \land r \in R) \to k = ⋃ (S ↾_{𝑡} k)$
128	127	xpeq1d	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \land r \in R) \to k \times r = ⋃ (S ↾_{𝑡} k) \times r$
129	128	sseq1d	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \land r \in R) \to (k \times r \subseteq v \cap (k \times X) \leftrightarrow ⋃ (S ↾_{𝑡} k) \times r \subseteq v \cap (k \times X))$
130	114 126 129	3bitrd	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \land r \in R) \to (r \subseteq \{x \in X \| k \times \{x\} \subseteq v\} \leftrightarrow ⋃ (S ↾_{𝑡} k) \times r \subseteq v \cap (k \times X))$
131	130	anbi2d	$⊢ (((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \land r \in R) \to ((w \in r \land r \subseteq \{x \in X \| k \times \{x\} \subseteq v\}) \leftrightarrow (w \in r \land ⋃ (S ↾_{𝑡} k) \times r \subseteq v \cap (k \times X)))$
132	131	rexbidva	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to (\exists r \in R (w \in r \land r \subseteq \{x \in X \| k \times \{x\} \subseteq v\}) \leftrightarrow \exists r \in R (w \in r \land ⋃ (S ↾_{𝑡} k) \times r \subseteq v \cap (k \times X)))$
133	109 132	mpbird	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land (w \in X \land k \times \{w\} \subseteq v)) \to \exists r \in R (w \in r \land r \subseteq \{x \in X \| k \times \{x\} \subseteq v\})$
134	58 133	sylan2b	$⊢ ((((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \land w \in \{x \in X \| k \times \{x\} \subseteq v\}) \to \exists r \in R (w \in r \land r \subseteq \{x \in X \| k \times \{x\} \subseteq v\})$
135	134	ralrimiva	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \to \forall w \in \{x \in X \| k \times \{x\} \subseteq v\} \exists r \in R (w \in r \land r \subseteq \{x \in X \| k \times \{x\} \subseteq v\})$
136		eltop2	$⊢ R \in Top \to (\{x \in X \| k \times \{x\} \subseteq v\} \in R \leftrightarrow \forall w \in \{x \in X \| k \times \{x\} \subseteq v\} \exists r \in R (w \in r \land r \subseteq \{x \in X \| k \times \{x\} \subseteq v\}))$
137	14 68 136	3syl	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \to (\{x \in X \| k \times \{x\} \subseteq v\} \in R \leftrightarrow \forall w \in \{x \in X \| k \times \{x\} \subseteq v\} \exists r \in R (w \in r \land r \subseteq \{x \in X \| k \times \{x\} \subseteq v\}))$
138	135 137	mpbird	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \to \{x \in X \| k \times \{x\} \subseteq v\} \in R$
139	54 138	eqeltrd	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \to \{x \in X \| (y \in Y ⟼ ⟨y, x⟩) \in \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}\} \in R$
140		imaeq2	$⊢ z = \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\} \to F^{-1} [z] = F^{-1} [\{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}]$
141	1	mptpreima	$⊢ F^{-1} [\{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}] = \{x \in X \| (y \in Y ⟼ ⟨y, x⟩) \in \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}\}$
142	140 141	eqtrdi	$⊢ z = \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\} \to F^{-1} [z] = \{x \in X \| (y \in Y ⟼ ⟨y, x⟩) \in \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}\}$
143	142	eleq1d	$⊢ z = \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\} \to (F^{-1} [z] \in R \leftrightarrow \{x \in X \| (y \in Y ⟼ ⟨y, x⟩) \in \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}\} \in R)$
144	139 143	syl5ibrcom	$⊢ (((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \land S ↾_{𝑡} k \in Comp) \to (z = \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\} \to F^{-1} [z] \in R)$
145	144	expimpd	$⊢ ((R \in TopOn (X) \land S \in TopOn (Y)) \land (k \in 𝒫 ⋃ S \land v \in (S \times_{t} R))) \to ((S ↾_{𝑡} k \in Comp \land z = \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}) \to F^{-1} [z] \in R)$
146	145	rexlimdvva	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to (\exists k \in 𝒫 ⋃ S \exists v \in (S \times_{t} R) (S ↾_{𝑡} k \in Comp \land z = \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}) \to F^{-1} [z] \in R)$
147	13 146	syl5bi	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to (z \in ran (k \in \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\}, v \in (S \times_{t} R) ⟼ \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}) \to F^{-1} [z] \in R)$
148	147	ralrimiv	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to \forall z \in ran (k \in \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\}, v \in (S \times_{t} R) ⟼ \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}) F^{-1} [z] \in R$
149		simpl	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to R \in TopOn (X)$
150		ovex	$⊢ S Cn (S \times_{t} R) \in V$
151	150	pwex	$⊢ 𝒫 (S Cn (S \times_{t} R)) \in V$
152	9 10 11	xkotf	$⊢ (k \in \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\}, v \in (S \times_{t} R) ⟼ \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}) : \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\} \times (S \times_{t} R) ⟶ 𝒫 (S Cn (S \times_{t} R))$
153		frn	$⊢ (k \in \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\}, v \in (S \times_{t} R) ⟼ \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}) : \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\} \times (S \times_{t} R) ⟶ 𝒫 (S Cn (S \times_{t} R)) \to ran (k \in \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\}, v \in (S \times_{t} R) ⟼ \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}) \subseteq 𝒫 (S Cn (S \times_{t} R))$
154	152 153	ax-mp	$⊢ ran (k \in \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\}, v \in (S \times_{t} R) ⟼ \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}) \subseteq 𝒫 (S Cn (S \times_{t} R))$
155	151 154	ssexi	$⊢ ran (k \in \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\}, v \in (S \times_{t} R) ⟼ \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}) \in V$
156	155	a1i	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to ran (k \in \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\}, v \in (S \times_{t} R) ⟼ \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}) \in V$
157	9 10 11	xkoval	$⊢ (S \in Top \land S \times_{t} R \in Top) \to (S \times_{t} R)^_{ko} S = topGen (fi (ran (k \in \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\}, v \in (S \times_{t} R) ⟼ \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\})))$
158	67 70 157	syl2anc	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to (S \times_{t} R)^_{ko} S = topGen (fi (ran (k \in \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\}, v \in (S \times_{t} R) ⟼ \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\})))$
159		eqid	$⊢ (S \times_{t} R)^_{ko} S = (S \times_{t} R)^_{ko} S$
160	159	xkotopon	$⊢ (S \in Top \land S \times_{t} R \in Top) \to (S \times_{t} R)^_{ko} S \in TopOn (S Cn (S \times_{t} R))$
161	67 70 160	syl2anc	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to (S \times_{t} R)^_{ko} S \in TopOn (S Cn (S \times_{t} R))$
162	149 156 158 161	subbascn	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to (F \in (R Cn ((S \times_{t} R)^_{ko} S)) \leftrightarrow (F : X ⟶ S Cn (S \times_{t} R) \land \forall z \in ran (k \in \{w \in 𝒫 ⋃ S \| S ↾_{𝑡} w \in Comp\}, v \in (S \times_{t} R) ⟼ \{f \in (S Cn (S \times_{t} R)) \| f [k] \subseteq v\}) F^{-1} [z] \in R))$
163	8 148 162	mpbir2and	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to F \in (R Cn ((S \times_{t} R)^_{ko} S))$

Metamath Proof Explorer

Theorem xkoinjcn

Proof