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] \exists u \in S (x \in u \land u \subseteq s \land S ↾_{𝑡} s \in Comp))$
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	77	raleqdv	$⊢ φ \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)) \leftrightarrow \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	75 78	mpbid	$⊢ φ \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))$
80		eqid	$⊢ ⋃ (S ↾_{𝑡} B [K]) = ⋃ (S ↾_{𝑡} B [K])$
81		fveq2	$⊢ s = k (y) \to int (S) (s) = int (S) (k (y))$
82	81	sseq2d	$⊢ s = k (y) \to (y \subseteq int (S) (s) \leftrightarrow y \subseteq int (S) (k (y)))$
83		oveq2	$⊢ s = k (y) \to S ↾_{𝑡} s = S ↾_{𝑡} k (y)$
84	83	eleq1d	$⊢ s = k (y) \to (S ↾_{𝑡} s \in Comp \leftrightarrow S ↾_{𝑡} k (y) \in Comp)$
85	82 84	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))$
86	80 85	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)))$
87	10 79 86	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)))$
88	77	adantr	$⊢ (φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \to B [K] = ⋃ (S ↾_{𝑡} B [K])$
89	88	eqeq1d	$⊢ (φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \to (B [K] = ⋃ w \leftrightarrow ⋃ (S ↾_{𝑡} B [K]) = ⋃ w)$
90	89	biimpar	$⊢ ((φ \land w \in (𝒫 (S ↾_{𝑡} B [K]) \cap Fin)) \land ⋃ (S ↾_{𝑡} B [K]) = ⋃ w) \to B [K] = ⋃ w$
91	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$
92		cntop2	$⊢ A \in (S Cn T) \to T \in Top$
93	6 92	syl	$⊢ φ \to T \in Top$
94	93	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$
95		xkotop	$⊢ (S \in Top \land T \in Top) \to T^_{ko} S \in Top$
96	91 94 95	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$
97		cntop1	$⊢ B \in (R Cn S) \to R \in Top$
98	7 97	syl	$⊢ φ \to R \in Top$
99	98	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$
100		xkotop	$⊢ (R \in Top \land S \in Top) \to S^_{ko} R \in Top$
101	99 91 100	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$
102		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]$
103	102	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]$
104		sspwuni	$⊢ ran k \subseteq 𝒫 A^{-1} [V] \leftrightarrow ⋃ ran k \subseteq A^{-1} [V]$
105	103 104	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]$
106	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$
107	106 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$
108	105 107	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$
109		ffn	$⊢ k : w ⟶ 𝒫 A^{-1} [V] \to k Fn w$
110		fniunfv	$⊢ k Fn w \to ⋃_{y \in w} k (y) = ⋃ ran k$
111	102 109 110	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$
112	111	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$
113		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)$
114	113	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$
115		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)$
116		simpr	$⊢ (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp) \to S ↾_{𝑡} k (y) \in Comp$
117	116	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$
118	115 117	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$
119	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$
120	91 114 118 119	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$
121	112 120	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$
122	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$
123	17 91 94 108 121 122	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)$
124	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$
125	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$
126	111 108	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$
127		iunss	$⊢ ⋃_{y \in w} k (y) \subseteq ⋃ S \leftrightarrow \forall y \in w k (y) \subseteq ⋃ S$
128	126 127	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$
129	17	ntropn	$⊢ (S \in Top \land k (y) \subseteq ⋃ S) \to int (S) (k (y)) \in S$
130	129	ex	$⊢ S \in Top \to (k (y) \subseteq ⋃ S \to int (S) (k (y)) \in S)$
131	130	ralimdv	$⊢ S \in Top \to (\forall y \in w k (y) \subseteq ⋃ S \to \forall y \in w int (S) (k (y)) \in S)$
132	91 128 131	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$
133		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$
134	91 132 133	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$
135	23 99 91 124 125 134	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)$
136		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))$
137	96 101 123 135 136	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))$
138		imaeq1	$⊢ a = A \to a [⋃ ran k] = A [⋃ ran k]$
139	138	sseq1d	$⊢ a = A \to (a [⋃ ran k] \subseteq V \leftrightarrow A [⋃ ran k] \subseteq V)$
140	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)$
141		imaiun	$⊢ A [⋃_{y \in w} k (y)] = ⋃_{y \in w} A [k (y)]$
142	111	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]$
143	141 142	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]$
144	111 105	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]$
145	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$
146	102 109	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$
147	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$
148	108 147	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$
149		simpl1	$⊢ ((Fun A \land k Fn w \land ⋃ ran k \subseteq dom A) \land y \in w) \to Fun A$
150	110	3ad2ant2	$⊢ (Fun A \land k Fn w \land ⋃ ran k \subseteq dom A) \to ⋃_{y \in w} k (y) = ⋃ ran k$
151		simp3	$⊢ (Fun A \land k Fn w \land ⋃ ran k \subseteq dom A) \to ⋃ ran k \subseteq dom A$
152	150 151	eqsstrd	$⊢ (Fun A \land k Fn w \land ⋃ ran k \subseteq dom A) \to ⋃_{y \in w} k (y) \subseteq dom A$
153		iunss	$⊢ ⋃_{y \in w} k (y) \subseteq dom A \leftrightarrow \forall y \in w k (y) \subseteq dom A$
154	152 153	sylib	$⊢ (Fun A \land k Fn w \land ⋃ ran k \subseteq dom A) \to \forall y \in w k (y) \subseteq dom A$
155	154	r19.21bi	$⊢ ((Fun A \land k Fn w \land ⋃ ran k \subseteq dom A) \land y \in w) \to k (y) \subseteq dom A$
156		funimass3	$⊢ (Fun A \land k (y) \subseteq dom A) \to (A [k (y)] \subseteq V \leftrightarrow k (y) \subseteq A^{-1} [V])$
157	149 155 156	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])$
158	157	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])$
159		iunss	$⊢ ⋃_{y \in w} A [k (y)] \subseteq V \leftrightarrow \forall y \in w A [k (y)] \subseteq V$
160		iunss	$⊢ ⋃_{y \in w} k (y) \subseteq A^{-1} [V] \leftrightarrow \forall y \in w k (y) \subseteq A^{-1} [V]$
161	158 159 160	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])$
162	145 146 148 161	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])$
163	144 162	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$
164	143 163	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$
165	139 140 164	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\}$
166		imaeq1	$⊢ b = B \to b [K] = B [K]$
167	166	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)))$
168	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)$
169		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$
170		uniiun	$⊢ ⋃ w = ⋃_{y \in w} y$
171	169 170	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$
172		simpl	$⊢ (y \subseteq int (S) (k (y)) \land S ↾_{𝑡} k (y) \in Comp) \to y \subseteq int (S) (k (y))$
173	172	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))$
174		ss2iun	$⊢ \forall y \in w y \subseteq int (S) (k (y)) \to ⋃_{y \in w} y \subseteq ⋃_{y \in w} int (S) (k (y))$
175	115 173 174	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))$
176	171 175	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))$
177	167 168 176	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))\}$
178	165 177	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))\})$
179		imaeq1	$⊢ a = u \to a [⋃ ran k] = u [⋃ ran k]$
180	179	sseq1d	$⊢ a = u \to (a [⋃ ran k] \subseteq V \leftrightarrow u [⋃ ran k] \subseteq V)$
181	180	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)$
182		imaeq1	$⊢ b = v \to b [K] = v [K]$
183	182	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)))$
184	183	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)))$
185	181 184	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))))$
186		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)$
187		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)$
188		coeq1	$⊢ f = u \to f \circ g = u \circ g$
189		coeq2	$⊢ g = v \to u \circ g = u \circ v$
190		vex	$⊢ u \in V$
191		vex	$⊢ v \in V$
192	190 191	coex	$⊢ u \circ v \in V$
193	188 189 1 192	ovmpo	$⊢ (u \in (S Cn T) \land v \in (R Cn S)) \to u F v = u \circ v$
194	186 187 193	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$
195		imaeq1	$⊢ h = u \circ v \to h [K] = (u \circ v) [K]$
196	195	sseq1d	$⊢ h = u \circ v \to (h [K] \subseteq V \leftrightarrow (u \circ v) [K] \subseteq V)$
197		cnco	$⊢ (v \in (R Cn S) \land u \in (S Cn T)) \to u \circ v \in (R Cn T)$
198	187 186 197	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)$
199		imaco	$⊢ (u \circ v) [K] = u [v [K]]$
200		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))$
201	17	ntrss2	$⊢ (S \in Top \land k (y) \subseteq ⋃ S) \to int (S) (k (y)) \subseteq k (y)$
202	201	ex	$⊢ S \in Top \to (k (y) \subseteq ⋃ S \to int (S) (k (y)) \subseteq k (y))$
203	202	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))$
204	91 128 203	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)$
205		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)$
206	204 205	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)$
207	206 111	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$
208	207	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$
209	200 208	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$
210		imass2	$⊢ v [K] \subseteq ⋃ ran k \to u [v [K]] \subseteq u [⋃ ran k]$
211	209 210	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]$
212		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$
213	211 212	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$
214	199 213	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$
215	196 198 214	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\}$
216	194 215	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\}$
217	185 216	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\}$
218	217	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\}$
219	1	mpofun	$⊢ Fun F$
220		ssrab2	$⊢ \{a \in (S Cn T) \| a [⋃ ran k] \subseteq V\} \subseteq S Cn T$
221		ssrab2	$⊢ \{b \in (R Cn S) \| b [K] \subseteq ⋃_{y \in w} int (S) (k (y))\} \subseteq R Cn S$
222		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)$
223	220 221 222	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)$
224		vex	$⊢ f \in V$
225		vex	$⊢ g \in V$
226	224 225	coex	$⊢ f \circ g \in V$
227	1 226	dmmpo	$⊢ dom F = (S Cn T) \times (R Cn S)$
228	223 227	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$
229		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\})$
230	219 228 229	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\}$
231	218 230	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\}$
232		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\}])$
233	219 228 232	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\}]$
234	231 233	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\}]$
235		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))\}))$
236		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\}])$
237	235 236	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\}]))$
238	237	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\}])$
239	137 178 234 238	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\}])$
240	239	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\}]))$
241	240	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\}]))$
242	90 241	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\}]))$
243	242	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\}]))$
244	243	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\}]))$
245	87 244	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