xkococnlem

Description: Continuity of the composition operation as a function on continuous function spaces. (Contributed by Mario Carneiro, 20-Mar-2015) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	xkococn.1	$⊢ F = (f \in (S Cn T), g \in (R Cn S) ⟼ f \circ g)$
	xkococn.s	$⊢ φ \to S \in N-LocallyComp$
	xkococn.k	$⊢ φ \to K \subseteq ⋃ R$
	xkococn.c	$⊢ φ \to R ↾_{𝑡} K \in Comp$
	xkococn.v	$⊢ φ \to V \in T$
	xkococn.a	$⊢ φ \to A \in (S Cn T)$
	xkococn.b	$⊢ φ \to B \in (R Cn S)$
	xkococn.i	$⊢ φ \to (A \circ B) [K] \subseteq V$
Assertion	xkococnlem	$⊢ φ \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (⟨A, B⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [K] \subseteq V\}])$

Proof

Step	Hyp	Ref	Expression
1		xkococn.1	$⊢ F = (f \in (S Cn T), g \in (R Cn S) ⟼ f \circ g)$
2		xkococn.s	$⊢ φ \to S \in N-LocallyComp$
3		xkococn.k	$⊢ φ \to K \subseteq ⋃ R$
4		xkococn.c	$⊢ φ \to R ↾_{𝑡} K \in Comp$
5		xkococn.v	$⊢ φ \to V \in T$
6		xkococn.a	$⊢ φ \to A \in (S Cn T)$
7		xkococn.b	$⊢ φ \to B \in (R Cn S)$
8		xkococn.i	$⊢ φ \to (A \circ B) [K] \subseteq V$
9		imacmp	$⊢ (B \in (R Cn S) \land R ↾_{𝑡} K \in Comp) \to S ↾_{𝑡} B [K] \in Comp$
10	7 4 9	syl2anc	$⊢ φ \to S ↾_{𝑡} B [K] \in Comp$
11	2	adantr	$⊢ (φ \land x \in B [K]) \to S \in N-LocallyComp$
12		cnima	$⊢ (A \in (S Cn T) \land V \in T) \to A^{-1} [V] \in S$
13	6 5 12	syl2anc	$⊢ φ \to A^{-1} [V] \in S$
14	13	adantr	$⊢ (φ \land x \in B [K]) \to A^{-1} [V] \in S$
15		imaco	$⊢ (A \circ B) [K] = A [B [K]]$
16	15 8	eqsstrrid	$⊢ φ \to A [B [K]] \subseteq V$
17		eqid	$⊢ ⋃ S = ⋃ S$
18		eqid	$⊢ ⋃ T = ⋃ T$
19	17 18	cnf	$⊢ A \in (S Cn T) \to A : ⋃ S ⟶ ⋃ T$
20		ffun	$⊢ A : ⋃ S ⟶ ⋃ T \to Fun A$
21	6 19 20	3syl	$⊢ φ \to Fun A$
22		imassrn	$⊢ B [K] \subseteq ran B$
23		eqid	$⊢ ⋃ R = ⋃ R$
24	23 17	cnf	$⊢ B \in (R Cn S) \to B : ⋃ R ⟶ ⋃ S$
25		frn	$⊢ B : ⋃ R ⟶ ⋃ S \to ran B \subseteq ⋃ S$
26	7 24 25	3syl	$⊢ φ \to ran B \subseteq ⋃ S$
27	22 26	sstrid	$⊢ φ \to B [K] \subseteq ⋃ S$
28		fdm	$⊢ A : ⋃ S ⟶ ⋃ T \to dom A = ⋃ S$
29	6 19 28	3syl	$⊢ φ \to dom A = ⋃ S$
30	27 29	sseqtrrd	$⊢ φ \to B [K] \subseteq dom A$
31		funimass3	$⊢ (Fun A \land B [K] \subseteq dom A) \to (A [B [K]] \subseteq V \leftrightarrow B [K] \subseteq A^{-1} [V])$
32	21 30 31	syl2anc	$⊢ φ \to (A [B [K]] \subseteq V \leftrightarrow B [K] \subseteq A^{-1} [V])$
33	16 32	mpbid	$⊢ φ \to B [K] \subseteq A^{-1} [V]$
34	33	sselda	$⊢ (φ \land x \in B [K]) \to x \in A^{-1} [V]$
35		nlly2i	$⊢ (S \in N-LocallyComp\landA^{-1} [V] \in S\landx \in A^{-1} [V]\to\exists s \in 𝒫 A^{-1} [V])$
36	11 14 34 35	syl3anc	$⊢ (φ \land x \in B [K]) \to \exists s \in 𝒫 A^{-1} [V] \exists u \in S (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp)$
37		nllytop	$⊢ S \in N-LocallyComp\toS \in Top$
38	2 37	syl	$⊢ φ \to S \in Top$
39	38	ad3antrrr	$⊢ (((φ \land x \in B [K]) \land s \in 𝒫 A^{-1} [V]) \land (u \in S \land (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp))) \to S \in Top$
40		imaexg	$⊢ B \in (R Cn S) \to B [K] \in V$
41	7 40	syl	$⊢ φ \to B [K] \in V$
42	41	ad3antrrr	$⊢ (((φ \land x \in B [K]) \land s \in 𝒫 A^{-1} [V]) \land (u \in S \land (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp))) \to B [K] \in V$
43		simprl	$⊢ (((φ \land x \in B [K]) \land s \in 𝒫 A^{-1} [V]) \land (u \in S \land (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp))) \to u \in S$
44		elrestr	$⊢ (S \in Top \land B [K] \in V \land u \in S) \to u \cap B [K] \in (S ↾_{𝑡} B [K])$
45	39 42 43 44	syl3anc	$⊢ (((φ \land x \in B [K]) \land s \in 𝒫 A^{-1} [V]) \land (u \in S \land (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp))) \to u \cap B [K] \in (S ↾_{𝑡} B [K])$
46		simprr1	$⊢ (((φ \land x \in B [K]) \land s \in 𝒫 A^{-1} [V]) \land (u \in S \land (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp))) \to x \in u$
47		simpllr	$⊢ (((φ \land x \in B [K]) \land s \in 𝒫 A^{-1} [V]) \land (u \in S \land (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp))) \to x \in B [K]$
48	46 47	elind	$⊢ (((φ \land x \in B [K]) \land s \in 𝒫 A^{-1} [V]) \land (u \in S \land (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp))) \to x \in (u \cap B [K])$
49		inss1	$⊢ u \cap B [K] \subseteq u$
50		elpwi	$⊢ s \in 𝒫 A^{-1} [V] \to s \subseteq A^{-1} [V]$
51	50	ad2antlr	$⊢ (((φ \land x \in B [K]) \land s \in 𝒫 A^{-1} [V]) \land (u \in S \land (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp))) \to s \subseteq A^{-1} [V]$
52		elssuni	$⊢ A^{-1} [V] \in S \to A^{-1} [V] \subseteq ⋃ S$
53	13 52	syl	$⊢ φ \to A^{-1} [V] \subseteq ⋃ S$
54	53	ad3antrrr	$⊢ (((φ \land x \in B [K]) \land s \in 𝒫 A^{-1} [V]) \land (u \in S \land (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp))) \to A^{-1} [V] \subseteq ⋃ S$
55	51 54	sstrd	$⊢ (((φ \land x \in B [K]) \land s \in 𝒫 A^{-1} [V]) \land (u \in S \land (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp))) \to s \subseteq ⋃ S$
56		simprr2	$⊢ (((φ \land x \in B [K]) \land s \in 𝒫 A^{-1} [V]) \land (u \in S \land (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp))) \to u \subseteq s$
57	17	ssntr	$⊢ ((S \in Top \land s \subseteq ⋃ S) \land (u \in S \land u \subseteq s)) \to u \subseteq int (S) (s)$
58	39 55 43 56 57	syl22anc	$⊢ (((φ \land x \in B [K]) \land s \in 𝒫 A^{-1} [V]) \land (u \in S \land (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp))) \to u \subseteq int (S) (s)$
59	49 58	sstrid	$⊢ (((φ \land x \in B [K]) \land s \in 𝒫 A^{-1} [V]) \land (u \in S \land (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp))) \to u \cap B [K] \subseteq int (S) (s)$
60		simprr3	$⊢ (((φ \land x \in B [K]) \land s \in 𝒫 A^{-1} [V]) \land (u \in S \land (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp))) \to S ↾_{𝑡} s \in Comp$
61	59 60	jca	$⊢ (((φ \land x \in B [K]) \land s \in 𝒫 A^{-1} [V]) \land (u \in S \land (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp))) \to (u \cap B [K] \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp)$
62		eleq2	$⊢ y = u \cap B [K] \to (x \in y \leftrightarrow x \in (u \cap B [K]))$
63		cleq1lem	$⊢ y = u \cap B [K] \to ((y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp) \leftrightarrow (u \cap B [K] \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp))$
64	62 63	anbi12d	$⊢ y = u \cap B [K] \to ((x \in y \land (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp)) \leftrightarrow (x \in (u \cap B [K]) \land (u \cap B [K] \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp)))$
65	64	rspcev	$⊢ (u \cap B [K] \in (S ↾_{𝑡} B [K]) \land (x \in (u \cap B [K]) \land (u \cap B [K] \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp))) \to \exists y \in (S ↾_{𝑡} B [K]) (x \in y \land (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp))$
66	45 48 61 65	syl12anc	$⊢ (((φ \land x \in B [K]) \land s \in 𝒫 A^{-1} [V]) \land (u \in S \land (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp))) \to \exists y \in (S ↾_{𝑡} B [K]) (x \in y \land (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp))$
67	66	rexlimdvaa	$⊢ ((φ \land x \in B [K]) \land s \in 𝒫 A^{-1} [V]) \to (\exists u \in S (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp) \to \exists y \in (S ↾_{𝑡} B [K]) (x \in y \land (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp)))$
68	67	reximdva	$⊢ (φ \land x \in B [K]) \to (\exists s \in 𝒫 A^{-1} [V] \exists u \in S (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp) \to \exists s \in 𝒫 A^{-1} [V] \exists y \in (S ↾_{𝑡} B [K]) (x \in y \land (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp)))$
69	36 68	mpd	$⊢ (φ \land x \in B [K]) \to \exists s \in 𝒫 A^{-1} [V] \exists y \in (S ↾_{𝑡} B [K]) (x \in y \land (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp))$
70		rexcom	$⊢ \exists s \in 𝒫 A^{-1} [V] \exists y \in (S ↾_{𝑡} B [K]) (x \in y \land (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp)) \leftrightarrow \exists y \in (S ↾_{𝑡} B [K]) \exists s \in 𝒫 A^{-1} [V] (x \in y \land (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp))$
71		r19.42v	$⊢ \exists s \in 𝒫 A^{-1} [V] (x \in y \land (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp)) \leftrightarrow (x \in y \land \exists s \in 𝒫 A^{-1} [V] (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp))$
72	71	rexbii	$⊢ \exists y \in (S ↾_{𝑡} B [K]) \exists s \in 𝒫 A^{-1} [V] (x \in y \land (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp)) \leftrightarrow \exists y \in (S ↾_{𝑡} B [K]) (x \in y \land \exists s \in 𝒫 A^{-1} [V] (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp))$
73	70 72	bitri	$⊢ \exists s \in 𝒫 A^{-1} [V] \exists y \in (S ↾_{𝑡} B [K]) (x \in y \land (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp)) \leftrightarrow \exists y \in (S ↾_{𝑡} B [K]) (x \in y \land \exists s \in 𝒫 A^{-1} [V] (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp))$
74	69 73	sylib	$⊢ (φ \land x \in B [K]) \to \exists y \in (S ↾_{𝑡} B [K]) (x \in y \land \exists s \in 𝒫 A^{-1} [V] (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp))$
75	74	ralrimiva	$⊢ φ \to \forall x \in B [K] \exists y \in (S ↾_{𝑡} B [K]) (x \in y \land \exists s \in 𝒫 A^{-1} [V] (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp))$
76	17	restuni	$⊢ (S \in Top \land B [K] \subseteq ⋃ S) \to B [K] = ⋃ (S ↾_{𝑡} B [K])$
77	38 27 76	syl2anc	$⊢ φ \to B [K] = ⋃ (S ↾_{𝑡} B [K])$
78	75 77	raleqtrdv	$⊢ φ \to \forall x \in ⋃ (S ↾_{𝑡} B [K]) \exists y \in (S ↾_{𝑡} B [K]) (x \in y \land \exists s \in 𝒫 A^{-1} [V] (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp))$
79		eqid	$⊢ ⋃ (S ↾_{𝑡} B [K]) = ⋃ (S ↾_{𝑡} B [K])$
80		fveq2	$⊢ s = k (y) \to int (S) (s) = int (S) (k (y))$
81	80	sseq2d	$⊢ s = k (y) \to (y \subseteq int (S) (s) \leftrightarrow y \subseteq int (S) (k (y)))$
82		oveq2	$⊢ s = k (y) \to S ↾_{𝑡} s = S ↾_{𝑡} k (y)$
83	82	eleq1d	$⊢ s = k (y) \to (S ↾_{𝑡} s \in Comp \leftrightarrow S ↾_{𝑡} k (y) \in Comp)$
84	81 83	anbi12d	$⊢ s = k (y) \to ((y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp) \leftrightarrow (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp))$
85	79 84	cmpcovf	$⊢ (S ↾_{𝑡} B [K] \in Comp \land \forall x \in ⋃ (S ↾_{𝑡} B [K]) \exists y \in (S ↾_{𝑡} B [K]) (x \in y \land \exists s \in 𝒫 A^{-1} [V] (y \subseteq int (S) (s) \land S ↾_{𝑡} s \in Comp))) \to \exists w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin) (⋃ (S ↾_{𝑡} B [K]) = ⋃ w \land \exists k (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))$
86	10 78 85	syl2anc	$⊢ φ \to \exists w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin) (⋃ (S ↾_{𝑡} B [K]) = ⋃ w \land \exists k (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))$
87	77	adantr	$⊢ (φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \to B [K] = ⋃ (S ↾_{𝑡} B [K])$
88	87	eqeq1d	$⊢ (φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \to (B [K] = ⋃ w \leftrightarrow ⋃ (S ↾_{𝑡} B [K]) = ⋃ w)$
89	88	biimpar	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land ⋃ (S ↾_{𝑡} B [K]) = ⋃ w) \to B [K] = ⋃ w$
90	38	ad2antrr	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to S \in Top$
91		cntop2	$⊢ A \in (S Cn T) \to T \in Top$
92	6 91	syl	$⊢ φ \to T \in Top$
93	92	ad2antrr	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to T \in Top$
94		xkotop	$⊢ (S \in Top \land T \in Top) \to T^_{ko} S \in Top$
95	90 93 94	syl2anc	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to T^_{ko} S \in Top$
96		cntop1	$⊢ B \in (R Cn S) \to R \in Top$
97	7 96	syl	$⊢ φ \to R \in Top$
98	97	ad2antrr	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to R \in Top$
99		xkotop	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R \in Top$
100	98 90 99	syl2anc	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to S^_{ko} R \in Top$
101		simprrl	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to k : w ⟶ 𝒫 A^{-1} [V]$
102	101	frnd	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to ran k \subseteq 𝒫 A^{-1} [V]$
103		sspwuni	$⊢ ran k \subseteq 𝒫 A^{-1} [V] \leftrightarrow ⋃ ran k \subseteq A^{-1} [V]$
104	102 103	sylib	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to ⋃ ran k \subseteq A^{-1} [V]$
105	13	ad2antrr	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to A^{-1} [V] \in S$
106	105 52	syl	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to A^{-1} [V] \subseteq ⋃ S$
107	104 106	sstrd	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to ⋃ ran k \subseteq ⋃ S$
108		ffn	$⊢ k : w ⟶ 𝒫 A^{-1} [V] \to k Fn w$
109		fniunfv	$⊢ k Fn w \to ⋃_{y \in w} k (y) = ⋃ ran k$
110	101 108 109	3syl	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to ⋃_{y \in w} k (y) = ⋃ ran k$
111	110	oveq2d	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to S ↾_{𝑡} ⋃_{y \in w} k (y) = S ↾_{𝑡} ⋃ ran k$
112		simplr	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)$
113	112	elin2d	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to w \in Fin$
114		simprrr	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)$
115		simpr	$⊢ (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp) \to S ↾_{𝑡} k (y) \in Comp$
116	115	ralimi	$⊢ \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp) \to \forall y \in w S ↾_{𝑡} k (y) \in Comp$
117	114 116	syl	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to \forall y \in w S ↾_{𝑡} k (y) \in Comp$
118	17	fiuncmp	$⊢ (S \in Top \land w \in Fin \land \forall y \in w S ↾_{𝑡} k (y) \in Comp) \to S ↾_{𝑡} ⋃_{y \in w} k (y) \in Comp$
119	90 113 117 118	syl3anc	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to S ↾_{𝑡} ⋃_{y \in w} k (y) \in Comp$
120	111 119	eqeltrrd	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to S ↾_{𝑡} ⋃ ran k \in Comp$
121	5	ad2antrr	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to V \in T$
122	17 90 93 107 120 121	xkoopn	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \in (T^_{ko} S)$
123	3	ad2antrr	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to K \subseteq ⋃ R$
124	4	ad2antrr	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to R ↾_{𝑡} K \in Comp$
125	110 107	eqsstrd	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to ⋃_{y \in w} k (y) \subseteq ⋃ S$
126		iunss	$⊢ ⋃_{y \in w} k (y) \subseteq ⋃ S \leftrightarrow \forall y \in w k (y) \subseteq ⋃ S$
127	125 126	sylib	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to \forall y \in w k (y) \subseteq ⋃ S$
128	17	ntropn	$⊢ (S \in Top \land k (y) \subseteq ⋃ S) \to int (S) (k (y)) \in S$
129	128	ex	$⊢ S \in Top \to (k (y) \subseteq ⋃ S \to int (S) (k (y)) \in S)$
130	129	ralimdv	$⊢ S \in Top \to (\forall y \in w k (y) \subseteq ⋃ S \to \forall y \in w int (S) (k (y)) \in S)$
131	90 127 130	sylc	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to \forall y \in w int (S) (k (y)) \in S$
132		iunopn	$⊢ (S \in Top \land \forall y \in w int (S) (k (y)) \in S) \to ⋃_{y \in w} int (S) (k (y)) \in S$
133	90 131 132	syl2anc	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to ⋃_{y \in w} int (S) (k (y)) \in S$
134	23 98 90 123 124 133	xkoopn	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \in (S^_{ko} R)$
135		txopn	$⊢ ((T^_{ko} S \in Top \land S^_{ko} R \in Top) \land (\{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \in (T^_{ko} S) \land \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \in (S^_{ko} R))) \to \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \in ((T^_{ko} S) \times_{t} (S^_{ko} R))$
136	95 100 122 134 135	syl22anc	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \in ((T^_{ko} S) \times_{t} (S^_{ko} R))$
137		imaeq1	$⊢ a = A \to a [⋃ ran k] = A [⋃ ran k]$
138	137	sseq1d	$⊢ a = A \to (a [⋃ ran k] \subseteq V \leftrightarrow A [⋃ ran k] \subseteq V)$
139	6	ad2antrr	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to A \in (S Cn T)$
140		imaiun	$⊢ A [⋃_{y \in w} k (y)] = ⋃_{y \in w} A [k (y)]$
141	110	imaeq2d	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to A [⋃_{y \in w} k (y)] = A [⋃ ran k]$
142	140 141	eqtr3id	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to ⋃_{y \in w} A [k (y)] = A [⋃ ran k]$
143	110 104	eqsstrd	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to ⋃_{y \in w} k (y) \subseteq A^{-1} [V]$
144	21	ad2antrr	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to Fun A$
145	101 108	syl	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to k Fn w$
146	29	ad2antrr	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to dom A = ⋃ S$
147	107 146	sseqtrrd	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to ⋃ ran k \subseteq dom A$
148		simpl1	$⊢ ((Fun A \land k Fn w \land ⋃ ran k \subseteq dom A) \land y \in w) \to Fun A$
149	109	3ad2ant2	$⊢ (Fun A \land k Fn w \land ⋃ ran k \subseteq dom A) \to ⋃_{y \in w} k (y) = ⋃ ran k$
150		simp3	$⊢ (Fun A \land k Fn w \land ⋃ ran k \subseteq dom A) \to ⋃ ran k \subseteq dom A$
151	149 150	eqsstrd	$⊢ (Fun A \land k Fn w \land ⋃ ran k \subseteq dom A) \to ⋃_{y \in w} k (y) \subseteq dom A$
152		iunss	$⊢ ⋃_{y \in w} k (y) \subseteq dom A \leftrightarrow \forall y \in w k (y) \subseteq dom A$
153	151 152	sylib	$⊢ (Fun A \land k Fn w \land ⋃ ran k \subseteq dom A) \to \forall y \in w k (y) \subseteq dom A$
154	153	r19.21bi	$⊢ ((Fun A \land k Fn w \land ⋃ ran k \subseteq dom A) \land y \in w) \to k (y) \subseteq dom A$
155		funimass3	$⊢ (Fun A \land k (y) \subseteq dom A) \to (A [k (y)] \subseteq V \leftrightarrow k (y) \subseteq A^{-1} [V])$
156	148 154 155	syl2anc	$⊢ ((Fun A \land k Fn w \land ⋃ ran k \subseteq dom A) \land y \in w) \to (A [k (y)] \subseteq V \leftrightarrow k (y) \subseteq A^{-1} [V])$
157	156	ralbidva	$⊢ (Fun A \land k Fn w \land ⋃ ran k \subseteq dom A) \to (\forall y \in w A [k (y)] \subseteq V \leftrightarrow \forall y \in w k (y) \subseteq A^{-1} [V])$
158		iunss	$⊢ ⋃_{y \in w} A [k (y)] \subseteq V \leftrightarrow \forall y \in w A [k (y)] \subseteq V$
159		iunss	$⊢ ⋃_{y \in w} k (y) \subseteq A^{-1} [V] \leftrightarrow \forall y \in w k (y) \subseteq A^{-1} [V]$
160	157 158 159	3bitr4g	$⊢ (Fun A \land k Fn w \land ⋃ ran k \subseteq dom A) \to (⋃_{y \in w} A [k (y)] \subseteq V \leftrightarrow ⋃_{y \in w} k (y) \subseteq A^{-1} [V])$
161	144 145 147 160	syl3anc	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to (⋃_{y \in w} A [k (y)] \subseteq V \leftrightarrow ⋃_{y \in w} k (y) \subseteq A^{-1} [V])$
162	143 161	mpbird	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to ⋃_{y \in w} A [k (y)] \subseteq V$
163	142 162	eqsstrrd	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to A [⋃ ran k] \subseteq V$
164	138 139 163	elrabd	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to A \in \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\}$
165		imaeq1	$⊢ b = B \to b [K] = B [K]$
166	165	sseq1d	$⊢ b = B \to (b [K] \subseteq ⋃_{y \in w} int (S) (k (y)) \leftrightarrow B [K] \subseteq ⋃_{y \in w} int (S) (k (y)))$
167	7	ad2antrr	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to B \in (R Cn S)$
168		simprl	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to B [K] = ⋃ w$
169		uniiun	$⊢ ⋃ w = ⋃_{y \in w} y$
170	168 169	eqtrdi	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to B [K] = ⋃_{y \in w} y$
171		simpl	$⊢ (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp) \to y \subseteq int (S) (k (y))$
172	171	ralimi	$⊢ \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp) \to \forall y \in w y \subseteq int (S) (k (y))$
173		ss2iun	$⊢ \forall y \in w y \subseteq int (S) (k (y)) \to ⋃_{y \in w} y \subseteq ⋃_{y \in w} int (S) (k (y))$
174	114 172 173	3syl	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to ⋃_{y \in w} y \subseteq ⋃_{y \in w} int (S) (k (y))$
175	170 174	eqsstrd	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to B [K] \subseteq ⋃_{y \in w} int (S) (k (y))$
176	166 167 175	elrabd	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to B \in \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\}$
177	164 176	opelxpd	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to ⟨A, B⟩ \in (\{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\})$
178		imaeq1	$⊢ a = u \to a [⋃ ran k] = u [⋃ ran k]$
179	178	sseq1d	$⊢ a = u \to (a [⋃ ran k] \subseteq V \leftrightarrow u [⋃ ran k] \subseteq V)$
180	179	elrab	$⊢ u \in \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \leftrightarrow (u \in (S Cn T) \land u [⋃ ran k] \subseteq V)$
181		imaeq1	$⊢ b = v \to b [K] = v [K]$
182	181	sseq1d	$⊢ b = v \to (b [K] \subseteq ⋃_{y \in w} int (S) (k (y)) \leftrightarrow v [K] \subseteq ⋃_{y \in w} int (S) (k (y)))$
183	182	elrab	$⊢ v \in \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \leftrightarrow (v \in (R Cn S) \land v [K] \subseteq ⋃_{y \in w} int (S) (k (y)))$
184	180 183	anbi12i	$⊢ (u \in \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \land v \in \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\}) \leftrightarrow ((u \in (S Cn T) \land u [⋃ ran k] \subseteq V) \land (v \in (R Cn S) \land v [K] \subseteq ⋃_{y \in w} int (S) (k (y))))$
185		simprll	$⊢ (((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \land ((u \in (S Cn T) \land u [⋃ ran k] \subseteq V) \land (v \in (R Cn S) \land v [K] \subseteq ⋃_{y \in w} int (S) (k (y))))) \to u \in (S Cn T)$
186		simprrl	$⊢ (((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \land ((u \in (S Cn T) \land u [⋃ ran k] \subseteq V) \land (v \in (R Cn S) \land v [K] \subseteq ⋃_{y \in w} int (S) (k (y))))) \to v \in (R Cn S)$
187		coeq1	$⊢ f = u \to f \circ g = u \circ g$
188		coeq2	$⊢ g = v \to u \circ g = u \circ v$
189		vex	$⊢ u \in V$
190		vex	$⊢ v \in V$
191	189 190	coex	$⊢ u \circ v \in V$
192	187 188 1 191	ovmpo	$⊢ (u \in (S Cn T) \land v \in (R Cn S)) \to u F v = u \circ v$
193	185 186 192	syl2anc	$⊢ (((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \land ((u \in (S Cn T) \land u [⋃ ran k] \subseteq V) \land (v \in (R Cn S) \land v [K] \subseteq ⋃_{y \in w} int (S) (k (y))))) \to u F v = u \circ v$
194		imaeq1	$⊢ h = u \circ v \to h [K] = (u \circ v) [K]$
195	194	sseq1d	$⊢ h = u \circ v \to (h [K] \subseteq V \leftrightarrow (u \circ v) [K] \subseteq V)$
196		cnco	$⊢ (v \in (R Cn S) \land u \in (S Cn T)) \to u \circ v \in (R Cn T)$
197	186 185 196	syl2anc	$⊢ (((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \land ((u \in (S Cn T) \land u [⋃ ran k] \subseteq V) \land (v \in (R Cn S) \land v [K] \subseteq ⋃_{y \in w} int (S) (k (y))))) \to u \circ v \in (R Cn T)$
198		imaco	$⊢ (u \circ v) [K] = u [v [K]]$
199		simprrr	$⊢ (((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \land ((u \in (S Cn T) \land u [⋃ ran k] \subseteq V) \land (v \in (R Cn S) \land v [K] \subseteq ⋃_{y \in w} int (S) (k (y))))) \to v [K] \subseteq ⋃_{y \in w} int (S) (k (y))$
200	17	ntrss2	$⊢ (S \in Top \land k (y) \subseteq ⋃ S) \to int (S) (k (y)) \subseteq k (y)$
201	200	ex	$⊢ S \in Top \to (k (y) \subseteq ⋃ S \to int (S) (k (y)) \subseteq k (y))$
202	201	ralimdv	$⊢ S \in Top \to (\forall y \in w k (y) \subseteq ⋃ S \to \forall y \in w int (S) (k (y)) \subseteq k (y))$
203	90 127 202	sylc	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to \forall y \in w int (S) (k (y)) \subseteq k (y)$
204		ss2iun	$⊢ \forall y \in w int (S) (k (y)) \subseteq k (y) \to ⋃_{y \in w} int (S) (k (y)) \subseteq ⋃_{y \in w} k (y)$
205	203 204	syl	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to ⋃_{y \in w} int (S) (k (y)) \subseteq ⋃_{y \in w} k (y)$
206	205 110	sseqtrd	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to ⋃_{y \in w} int (S) (k (y)) \subseteq ⋃ ran k$
207	206	adantr	$⊢ (((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \land ((u \in (S Cn T) \land u [⋃ ran k] \subseteq V) \land (v \in (R Cn S) \land v [K] \subseteq ⋃_{y \in w} int (S) (k (y))))) \to ⋃_{y \in w} int (S) (k (y)) \subseteq ⋃ ran k$
208	199 207	sstrd	$⊢ (((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \land ((u \in (S Cn T) \land u [⋃ ran k] \subseteq V) \land (v \in (R Cn S) \land v [K] \subseteq ⋃_{y \in w} int (S) (k (y))))) \to v [K] \subseteq ⋃ ran k$
209		imass2	$⊢ v [K] \subseteq ⋃ ran k \to u [v [K]] \subseteq u [⋃ ran k]$
210	208 209	syl	$⊢ (((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \land ((u \in (S Cn T) \land u [⋃ ran k] \subseteq V) \land (v \in (R Cn S) \land v [K] \subseteq ⋃_{y \in w} int (S) (k (y))))) \to u [v [K]] \subseteq u [⋃ ran k]$
211		simprlr	$⊢ (((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \land ((u \in (S Cn T) \land u [⋃ ran k] \subseteq V) \land (v \in (R Cn S) \land v [K] \subseteq ⋃_{y \in w} int (S) (k (y))))) \to u [⋃ ran k] \subseteq V$
212	210 211	sstrd	$⊢ (((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \land ((u \in (S Cn T) \land u [⋃ ran k] \subseteq V) \land (v \in (R Cn S) \land v [K] \subseteq ⋃_{y \in w} int (S) (k (y))))) \to u [v [K]] \subseteq V$
213	198 212	eqsstrid	$⊢ (((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \land ((u \in (S Cn T) \land u [⋃ ran k] \subseteq V) \land (v \in (R Cn S) \land v [K] \subseteq ⋃_{y \in w} int (S) (k (y))))) \to (u \circ v) [K] \subseteq V$
214	195 197 213	elrabd	$⊢ (((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \land ((u \in (S Cn T) \land u [⋃ ran k] \subseteq V) \land (v \in (R Cn S) \land v [K] \subseteq ⋃_{y \in w} int (S) (k (y))))) \to u \circ v \in \{h \in (R Cn T) \| h [K] \subseteq V\}$
215	193 214	eqeltrd	$⊢ (((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \land ((u \in (S Cn T) \land u [⋃ ran k] \subseteq V) \land (v \in (R Cn S) \land v [K] \subseteq ⋃_{y \in w} int (S) (k (y))))) \to u F v \in \{h \in (R Cn T) \| h [K] \subseteq V\}$
216	184 215	sylan2b	$⊢ (((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \land (u \in \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \land v \in \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\})) \to u F v \in \{h \in (R Cn T) \| h [K] \subseteq V\}$
217	216	ralrimivva	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to \forall u \in \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \forall v \in \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} u F v \in \{h \in (R Cn T) \| h [K] \subseteq V\}$
218	1	mpofun	$⊢ Fun F$
219		ssrab2	$⊢ \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \subseteq S Cn T$
220		ssrab2	$⊢ \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \subseteq R Cn S$
221		xpss12	$⊢ (\{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \subseteq S Cn T \land \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \subseteq R Cn S) \to \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \subseteq (S Cn T) \times (R Cn S)$
222	219 220 221	mp2an	$⊢ \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \subseteq (S Cn T) \times (R Cn S)$
223		vex	$⊢ f \in V$
224		vex	$⊢ g \in V$
225	223 224	coex	$⊢ f \circ g \in V$
226	1 225	dmmpo	$⊢ dom F = (S Cn T) \times (R Cn S)$
227	222 226	sseqtrri	$⊢ \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \subseteq dom F$
228		funimassov	$⊢ (Fun F \land \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \subseteq dom F) \to (F [\{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\}] \subseteq \{h \in (R Cn T) \| h [K] \subseteq V\} \leftrightarrow \forall u \in \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \forall v \in \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} u F v \in \{h \in (R Cn T) \| h [K] \subseteq V\})$
229	218 227 228	mp2an	$⊢ F [\{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\}] \subseteq \{h \in (R Cn T) \| h [K] \subseteq V\} \leftrightarrow \forall u \in \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \forall v \in \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} u F v \in \{h \in (R Cn T) \| h [K] \subseteq V\}$
230	217 229	sylibr	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to F [\{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\}] \subseteq \{h \in (R Cn T) \| h [K] \subseteq V\}$
231		funimass3	$⊢ (Fun F \land \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \subseteq dom F) \to (F [\{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\}] \subseteq \{h \in (R Cn T) \| h [K] \subseteq V\} \leftrightarrow \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \subseteq F^{-1} [\{h \in (R Cn T) \| h [K] \subseteq V\}])$
232	218 227 231	mp2an	$⊢ F [\{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\}] \subseteq \{h \in (R Cn T) \| h [K] \subseteq V\} \leftrightarrow \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \subseteq F^{-1} [\{h \in (R Cn T) \| h [K] \subseteq V\}]$
233	230 232	sylib	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \subseteq F^{-1} [\{h \in (R Cn T) \| h [K] \subseteq V\}]$
234		eleq2	$⊢ z = \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \to (⟨A, B⟩ \in z \leftrightarrow ⟨A, B⟩ \in (\{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\}))$
235		sseq1	$⊢ z = \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \to (z \subseteq F^{-1} [\{h \in (R Cn T) \| h [K] \subseteq V\}] \leftrightarrow \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \subseteq F^{-1} [\{h \in (R Cn T) \| h [K] \subseteq V\}])$
236	234 235	anbi12d	$⊢ z = \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \to ((⟨A, B⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [K] \subseteq V\}]) \leftrightarrow (⟨A, B⟩ \in (\{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\}) \land \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \subseteq F^{-1} [\{h \in (R Cn T) \| h [K] \subseteq V\}]))$
237	236	rspcev	$⊢ (\{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) \land (⟨A, B⟩ \in (\{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\}) \land \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \times \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \subseteq F^{-1} [\{h \in (R Cn T) \| h [K] \subseteq V\}])) \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (⟨A, B⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [K] \subseteq V\}])$
238	136 177 233 237	syl12anc	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land (B [K] = ⋃ w \land (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)))) \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (⟨A, B⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [K] \subseteq V\}])$
239	238	expr	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land B [K] = ⋃ w) \to ((k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)) \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (⟨A, B⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [K] \subseteq V\}]))$
240	239	exlimdv	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land B [K] = ⋃ w) \to (\exists k (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)) \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (⟨A, B⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [K] \subseteq V\}]))$
241	89 240	syldan	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land ⋃ (S ↾_{𝑡} B [K]) = ⋃ w) \to (\exists k (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp)) \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (⟨A, B⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [K] \subseteq V\}]))$
242	241	expimpd	$⊢ (φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \to ((⋃ (S ↾_{𝑡} B [K]) = ⋃ w \land \exists k (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp))) \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (⟨A, B⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [K] \subseteq V\}]))$
243	242	rexlimdva	$⊢ φ \to (\exists w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin) (⋃ (S ↾_{𝑡} B [K]) = ⋃ w \land \exists k (k : w ⟶ 𝒫 A^{-1} [V] \land \forall y \in w (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp))) \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (⟨A, B⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [K] \subseteq V\}]))$
244	86 243	mpd	$⊢ φ \to \exists z \in ((T^_{ko} S) \times_{t} (S^_{ko} R)) (⟨A, B⟩ \in z \land z \subseteq F^{-1} [\{h \in (R Cn T) \| h [K] \subseteq V\}])$

Metamath Proof Explorer

Theorem xkococnlem

Proof