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 23649

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 23387	. . . 4 ⊢ ((𝐵 ∈ (𝑅 Cn 𝑆) ∧ (𝑅 ↾_t 𝐾) ∈ Comp) → (𝑆 ↾_t (𝐵 “ 𝐾)) ∈ Comp)
4	1, 2, 3	syl2anc 590	. . 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 23255	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑆 Cn 𝑇) ∧ 𝑉 ∈ 𝑇) → (^◡𝐴 “ 𝑉) ∈ 𝑆)
10	7, 8, 9	syl2anc 590	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐴 “ 𝑉) ∈ 𝑆)
11	10	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → (^◡𝐴 “ 𝑉) ∈ 𝑆)
12		imaco 6209	. . . . . . . . . . 11 ⊢ ((𝐴 ∘ 𝐵) “ 𝐾) = (𝐴 “ (𝐵 “ 𝐾))
13		xkococn.i	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 ∘ 𝐵) “ 𝐾) ⊆ 𝑉)
14	12, 13	eqsstrrid 3961	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉)
15		eqid 2740	. . . . . . . . . . . . 13 ⊢ ∪ 𝑆 = ∪ 𝑆
16		eqid 2740	. . . . . . . . . . . . 13 ⊢ ∪ 𝑇 = ∪ 𝑇
17	15, 16	cnf 23236	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (𝑆 Cn 𝑇) → 𝐴:∪ 𝑆⟶∪ 𝑇)
18		ffun 6665	. . . . . . . . . . . 12 ⊢ (𝐴:∪ 𝑆⟶∪ 𝑇 → Fun 𝐴)
19	7, 17, 18	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → Fun 𝐴)
20		imassrn 6030	. . . . . . . . . . . . 13 ⊢ (𝐵 “ 𝐾) ⊆ ran 𝐵
21		eqid 2740	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑅 = ∪ 𝑅
22	21, 15	cnf 23236	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → 𝐵:∪ 𝑅⟶∪ 𝑆)
23		frn 6669	. . . . . . . . . . . . . 14 ⊢ (𝐵:∪ 𝑅⟶∪ 𝑆 → ran 𝐵 ⊆ ∪ 𝑆)
24	1, 22, 23	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐵 ⊆ ∪ 𝑆)
25	20, 24	sstrid 3933	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ ∪ 𝑆)
26		fdm 6671	. . . . . . . . . . . . 13 ⊢ (𝐴:∪ 𝑆⟶∪ 𝑇 → dom 𝐴 = ∪ 𝑆)
27	7, 17, 26	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → dom 𝐴 = ∪ 𝑆)
28	25, 27	sseqtrrd 3959	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ dom 𝐴)
29		funimass3 7002	. . . . . . . . . . 11 ⊢ ((Fun 𝐴 ∧ (𝐵 “ 𝐾) ⊆ dom 𝐴) → ((𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉 ↔ (𝐵 “ 𝐾) ⊆ (^◡𝐴 “ 𝑉)))
30	19, 28, 29	syl2anc 590	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉 ↔ (𝐵 “ 𝐾) ⊆ (^◡𝐴 “ 𝑉)))
31	14, 30	mpbid 233	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ (^◡𝐴 “ 𝑉))
32	31	sselda 3922	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → 𝑥 ∈ (^◡𝐴 “ 𝑉))
33		nlly2i 23466	. . . . . . . 8 ⊢ ((𝑆 ∈ 𝑛-Locally Comp ∧ (^◡𝐴 “ 𝑉) ∈ 𝑆 ∧ 𝑥 ∈ (^◡𝐴 “ 𝑉)) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))
34	6, 11, 32, 33	syl3anc 1379	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))
35		nllytop 23463	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ 𝑛-Locally Comp → 𝑆 ∈ Top)
36	5, 35	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ Top)
37	36	ad3antrrr 736	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
38		imaexg 7860	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → (𝐵 “ 𝐾) ∈ V)
39	1, 38	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 “ 𝐾) ∈ V)
40	39	ad3antrrr 736	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝐵 “ 𝐾) ∈ V)
41		simprl 776	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑢 ∈ 𝑆)
42		elrestr 17389	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Top ∧ (𝐵 “ 𝐾) ∈ V ∧ 𝑢 ∈ 𝑆) → (𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾_t (𝐵 “ 𝐾)))
43	37, 40, 41, 42	syl3anc 1379	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾_t (𝐵 “ 𝐾)))
44		simprr1 1228	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑥 ∈ 𝑢)
45		simpllr 781	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝐵 “ 𝐾))
46	44, 45	elind 4136	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)))
47		inss1 4172	. . . . . . . . . . . 12 ⊢ (𝑢 ∩ (𝐵 “ 𝐾)) ⊆ 𝑢
48		elpwi 4543	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉) → 𝑠 ⊆ (^◡𝐴 “ 𝑉))
49	48	ad2antlr 733	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑠 ⊆ (^◡𝐴 “ 𝑉))
50		elssuni 4876	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐴 “ 𝑉) ∈ 𝑆 → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
51	10, 50	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
52	51	ad3antrrr 736	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
53	49, 52	sstrd 3932	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑠 ⊆ ∪ 𝑆)
54		simprr2 1229	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑢 ⊆ 𝑠)
55	15	ssntr 23048	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ Top ∧ 𝑠 ⊆ ∪ 𝑆) ∧ (𝑢 ∈ 𝑆 ∧ 𝑢 ⊆ 𝑠)) → 𝑢 ⊆ ((int‘𝑆)‘𝑠))
56	37, 53, 41, 54, 55	syl22anc 844	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑢 ⊆ ((int‘𝑆)‘𝑠))
57	47, 56	sstrid 3933	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠))
58		simprr3 1230	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝑆 ↾_t 𝑠) ∈ Comp)
59	57, 58	jca 516	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))
60		eleq2 2829	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾))))
61		cleq1lem 14942	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp) ↔ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
62	60, 61	anbi12d 638	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → ((𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ (𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)) ∧ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))))
63	62	rspcev 3567	. . . . . . . . . 10 ⊢ (((𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾_t (𝐵 “ 𝐾)) ∧ (𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)) ∧ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
64	43, 46, 59, 63	syl12anc 842	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
65	64	rexlimdvaa 3142	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) → (∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))))
66	65	reximdva 3153	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))))
67	34, 66	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
68		rexcom 3269	. . . . . . 7 ⊢ (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
69		r19.42v 3172	. . . . . . . 8 ⊢ (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ (𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
70	69	rexbii 3087	. . . . . . 7 ⊢ (∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
71	68, 70	bitri 276	. . . . . 6 ⊢ (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
72	67, 71	sylib 219	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
73	72	ralrimiva 3132	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ (𝐵 “ 𝐾)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
74	15	restuni 23152	. . . . 5 ⊢ ((𝑆 ∈ Top ∧ (𝐵 “ 𝐾) ⊆ ∪ 𝑆) → (𝐵 “ 𝐾) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾)))
75	36, 25, 74	syl2anc 590	. . . 4 ⊢ (𝜑 → (𝐵 “ 𝐾) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾)))
76	73, 75	raleqtrdv 3300	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ∪ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
77		eqid 2740	. . . 4 ⊢ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾))
78		fveq2 6834	. . . . . 6 ⊢ (𝑠 = (𝑘‘𝑦) → ((int‘𝑆)‘𝑠) = ((int‘𝑆)‘(𝑘‘𝑦)))
79	78	sseq2d 3954	. . . . 5 ⊢ (𝑠 = (𝑘‘𝑦) → (𝑦 ⊆ ((int‘𝑆)‘𝑠) ↔ 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦))))
80		oveq2 7371	. . . . . 6 ⊢ (𝑠 = (𝑘‘𝑦) → (𝑆 ↾_t 𝑠) = (𝑆 ↾_t (𝑘‘𝑦)))
81	80	eleq1d 2825	. . . . 5 ⊢ (𝑠 = (𝑘‘𝑦) → ((𝑆 ↾_t 𝑠) ∈ Comp ↔ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))
82	79, 81	anbi12d 638	. . . 4 ⊢ (𝑠 = (𝑘‘𝑦) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp) ↔ (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))
83	77, 82	cmpcovf 23381	. . 3 ⊢ (((𝑆 ↾_t (𝐵 “ 𝐾)) ∈ Comp ∧ ∀𝑥 ∈ ∪ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ∃𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)(∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))))
84	4, 76, 83	syl2anc 590	. 2 ⊢ (𝜑 → ∃𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)(∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))))
85	75	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) → (𝐵 “ 𝐾) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾)))
86	85	eqeq1d 2742	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) → ((𝐵 “ 𝐾) = ∪ 𝑤 ↔ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤))
87	86	biimpar 478	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤) → (𝐵 “ 𝐾) = ∪ 𝑤)
88	36	ad2antrr 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑆 ∈ Top)
89		cntop2 23231	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (𝑆 Cn 𝑇) → 𝑇 ∈ Top)
90	7, 89	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ Top)
91	90	ad2antrr 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑇 ∈ Top)
92		xkotop 23578	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ↑_ko 𝑆) ∈ Top)
93	88, 91, 92	syl2anc 590	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑇 ↑_ko 𝑆) ∈ Top)
94		cntop1 23230	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → 𝑅 ∈ Top)
95	1, 94	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ Top)
96	95	ad2antrr 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑅 ∈ Top)
97		xkotop 23578	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑_ko 𝑅) ∈ Top)
98	96, 88, 97	syl2anc 590	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↑_ko 𝑅) ∈ Top)
99		simprrl 786	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉))
100	99	frnd 6670	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ran 𝑘 ⊆ 𝒫 (^◡𝐴 “ 𝑉))
101		sspwuni 5036	. . . . . . . . . . . 12 ⊢ (ran 𝑘 ⊆ 𝒫 (^◡𝐴 “ 𝑉) ↔ ∪ ran 𝑘 ⊆ (^◡𝐴 “ 𝑉))
102	100, 101	sylib 219	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ (^◡𝐴 “ 𝑉))
103	10	ad2antrr 732	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (^◡𝐴 “ 𝑉) ∈ 𝑆)
104	103, 50	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
105	102, 104	sstrd 3932	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ ∪ 𝑆)
106		ffn 6662	. . . . . . . . . . . . 13 ⊢ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) → 𝑘 Fn 𝑤)
107		fniunfv 7198	. . . . . . . . . . . . 13 ⊢ (𝑘 Fn 𝑤 → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘)
108	99, 106, 107	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘)
109	108	oveq2d 7379	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾_t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = (𝑆 ↾_t ∪ ran 𝑘))
110		simplr 774	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin))
111	110	elin2d 4141	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑤 ∈ Fin)
112		simprrr 787	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))
113		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)
114	113	ralimi 3077	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → ∀𝑦 ∈ 𝑤 (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)
115	112, 114	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)
116	15	fiuncmp 23394	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Top ∧ 𝑤 ∈ Fin ∧ ∀𝑦 ∈ 𝑤 (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → (𝑆 ↾_t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) ∈ Comp)
117	88, 111, 115, 116	syl3anc 1379	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾_t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) ∈ Comp)
118	109, 117	eqeltrrd 2841	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾_t ∪ ran 𝑘) ∈ Comp)
119	8	ad2antrr 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑉 ∈ 𝑇)
120	15, 88, 91, 105, 118, 119	xkoopn 23579	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∈ (𝑇 ↑_ko 𝑆))
121		xkococn.k	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ⊆ ∪ 𝑅)
122	121	ad2antrr 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐾 ⊆ ∪ 𝑅)
123	2	ad2antrr 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑅 ↾_t 𝐾) ∈ Comp)
124	108, 105	eqsstrd 3956	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆)
125		iunss 4981	. . . . . . . . . . . . 13 ⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆)
126	124, 125	sylib 219	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆)
127	15	ntropn 23039	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ Top ∧ (𝑘‘𝑦) ⊆ ∪ 𝑆) → ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
128	127	ex 413	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Top → ((𝑘‘𝑦) ⊆ ∪ 𝑆 → ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆))
129	128	ralimdv 3154	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ Top → (∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆))
130	88, 126, 129	sylc 65	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
131		iunopn 22888	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Top ∧ ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
132	88, 130, 131	syl2anc 590	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
133	21, 96, 88, 122, 123, 132	xkoopn 23579	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ∈ (𝑆 ↑_ko 𝑅))
134		txopn 23592	. . . . . . . . 9 ⊢ ((((𝑇 ↑_ko 𝑆) ∈ Top ∧ (𝑆 ↑_ko 𝑅) ∈ Top) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∈ (𝑇 ↑_ko 𝑆) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ∈ (𝑆 ↑_ko 𝑅))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)))
135	93, 98, 120, 133, 134	syl22anc 844	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)))
136		imaeq1 6014	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝑎 “ ∪ ran 𝑘) = (𝐴 “ ∪ ran 𝑘))
137	136	sseq1d 3953	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((𝑎 “ ∪ ran 𝑘) ⊆ 𝑉 ↔ (𝐴 “ ∪ ran 𝑘) ⊆ 𝑉))
138	7	ad2antrr 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐴 ∈ (𝑆 Cn 𝑇))
139		imaiun 7196	. . . . . . . . . . . 12 ⊢ (𝐴 “ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦))
140	108	imaeq2d 6019	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐴 “ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = (𝐴 “ ∪ ran 𝑘))
141	139, 140	eqtr3id 2789	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) = (𝐴 “ ∪ ran 𝑘))
142	108, 102	eqsstrd 3956	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉))
143	19	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → Fun 𝐴)
144	99, 106	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑘 Fn 𝑤)
145	27	ad2antrr 732	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → dom 𝐴 = ∪ 𝑆)
146	105, 145	sseqtrrd 3959	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ dom 𝐴)
147		simpl1 1198	. . . . . . . . . . . . . . . 16 ⊢ (((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → Fun 𝐴)
148	107	3ad2ant2 1140	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘)
149		simp3 1144	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪ ran 𝑘 ⊆ dom 𝐴)
150	148, 149	eqsstrd 3956	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴)
151		iunss 4981	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴)
152	150, 151	sylib 219	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴)
153	152	r19.21bi 3232	. . . . . . . . . . . . . . . 16 ⊢ (((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → (𝑘‘𝑦) ⊆ dom 𝐴)
154		funimass3 7002	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐴 ∧ (𝑘‘𝑦) ⊆ dom 𝐴) → ((𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
155	147, 153, 154	syl2anc 590	. . . . . . . . . . . . . . 15 ⊢ (((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → ((𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
156	155	ralbidva 3161	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → (∀𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
157		iunss 4981	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∀𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉)
158		iunss 4981	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉) ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉))
159	156, 157, 158	3bitr4g 315	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
160	143, 144, 146, 159	syl3anc 1379	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
161	142, 160	mpbird 258	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉)
162	141, 161	eqsstrrd 3957	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐴 “ ∪ ran 𝑘) ⊆ 𝑉)
163	137, 138, 162	elrabd 3638	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐴 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉})
164		imaeq1 6014	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝑏 “ 𝐾) = (𝐵 “ 𝐾))
165	164	sseq1d 3953	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ↔ (𝐵 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))
166	1	ad2antrr 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐵 ∈ (𝑅 Cn 𝑆))
167		simprl 776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) = ∪ 𝑤)
168		uniiun 4995	. . . . . . . . . . . 12 ⊢ ∪ 𝑤 = ∪ 𝑦 ∈ 𝑤 𝑦
169	167, 168	eqtrdi 2791	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) = ∪ 𝑦 ∈ 𝑤 𝑦)
170		simpl 483	. . . . . . . . . . . . 13 ⊢ ((𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)))
171	170	ralimi 3077	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → ∀𝑦 ∈ 𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)))
172		ss2iun 4947	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) → ∪ 𝑦 ∈ 𝑤 𝑦 ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
173	112, 171, 172	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 𝑦 ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
174	169, 173	eqsstrd 3956	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
175	165, 166, 174	elrabd 3638	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐵 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})
176	163, 175	opelxpd 5664	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}))
177		imaeq1 6014	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑢 → (𝑎 “ ∪ ran 𝑘) = (𝑢 “ ∪ ran 𝑘))
178	177	sseq1d 3953	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑢 → ((𝑎 “ ∪ ran 𝑘) ⊆ 𝑉 ↔ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉))
179	178	elrab 3636	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ↔ (𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉))
180		imaeq1 6014	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑣 → (𝑏 “ 𝐾) = (𝑣 “ 𝐾))
181	180	sseq1d 3953	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑣 → ((𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ↔ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))
182	181	elrab 3636	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ↔ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))
183	179, 182	anbi12i 634	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ↔ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))))
184		simprll 784	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → 𝑢 ∈ (𝑆 Cn 𝑇))
185		simprrl 786	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → 𝑣 ∈ (𝑅 Cn 𝑆))
186		coeq1 5806	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑢 → (𝑓 ∘ 𝑔) = (𝑢 ∘ 𝑔))
187		coeq2 5807	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑣 → (𝑢 ∘ 𝑔) = (𝑢 ∘ 𝑣))
188		xkococn.1	. . . . . . . . . . . . . . 15 ⊢ 𝐹 = (𝑓 ∈ (𝑆 Cn 𝑇), 𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝑓 ∘ 𝑔))
189		vex 3436	. . . . . . . . . . . . . . . 16 ⊢ 𝑢 ∈ V
190		vex 3436	. . . . . . . . . . . . . . . 16 ⊢ 𝑣 ∈ V
191	189, 190	coex 7877	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∘ 𝑣) ∈ V
192	186, 187, 188, 191	ovmpo 7523	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ 𝑣 ∈ (𝑅 Cn 𝑆)) → (𝑢𝐹𝑣) = (𝑢 ∘ 𝑣))
193	184, 185, 192	syl2anc 590	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢𝐹𝑣) = (𝑢 ∘ 𝑣))
194		imaeq1 6014	. . . . . . . . . . . . . . 15 ⊢ (ℎ = (𝑢 ∘ 𝑣) → (ℎ “ 𝐾) = ((𝑢 ∘ 𝑣) “ 𝐾))
195	194	sseq1d 3953	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑢 ∘ 𝑣) → ((ℎ “ 𝐾) ⊆ 𝑉 ↔ ((𝑢 ∘ 𝑣) “ 𝐾) ⊆ 𝑉))
196		cnco 23256	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ (𝑅 Cn 𝑆) ∧ 𝑢 ∈ (𝑆 Cn 𝑇)) → (𝑢 ∘ 𝑣) ∈ (𝑅 Cn 𝑇))
197	185, 184, 196	syl2anc 590	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 ∘ 𝑣) ∈ (𝑅 Cn 𝑇))
198		imaco 6209	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∘ 𝑣) “ 𝐾) = (𝑢 “ (𝑣 “ 𝐾))
199		simprrr 787	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
200	15	ntrss2 23047	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ Top ∧ (𝑘‘𝑦) ⊆ ∪ 𝑆) → ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦))
201	200	ex 413	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑆 ∈ Top → ((𝑘‘𝑦) ⊆ ∪ 𝑆 → ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦)))
202	201	ralimdv 3154	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ∈ Top → (∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦)))
203	88, 126, 202	sylc 65	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦))
204		ss2iun 4947	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦))
205	203, 204	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦))
206	205, 108	sseqtrd 3958	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ ran 𝑘)
207	206	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ ran 𝑘)
208	199, 207	sstrd 3932	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑣 “ 𝐾) ⊆ ∪ ran 𝑘)
209		imass2 6061	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 “ 𝐾) ⊆ ∪ ran 𝑘 → (𝑢 “ (𝑣 “ 𝐾)) ⊆ (𝑢 “ ∪ ran 𝑘))
210	208, 209	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ (𝑣 “ 𝐾)) ⊆ (𝑢 “ ∪ ran 𝑘))
211		simprlr 785	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉)
212	210, 211	sstrd 3932	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ (𝑣 “ 𝐾)) ⊆ 𝑉)
213	198, 212	eqsstrid 3960	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → ((𝑢 ∘ 𝑣) “ 𝐾) ⊆ 𝑉)
214	195, 197, 213	elrabd 3638	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 ∘ 𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
215	193, 214	eqeltrd 2840	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
216	183, 215	sylan2b 600	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) → (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
217	216	ralrimivva 3183	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
218	188	mpofun 7487	. . . . . . . . . . 11 ⊢ Fun 𝐹
219		ssrab2 4018	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇)
220		ssrab2 4018	. . . . . . . . . . . . 13 ⊢ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ⊆ (𝑅 Cn 𝑆)
221		xpss12 5640	. . . . . . . . . . . . 13 ⊢ (({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ⊆ (𝑅 Cn 𝑆)) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆)))
222	219, 220, 221	mp2an 698	. . . . . . . . . . . 12 ⊢ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))
223		vex 3436	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
224		vex 3436	. . . . . . . . . . . . . 14 ⊢ 𝑔 ∈ V
225	223, 224	coex 7877	. . . . . . . . . . . . 13 ⊢ (𝑓 ∘ 𝑔) ∈ V
226	188, 225	dmmpo 8020	. . . . . . . . . . . 12 ⊢ dom 𝐹 = ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))
227	222, 226	sseqtrri 3971	. . . . . . . . . . 11 ⊢ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹
228		funimassov 7540	. . . . . . . . . . 11 ⊢ ((Fun 𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))
229	218, 227, 228	mp2an 698	. . . . . . . . . 10 ⊢ ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
230	217, 229	sylibr 235	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
231		funimass3 7002	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))
232	218, 227, 231	mp2an 698	. . . . . . . . 9 ⊢ ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))
233	230, 232	sylib 219	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))
234		eleq2 2829	. . . . . . . . . 10 ⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → (⟨𝐴, 𝐵⟩ ∈ 𝑧 ↔ ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})))
235		sseq1 3947	. . . . . . . . . 10 ⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → (𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))
236	234, 235	anbi12d 638	. . . . . . . . 9 ⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → ((⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})) ↔ (⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
237	236	rspcev 3567	. . . . . . . 8 ⊢ ((({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)) ∧ (⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))
238	135, 176, 233, 237	syl12anc 842	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))
239	238	expr 457	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ (𝐵 “ 𝐾) = ∪ 𝑤) → ((𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
240	239	exlimdv 1940	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ (𝐵 “ 𝐾) = ∪ 𝑤) → (∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
241	87, 240	syldan 597	. . . 4 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤) → (∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
242	241	expimpd 454	. . 3 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) → ((∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
243	242	rexlimdva 3141	. 2 ⊢ (𝜑 → (∃𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)(∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
244	84, 243	mpd 15	1 ⊢ (𝜑 → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∃wex 1786 ∈ wcel 2119 ∀wral 3054 ∃wrex 3064 {crab 3392 Vcvv 3432 ∩ cin 3889 ⊆ wss 3890 𝒫 cpw 4536 ⟨cop 4568 ∪ cuni 4845 ∪ ciun 4928 × cxp 5623 ^◡ccnv 5624 dom cdm 5625 ran crn 5626 “ cima 5628 ∘ ccom 5629 Fun wfun 6486 Fn wfn 6487 ⟶wf 6488 ‘cfv 6492 (class class class)co 7363 ∈ cmpo 7365 Fincfn 8890 ↾_t crest 17381 Topctop 22883 intcnt 23007 Cn ccn 23214 Compccmp 23376 𝑛-Locally cnlly 23455 ×_t ctx 23550 ↑_ko cxko 23551

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-rep 5206 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 ax-un 7685

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-ral 3055 df-rex 3065 df-reu 3346 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4846 df-int 4885 df-iun 4930 df-br 5080 df-opab 5142 df-mpt 5161 df-tr 5187 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7366 df-oprab 7367 df-mpo 7368 df-om 7814 df-1st 7938 df-2nd 7939 df-1o 8402 df-map 8772 df-en 8891 df-dom 8892 df-fin 8894 df-fi 9321 df-rest 17383 df-topgen 17404 df-top 22884 df-topon 22901 df-bases 22936 df-ntr 23010 df-nei 23088 df-cn 23217 df-cmp 23377 df-nlly 23457 df-tx 23552 df-xko 23553

This theorem is referenced by: xkococn 23650

W3C validator