xkococnlem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > xkococnlem		Structured version Visualization version GIF version

Theorem xkococnlem 21462

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.)

**Hypotheses**
Ref	Expression
xkococn.1	⊢ 𝐹 = (𝑓 ∈ (𝑆 Cn 𝑇), 𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝑓 ∘ 𝑔))
xkococn.s	⊢ (𝜑 → 𝑆 ∈ 𝑛-Locally Comp)
xkococn.k	⊢ (𝜑 → 𝐾 ⊆ ∪ 𝑅)
xkococn.c	⊢ (𝜑 → (𝑅 ↾_t 𝐾) ∈ Comp)
xkococn.v	⊢ (𝜑 → 𝑉 ∈ 𝑇)
xkococn.a	⊢ (𝜑 → 𝐴 ∈ (𝑆 Cn 𝑇))
xkococn.b	⊢ (𝜑 → 𝐵 ∈ (𝑅 Cn 𝑆))
xkococn.i	⊢ (𝜑 → ((𝐴 ∘ 𝐵) “ 𝐾) ⊆ 𝑉)

**Assertion**
Ref	Expression
xkococnlem	⊢ (𝜑 → ∃𝑧 ∈ ((𝑇 ^_ko 𝑆) ×_t (𝑆 ^_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))

Distinct variable groups: 𝑧,𝐴 𝑧,𝐵 𝑓,𝑔,ℎ,𝑧,𝑅 𝑆,𝑓,𝑔,𝑧 ℎ,𝐾,𝑧 𝑇,𝑓,𝑔,ℎ,𝑧 𝑧,𝐹 ℎ,𝑉,𝑧 Allowed substitution hints: 𝜑(𝑧,𝑓,𝑔,ℎ) 𝐴(𝑓,𝑔,ℎ) 𝐵(𝑓,𝑔,ℎ) 𝑆(ℎ) 𝐹(𝑓,𝑔,ℎ) 𝐾(𝑓,𝑔) 𝑉(𝑓,𝑔)

Proof of Theorem xkococnlem Dummy variables 𝑘 𝑎 𝑠 𝑢 𝑣 𝑤 𝑥 𝑦 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xkococn.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ (𝑅 Cn 𝑆))
2		xkococn.c	. . . 4 ⊢ (𝜑 → (𝑅 ↾_t 𝐾) ∈ Comp)
3		imacmp 21200	. . . 4 ⊢ ((𝐵 ∈ (𝑅 Cn 𝑆) ∧ (𝑅 ↾_t 𝐾) ∈ Comp) → (𝑆 ↾_t (𝐵 “ 𝐾)) ∈ Comp)
4	1, 2, 3	syl2anc 693	. . 3 ⊢ (𝜑 → (𝑆 ↾_t (𝐵 “ 𝐾)) ∈ Comp)
5		xkococn.s	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ 𝑛-Locally Comp)
6	5	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → 𝑆 ∈ 𝑛-Locally Comp)
7		xkococn.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ (𝑆 Cn 𝑇))
8		xkococn.v	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ 𝑇)
9		cnima 21069	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑆 Cn 𝑇) ∧ 𝑉 ∈ 𝑇) → (^◡𝐴 “ 𝑉) ∈ 𝑆)
10	7, 8, 9	syl2anc 693	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐴 “ 𝑉) ∈ 𝑆)
11	10	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → (^◡𝐴 “ 𝑉) ∈ 𝑆)
12		imaco 5640	. . . . . . . . . . 11 ⊢ ((𝐴 ∘ 𝐵) “ 𝐾) = (𝐴 “ (𝐵 “ 𝐾))
13		xkococn.i	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 ∘ 𝐵) “ 𝐾) ⊆ 𝑉)
14	12, 13	syl5eqssr 3650	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉)
15		eqid 2622	. . . . . . . . . . . . 13 ⊢ ∪ 𝑆 = ∪ 𝑆
16		eqid 2622	. . . . . . . . . . . . 13 ⊢ ∪ 𝑇 = ∪ 𝑇
17	15, 16	cnf 21050	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (𝑆 Cn 𝑇) → 𝐴:∪ 𝑆⟶∪ 𝑇)
18		ffun 6048	. . . . . . . . . . . 12 ⊢ (𝐴:∪ 𝑆⟶∪ 𝑇 → Fun 𝐴)
19	7, 17, 18	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → Fun 𝐴)
20		imassrn 5477	. . . . . . . . . . . . 13 ⊢ (𝐵 “ 𝐾) ⊆ ran 𝐵
21		eqid 2622	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑅 = ∪ 𝑅
22	21, 15	cnf 21050	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → 𝐵:∪ 𝑅⟶∪ 𝑆)
23		frn 6053	. . . . . . . . . . . . . 14 ⊢ (𝐵:∪ 𝑅⟶∪ 𝑆 → ran 𝐵 ⊆ ∪ 𝑆)
24	1, 22, 23	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐵 ⊆ ∪ 𝑆)
25	20, 24	syl5ss 3614	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ ∪ 𝑆)
26		fdm 6051	. . . . . . . . . . . . 13 ⊢ (𝐴:∪ 𝑆⟶∪ 𝑇 → dom 𝐴 = ∪ 𝑆)
27	7, 17, 26	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → dom 𝐴 = ∪ 𝑆)
28	25, 27	sseqtr4d 3642	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ dom 𝐴)
29		funimass3 6333	. . . . . . . . . . 11 ⊢ ((Fun 𝐴 ∧ (𝐵 “ 𝐾) ⊆ dom 𝐴) → ((𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉 ↔ (𝐵 “ 𝐾) ⊆ (^◡𝐴 “ 𝑉)))
30	19, 28, 29	syl2anc 693	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉 ↔ (𝐵 “ 𝐾) ⊆ (^◡𝐴 “ 𝑉)))
31	14, 30	mpbid 222	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ (^◡𝐴 “ 𝑉))
32	31	sselda 3603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → 𝑥 ∈ (^◡𝐴 “ 𝑉))
33		nlly2i 21279	. . . . . . . 8 ⊢ ((𝑆 ∈ 𝑛-Locally Comp ∧ (^◡𝐴 “ 𝑉) ∈ 𝑆 ∧ 𝑥 ∈ (^◡𝐴 “ 𝑉)) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))
34	6, 11, 32, 33	syl3anc 1326	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))
35		nllytop 21276	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ 𝑛-Locally Comp → 𝑆 ∈ Top)
36	5, 35	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ Top)
37	36	ad3antrrr 766	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
38		imaexg 7103	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → (𝐵 “ 𝐾) ∈ V)
39	1, 38	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 “ 𝐾) ∈ V)
40	39	ad3antrrr 766	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝐵 “ 𝐾) ∈ V)
41		simprl 794	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑢 ∈ 𝑆)
42		elrestr 16089	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Top ∧ (𝐵 “ 𝐾) ∈ V ∧ 𝑢 ∈ 𝑆) → (𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾_t (𝐵 “ 𝐾)))
43	37, 40, 41, 42	syl3anc 1326	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾_t (𝐵 “ 𝐾)))
44		simprr1 1109	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑥 ∈ 𝑢)
45		simpllr 799	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝐵 “ 𝐾))
46	44, 45	elind 3798	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)))
47		inss1 3833	. . . . . . . . . . . 12 ⊢ (𝑢 ∩ (𝐵 “ 𝐾)) ⊆ 𝑢
48		elpwi 4168	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉) → 𝑠 ⊆ (^◡𝐴 “ 𝑉))
49	48	ad2antlr 763	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑠 ⊆ (^◡𝐴 “ 𝑉))
50		elssuni 4467	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐴 “ 𝑉) ∈ 𝑆 → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
51	10, 50	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
52	51	ad3antrrr 766	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
53	49, 52	sstrd 3613	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑠 ⊆ ∪ 𝑆)
54		simprr2 1110	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑢 ⊆ 𝑠)
55	15	ssntr 20862	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ Top ∧ 𝑠 ⊆ ∪ 𝑆) ∧ (𝑢 ∈ 𝑆 ∧ 𝑢 ⊆ 𝑠)) → 𝑢 ⊆ ((int‘𝑆)‘𝑠))
56	37, 53, 41, 54, 55	syl22anc 1327	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑢 ⊆ ((int‘𝑆)‘𝑠))
57	47, 56	syl5ss 3614	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠))
58		simprr3 1111	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝑆 ↾_t 𝑠) ∈ Comp)
59	57, 58	jca 554	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))
60		eleq2 2690	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾))))
61		sseq1 3626	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → (𝑦 ⊆ ((int‘𝑆)‘𝑠) ↔ (𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠)))
62	61	anbi1d 741	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp) ↔ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
63	60, 62	anbi12d 747	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → ((𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ (𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)) ∧ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))))
64	63	rspcev 3309	. . . . . . . . . 10 ⊢ (((𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾_t (𝐵 “ 𝐾)) ∧ (𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)) ∧ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
65	43, 46, 59, 64	syl12anc 1324	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
66	65	rexlimdvaa 3032	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) → (∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))))
67	66	reximdva 3017	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))))
68	34, 67	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
69		rexcom 3099	. . . . . . 7 ⊢ (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
70		r19.42v 3092	. . . . . . . 8 ⊢ (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ (𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
71	70	rexbii 3041	. . . . . . 7 ⊢ (∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
72	69, 71	bitri 264	. . . . . 6 ⊢ (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
73	68, 72	sylib 208	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
74	73	ralrimiva 2966	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ (𝐵 “ 𝐾)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
75	15	restuni 20966	. . . . . 6 ⊢ ((𝑆 ∈ Top ∧ (𝐵 “ 𝐾) ⊆ ∪ 𝑆) → (𝐵 “ 𝐾) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾)))
76	36, 25, 75	syl2anc 693	. . . . 5 ⊢ (𝜑 → (𝐵 “ 𝐾) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾)))
77	76	raleqdv 3144	. . . 4 ⊢ (𝜑 → (∀𝑥 ∈ (𝐵 “ 𝐾)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ ∀𝑥 ∈ ∪ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))))
78	74, 77	mpbid 222	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ∪ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
79		eqid 2622	. . . 4 ⊢ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾))
80		fveq2 6191	. . . . . 6 ⊢ (𝑠 = (𝑘‘𝑦) → ((int‘𝑆)‘𝑠) = ((int‘𝑆)‘(𝑘‘𝑦)))
81	80	sseq2d 3633	. . . . 5 ⊢ (𝑠 = (𝑘‘𝑦) → (𝑦 ⊆ ((int‘𝑆)‘𝑠) ↔ 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦))))
82		oveq2 6658	. . . . . 6 ⊢ (𝑠 = (𝑘‘𝑦) → (𝑆 ↾_t 𝑠) = (𝑆 ↾_t (𝑘‘𝑦)))
83	82	eleq1d 2686	. . . . 5 ⊢ (𝑠 = (𝑘‘𝑦) → ((𝑆 ↾_t 𝑠) ∈ Comp ↔ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))
84	81, 83	anbi12d 747	. . . 4 ⊢ (𝑠 = (𝑘‘𝑦) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp) ↔ (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))
85	79, 84	cmpcovf 21194	. . 3 ⊢ (((𝑆 ↾_t (𝐵 “ 𝐾)) ∈ Comp ∧ ∀𝑥 ∈ ∪ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ∃𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)(∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))))
86	4, 78, 85	syl2anc 693	. 2 ⊢ (𝜑 → ∃𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)(∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))))
87	76	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) → (𝐵 “ 𝐾) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾)))
88	87	eqeq1d 2624	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) → ((𝐵 “ 𝐾) = ∪ 𝑤 ↔ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤))
89	88	biimpar 502	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤) → (𝐵 “ 𝐾) = ∪ 𝑤)
90	36	ad2antrr 762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑆 ∈ Top)
91		cntop2 21045	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (𝑆 Cn 𝑇) → 𝑇 ∈ Top)
92	7, 91	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ Top)
93	92	ad2antrr 762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑇 ∈ Top)
94		xkotop 21391	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ^_ko 𝑆) ∈ Top)
95	90, 93, 94	syl2anc 693	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑇 ^_ko 𝑆) ∈ Top)
96		cntop1 21044	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → 𝑅 ∈ Top)
97	1, 96	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ Top)
98	97	ad2antrr 762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑅 ∈ Top)
99		xkotop 21391	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ^_ko 𝑅) ∈ Top)
100	98, 90, 99	syl2anc 693	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ^_ko 𝑅) ∈ Top)
101		simprrl 804	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉))
102		frn 6053	. . . . . . . . . . . . 13 ⊢ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) → ran 𝑘 ⊆ 𝒫 (^◡𝐴 “ 𝑉))
103	101, 102	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ran 𝑘 ⊆ 𝒫 (^◡𝐴 “ 𝑉))
104		sspwuni 4611	. . . . . . . . . . . 12 ⊢ (ran 𝑘 ⊆ 𝒫 (^◡𝐴 “ 𝑉) ↔ ∪ ran 𝑘 ⊆ (^◡𝐴 “ 𝑉))
105	103, 104	sylib 208	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ (^◡𝐴 “ 𝑉))
106	10	ad2antrr 762	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (^◡𝐴 “ 𝑉) ∈ 𝑆)
107	106, 50	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
108	105, 107	sstrd 3613	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ ∪ 𝑆)
109		ffn 6045	. . . . . . . . . . . . 13 ⊢ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) → 𝑘 Fn 𝑤)
110		fniunfv 6505	. . . . . . . . . . . . 13 ⊢ (𝑘 Fn 𝑤 → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘)
111	101, 109, 110	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘)
112	111	oveq2d 6666	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾_t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = (𝑆 ↾_t ∪ ran 𝑘))
113		inss2 3834	. . . . . . . . . . . . 13 ⊢ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin) ⊆ Fin
114		simplr 792	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin))
115	113, 114	sseldi 3601	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑤 ∈ Fin)
116		simprrr 805	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))
117		simpr 477	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)
118	117	ralimi 2952	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → ∀𝑦 ∈ 𝑤 (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)
119	116, 118	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)
120	15	fiuncmp 21207	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Top ∧ 𝑤 ∈ Fin ∧ ∀𝑦 ∈ 𝑤 (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → (𝑆 ↾_t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) ∈ Comp)
121	90, 115, 119, 120	syl3anc 1326	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾_t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) ∈ Comp)
122	112, 121	eqeltrrd 2702	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾_t ∪ ran 𝑘) ∈ Comp)
123	8	ad2antrr 762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑉 ∈ 𝑇)
124	15, 90, 93, 108, 122, 123	xkoopn 21392	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∈ (𝑇 ^_ko 𝑆))
125		xkococn.k	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ⊆ ∪ 𝑅)
126	125	ad2antrr 762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐾 ⊆ ∪ 𝑅)
127	2	ad2antrr 762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑅 ↾_t 𝐾) ∈ Comp)
128	111, 108	eqsstrd 3639	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆)
129		iunss 4561	. . . . . . . . . . . . 13 ⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆)
130	128, 129	sylib 208	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆)
131	15	ntropn 20853	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ Top ∧ (𝑘‘𝑦) ⊆ ∪ 𝑆) → ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
132	131	ex 450	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Top → ((𝑘‘𝑦) ⊆ ∪ 𝑆 → ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆))
133	132	ralimdv 2963	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ Top → (∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆))
134	90, 130, 133	sylc 65	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
135		iunopn 20703	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Top ∧ ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
136	90, 134, 135	syl2anc 693	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
137	21, 98, 90, 126, 127, 136	xkoopn 21392	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ∈ (𝑆 ^_ko 𝑅))
138		txopn 21405	. . . . . . . . 9 ⊢ ((((𝑇 ^_ko 𝑆) ∈ Top ∧ (𝑆 ^_ko 𝑅) ∈ Top) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∈ (𝑇 ^_ko 𝑆) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ∈ (𝑆 ^_ko 𝑅))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∈ ((𝑇 ^_ko 𝑆) ×_t (𝑆 ^_ko 𝑅)))
139	95, 100, 124, 137, 138	syl22anc 1327	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∈ ((𝑇 ^_ko 𝑆) ×_t (𝑆 ^_ko 𝑅)))
140	7	ad2antrr 762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐴 ∈ (𝑆 Cn 𝑇))
141		imaiun 6503	. . . . . . . . . . . 12 ⊢ (𝐴 “ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦))
142	111	imaeq2d 5466	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐴 “ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = (𝐴 “ ∪ ran 𝑘))
143	141, 142	syl5eqr 2670	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) = (𝐴 “ ∪ ran 𝑘))
144	111, 105	eqsstrd 3639	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉))
145	19	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → Fun 𝐴)
146	101, 109	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑘 Fn 𝑤)
147	27	ad2antrr 762	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → dom 𝐴 = ∪ 𝑆)
148	108, 147	sseqtr4d 3642	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ dom 𝐴)
149		simpl1 1064	. . . . . . . . . . . . . . . 16 ⊢ (((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → Fun 𝐴)
150	110	3ad2ant2 1083	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘)
151		simp3 1063	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪ ran 𝑘 ⊆ dom 𝐴)
152	150, 151	eqsstrd 3639	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴)
153		iunss 4561	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴)
154	152, 153	sylib 208	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴)
155	154	r19.21bi 2932	. . . . . . . . . . . . . . . 16 ⊢ (((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → (𝑘‘𝑦) ⊆ dom 𝐴)
156		funimass3 6333	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐴 ∧ (𝑘‘𝑦) ⊆ dom 𝐴) → ((𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
157	149, 155, 156	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → ((𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
158	157	ralbidva 2985	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → (∀𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
159		iunss 4561	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∀𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉)
160		iunss 4561	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉) ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉))
161	158, 159, 160	3bitr4g 303	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
162	145, 146, 148, 161	syl3anc 1326	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
163	144, 162	mpbird 247	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉)
164	143, 163	eqsstr3d 3640	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐴 “ ∪ ran 𝑘) ⊆ 𝑉)
165		imaeq1 5461	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝐴 → (𝑎 “ ∪ ran 𝑘) = (𝐴 “ ∪ ran 𝑘))
166	165	sseq1d 3632	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → ((𝑎 “ ∪ ran 𝑘) ⊆ 𝑉 ↔ (𝐴 “ ∪ ran 𝑘) ⊆ 𝑉))
167	166	elrab 3363	. . . . . . . . . 10 ⊢ (𝐴 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ↔ (𝐴 ∈ (𝑆 Cn 𝑇) ∧ (𝐴 “ ∪ ran 𝑘) ⊆ 𝑉))
168	140, 164, 167	sylanbrc 698	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐴 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉})
169	1	ad2antrr 762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐵 ∈ (𝑅 Cn 𝑆))
170		simprl 794	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) = ∪ 𝑤)
171		uniiun 4573	. . . . . . . . . . . 12 ⊢ ∪ 𝑤 = ∪ 𝑦 ∈ 𝑤 𝑦
172	170, 171	syl6eq 2672	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) = ∪ 𝑦 ∈ 𝑤 𝑦)
173		simpl 473	. . . . . . . . . . . . 13 ⊢ ((𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)))
174	173	ralimi 2952	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → ∀𝑦 ∈ 𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)))
175		ss2iun 4536	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) → ∪ 𝑦 ∈ 𝑤 𝑦 ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
176	116, 174, 175	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 𝑦 ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
177	172, 176	eqsstrd 3639	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
178		imaeq1 5461	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝐵 → (𝑏 “ 𝐾) = (𝐵 “ 𝐾))
179	178	sseq1d 3632	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → ((𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ↔ (𝐵 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))
180	179	elrab 3363	. . . . . . . . . 10 ⊢ (𝐵 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ↔ (𝐵 ∈ (𝑅 Cn 𝑆) ∧ (𝐵 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))
181	169, 177, 180	sylanbrc 698	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐵 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})
182		opelxpi 5148	. . . . . . . . 9 ⊢ ((𝐴 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∧ 𝐵 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}))
183	168, 181, 182	syl2anc 693	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}))
184		imaeq1 5461	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑢 → (𝑎 “ ∪ ran 𝑘) = (𝑢 “ ∪ ran 𝑘))
185	184	sseq1d 3632	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑢 → ((𝑎 “ ∪ ran 𝑘) ⊆ 𝑉 ↔ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉))
186	185	elrab 3363	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ↔ (𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉))
187		imaeq1 5461	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑣 → (𝑏 “ 𝐾) = (𝑣 “ 𝐾))
188	187	sseq1d 3632	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑣 → ((𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ↔ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))
189	188	elrab 3363	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ↔ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))
190	186, 189	anbi12i 733	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ↔ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))))
191		simprll 802	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → 𝑢 ∈ (𝑆 Cn 𝑇))
192		simprrl 804	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → 𝑣 ∈ (𝑅 Cn 𝑆))
193		coeq1 5279	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑢 → (𝑓 ∘ 𝑔) = (𝑢 ∘ 𝑔))
194		coeq2 5280	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑣 → (𝑢 ∘ 𝑔) = (𝑢 ∘ 𝑣))
195		xkococn.1	. . . . . . . . . . . . . . 15 ⊢ 𝐹 = (𝑓 ∈ (𝑆 Cn 𝑇), 𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝑓 ∘ 𝑔))
196		vex 3203	. . . . . . . . . . . . . . . 16 ⊢ 𝑢 ∈ V
197		vex 3203	. . . . . . . . . . . . . . . 16 ⊢ 𝑣 ∈ V
198	196, 197	coex 7118	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∘ 𝑣) ∈ V
199	193, 194, 195, 198	ovmpt2 6796	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ 𝑣 ∈ (𝑅 Cn 𝑆)) → (𝑢𝐹𝑣) = (𝑢 ∘ 𝑣))
200	191, 192, 199	syl2anc 693	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢𝐹𝑣) = (𝑢 ∘ 𝑣))
201		cnco 21070	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ (𝑅 Cn 𝑆) ∧ 𝑢 ∈ (𝑆 Cn 𝑇)) → (𝑢 ∘ 𝑣) ∈ (𝑅 Cn 𝑇))
202	192, 191, 201	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 ∘ 𝑣) ∈ (𝑅 Cn 𝑇))
203		imaco 5640	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∘ 𝑣) “ 𝐾) = (𝑢 “ (𝑣 “ 𝐾))
204		simprrr 805	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
205	15	ntrss2 20861	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ Top ∧ (𝑘‘𝑦) ⊆ ∪ 𝑆) → ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦))
206	205	ex 450	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑆 ∈ Top → ((𝑘‘𝑦) ⊆ ∪ 𝑆 → ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦)))
207	206	ralimdv 2963	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ∈ Top → (∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦)))
208	90, 130, 207	sylc 65	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦))
209		ss2iun 4536	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦))
210	208, 209	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦))
211	210, 111	sseqtrd 3641	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ ran 𝑘)
212	211	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ ran 𝑘)
213	204, 212	sstrd 3613	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑣 “ 𝐾) ⊆ ∪ ran 𝑘)
214		imass2 5501	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 “ 𝐾) ⊆ ∪ ran 𝑘 → (𝑢 “ (𝑣 “ 𝐾)) ⊆ (𝑢 “ ∪ ran 𝑘))
215	213, 214	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ (𝑣 “ 𝐾)) ⊆ (𝑢 “ ∪ ran 𝑘))
216		simprlr 803	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉)
217	215, 216	sstrd 3613	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ (𝑣 “ 𝐾)) ⊆ 𝑉)
218	203, 217	syl5eqss 3649	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → ((𝑢 ∘ 𝑣) “ 𝐾) ⊆ 𝑉)
219		imaeq1 5461	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = (𝑢 ∘ 𝑣) → (ℎ “ 𝐾) = ((𝑢 ∘ 𝑣) “ 𝐾))
220	219	sseq1d 3632	. . . . . . . . . . . . . . 15 ⊢ (ℎ = (𝑢 ∘ 𝑣) → ((ℎ “ 𝐾) ⊆ 𝑉 ↔ ((𝑢 ∘ 𝑣) “ 𝐾) ⊆ 𝑉))
221	220	elrab 3363	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∘ 𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ((𝑢 ∘ 𝑣) ∈ (𝑅 Cn 𝑇) ∧ ((𝑢 ∘ 𝑣) “ 𝐾) ⊆ 𝑉))
222	202, 218, 221	sylanbrc 698	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 ∘ 𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
223	200, 222	eqeltrd 2701	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
224	190, 223	sylan2b 492	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) → (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
225	224	ralrimivva 2971	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
226	195	mpt2fun 6762	. . . . . . . . . . 11 ⊢ Fun 𝐹
227		ssrab2 3687	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇)
228		ssrab2 3687	. . . . . . . . . . . . 13 ⊢ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ⊆ (𝑅 Cn 𝑆)
229		xpss12 5225	. . . . . . . . . . . . 13 ⊢ (({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ⊆ (𝑅 Cn 𝑆)) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆)))
230	227, 228, 229	mp2an 708	. . . . . . . . . . . 12 ⊢ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))
231		vex 3203	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
232		vex 3203	. . . . . . . . . . . . . 14 ⊢ 𝑔 ∈ V
233	231, 232	coex 7118	. . . . . . . . . . . . 13 ⊢ (𝑓 ∘ 𝑔) ∈ V
234	195, 233	dmmpt2 7240	. . . . . . . . . . . 12 ⊢ dom 𝐹 = ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))
235	230, 234	sseqtr4i 3638	. . . . . . . . . . 11 ⊢ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹
236		funimassov 6811	. . . . . . . . . . 11 ⊢ ((Fun 𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))
237	226, 235, 236	mp2an 708	. . . . . . . . . 10 ⊢ ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
238	225, 237	sylibr 224	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
239		funimass3 6333	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))
240	226, 235, 239	mp2an 708	. . . . . . . . 9 ⊢ ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))
241	238, 240	sylib 208	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))
242		eleq2 2690	. . . . . . . . . 10 ⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → (⟨𝐴, 𝐵⟩ ∈ 𝑧 ↔ ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})))
243		sseq1 3626	. . . . . . . . . 10 ⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → (𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))
244	242, 243	anbi12d 747	. . . . . . . . 9 ⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → ((⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})) ↔ (⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
245	244	rspcev 3309	. . . . . . . 8 ⊢ ((({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∈ ((𝑇 ^_ko 𝑆) ×_t (𝑆 ^_ko 𝑅)) ∧ (⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))) → ∃𝑧 ∈ ((𝑇 ^_ko 𝑆) ×_t (𝑆 ^_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))
246	139, 183, 241, 245	syl12anc 1324	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∃𝑧 ∈ ((𝑇 ^_ko 𝑆) ×_t (𝑆 ^_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))
247	246	expr 643	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ (𝐵 “ 𝐾) = ∪ 𝑤) → ((𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ^_ko 𝑆) ×_t (𝑆 ^_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
248	247	exlimdv 1861	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ (𝐵 “ 𝐾) = ∪ 𝑤) → (∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ^_ko 𝑆) ×_t (𝑆 ^_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
249	89, 248	syldan 487	. . . 4 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤) → (∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ^_ko 𝑆) ×_t (𝑆 ^_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
250	249	expimpd 629	. . 3 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) → ((∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))) → ∃𝑧 ∈ ((𝑇 ^_ko 𝑆) ×_t (𝑆 ^_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
251	250	rexlimdva 3031	. 2 ⊢ (𝜑 → (∃𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)(∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))) → ∃𝑧 ∈ ((𝑇 ^_ko 𝑆) ×_t (𝑆 ^_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
252	86, 251	mpd 15	1 ⊢ (𝜑 → ∃𝑧 ∈ ((𝑇 ^_ko 𝑆) ×_t (𝑆 ^_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∃wex 1704 ∈ wcel 1990 ∀wral 2912 ∃wrex 2913 {crab 2916 Vcvv 3200 ∩ cin 3573 ⊆ wss 3574 𝒫 cpw 4158 ⟨cop 4183 ∪ cuni 4436 ∪ ciun 4520 × cxp 5112 ^◡ccnv 5113 dom cdm 5114 ran crn 5115 “ cima 5117 ∘ ccom 5118 Fun wfun 5882 Fn wfn 5883 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ↦ cmpt2 6652 Fincfn 7955 ↾_t crest 16081 Topctop 20698 intcnt 20821 Cn ccn 21028 Compccmp 21189 𝑛-Locally cnlly 21268 ×_t ctx 21363 ^_ko cxko 21364

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-fin 7959 df-fi 8317 df-rest 16083 df-topgen 16104 df-top 20699 df-topon 20716 df-bases 20750 df-ntr 20824 df-nei 20902 df-cn 21031 df-cmp 21190 df-nlly 21270 df-tx 21365 df-xko 21366

This theorem is referenced by: xkococn 21463

W3C validator