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 23699

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 23437	. . . 4 ⊢ ((𝐵 ∈ (𝑅 Cn 𝑆) ∧ (𝑅 ↾_t 𝐾) ∈ Comp) → (𝑆 ↾_t (𝐵 “ 𝐾)) ∈ Comp)
4	1, 2, 3	syl2anc 593	. . 3 ⊢ (𝜑 → (𝑆 ↾_t (𝐵 “ 𝐾)) ∈ Comp)
5		xkococn.s	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ 𝑛-Locally Comp)
6	5	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → 𝑆 ∈ 𝑛-Locally Comp)
7		xkococn.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ (𝑆 Cn 𝑇))
8		xkococn.v	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ 𝑇)
9		cnima 23305	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑆 Cn 𝑇) ∧ 𝑉 ∈ 𝑇) → (^◡𝐴 “ 𝑉) ∈ 𝑆)
10	7, 8, 9	syl2anc 593	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐴 “ 𝑉) ∈ 𝑆)
11	10	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → (^◡𝐴 “ 𝑉) ∈ 𝑆)
12		imaco 6234	. . . . . . . . . . 11 ⊢ ((𝐴 ∘ 𝐵) “ 𝐾) = (𝐴 “ (𝐵 “ 𝐾))
13		xkococn.i	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 ∘ 𝐵) “ 𝐾) ⊆ 𝑉)
14	12, 13	eqsstrrid 3975	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉)
15		eqid 2761	. . . . . . . . . . . . 13 ⊢ ∪ 𝑆 = ∪ 𝑆
16		eqid 2761	. . . . . . . . . . . . 13 ⊢ ∪ 𝑇 = ∪ 𝑇
17	15, 16	cnf 23286	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (𝑆 Cn 𝑇) → 𝐴:∪ 𝑆⟶∪ 𝑇)
18		ffun 6690	. . . . . . . . . . . 12 ⊢ (𝐴:∪ 𝑆⟶∪ 𝑇 → Fun 𝐴)
19	7, 17, 18	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → Fun 𝐴)
20		imassrn 6057	. . . . . . . . . . . . 13 ⊢ (𝐵 “ 𝐾) ⊆ ran 𝐵
21		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑅 = ∪ 𝑅
22	21, 15	cnf 23286	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → 𝐵:∪ 𝑅⟶∪ 𝑆)
23		frn 6695	. . . . . . . . . . . . . 14 ⊢ (𝐵:∪ 𝑅⟶∪ 𝑆 → ran 𝐵 ⊆ ∪ 𝑆)
24	1, 22, 23	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐵 ⊆ ∪ 𝑆)
25	20, 24	sstrid 3947	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ ∪ 𝑆)
26		fdm 6697	. . . . . . . . . . . . 13 ⊢ (𝐴:∪ 𝑆⟶∪ 𝑇 → dom 𝐴 = ∪ 𝑆)
27	7, 17, 26	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → dom 𝐴 = ∪ 𝑆)
28	25, 27	sseqtrrd 3973	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ dom 𝐴)
29		funimass3 7031	. . . . . . . . . . 11 ⊢ ((Fun 𝐴 ∧ (𝐵 “ 𝐾) ⊆ dom 𝐴) → ((𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉 ↔ (𝐵 “ 𝐾) ⊆ (^◡𝐴 “ 𝑉)))
30	19, 28, 29	syl2anc 593	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉 ↔ (𝐵 “ 𝐾) ⊆ (^◡𝐴 “ 𝑉)))
31	14, 30	mpbid 234	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ (^◡𝐴 “ 𝑉))
32	31	sselda 3936	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → 𝑥 ∈ (^◡𝐴 “ 𝑉))
33		nlly2i 23516	. . . . . . . 8 ⊢ ((𝑆 ∈ 𝑛-Locally Comp ∧ (^◡𝐴 “ 𝑉) ∈ 𝑆 ∧ 𝑥 ∈ (^◡𝐴 “ 𝑉)) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))
34	6, 11, 32, 33	syl3anc 1389	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))
35		nllytop 23513	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ 𝑛-Locally Comp → 𝑆 ∈ Top)
36	5, 35	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ Top)
37	36	ad3antrrr 740	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
38		imaexg 7890	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → (𝐵 “ 𝐾) ∈ V)
39	1, 38	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 “ 𝐾) ∈ V)
40	39	ad3antrrr 740	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝐵 “ 𝐾) ∈ V)
41		simprl 780	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑢 ∈ 𝑆)
42		elrestr 17440	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Top ∧ (𝐵 “ 𝐾) ∈ V ∧ 𝑢 ∈ 𝑆) → (𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾_t (𝐵 “ 𝐾)))
43	37, 40, 41, 42	syl3anc 1389	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾_t (𝐵 “ 𝐾)))
44		simprr1 1234	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑥 ∈ 𝑢)
45		simpllr 785	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝐵 “ 𝐾))
46	44, 45	elind 4152	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)))
47		inss1 4188	. . . . . . . . . . . 12 ⊢ (𝑢 ∩ (𝐵 “ 𝐾)) ⊆ 𝑢
48		elpwi 4561	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉) → 𝑠 ⊆ (^◡𝐴 “ 𝑉))
49	48	ad2antlr 737	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑠 ⊆ (^◡𝐴 “ 𝑉))
50		elssuni 4896	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐴 “ 𝑉) ∈ 𝑆 → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
51	10, 50	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
52	51	ad3antrrr 740	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
53	49, 52	sstrd 3946	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑠 ⊆ ∪ 𝑆)
54		simprr2 1235	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑢 ⊆ 𝑠)
55	15	ssntr 23098	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ Top ∧ 𝑠 ⊆ ∪ 𝑆) ∧ (𝑢 ∈ 𝑆 ∧ 𝑢 ⊆ 𝑠)) → 𝑢 ⊆ ((int‘𝑆)‘𝑠))
56	37, 53, 41, 54, 55	syl22anc 849	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑢 ⊆ ((int‘𝑆)‘𝑠))
57	47, 56	sstrid 3947	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠))
58		simprr3 1236	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝑆 ↾_t 𝑠) ∈ Comp)
59	57, 58	jca 519	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))
60		eleq2 2850	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾))))
61		cleq1lem 14992	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp) ↔ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
62	60, 61	anbi12d 641	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → ((𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ (𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)) ∧ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))))
63	62	rspcev 3581	. . . . . . . . . 10 ⊢ (((𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾_t (𝐵 “ 𝐾)) ∧ (𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)) ∧ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
64	43, 46, 59, 63	syl12anc 847	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
65	64	rexlimdvaa 3163	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) → (∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))))
66	65	reximdva 3174	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))))
67	34, 66	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
68		rexcom 3290	. . . . . . 7 ⊢ (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
69		r19.42v 3193	. . . . . . . 8 ⊢ (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ (𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
70	69	rexbii 3108	. . . . . . 7 ⊢ (∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
71	68, 70	bitri 277	. . . . . 6 ⊢ (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
72	67, 71	sylib 220	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
73	72	ralrimiva 3153	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ (𝐵 “ 𝐾)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
74	15	restuni 23202	. . . . 5 ⊢ ((𝑆 ∈ Top ∧ (𝐵 “ 𝐾) ⊆ ∪ 𝑆) → (𝐵 “ 𝐾) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾)))
75	36, 25, 74	syl2anc 593	. . . 4 ⊢ (𝜑 → (𝐵 “ 𝐾) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾)))
76	73, 75	raleqtrdv 3321	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ∪ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
77		eqid 2761	. . . 4 ⊢ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾))
78		fveq2 6863	. . . . . 6 ⊢ (𝑠 = (𝑘‘𝑦) → ((int‘𝑆)‘𝑠) = ((int‘𝑆)‘(𝑘‘𝑦)))
79	78	sseq2d 3968	. . . . 5 ⊢ (𝑠 = (𝑘‘𝑦) → (𝑦 ⊆ ((int‘𝑆)‘𝑠) ↔ 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦))))
80		oveq2 7400	. . . . . 6 ⊢ (𝑠 = (𝑘‘𝑦) → (𝑆 ↾_t 𝑠) = (𝑆 ↾_t (𝑘‘𝑦)))
81	80	eleq1d 2846	. . . . 5 ⊢ (𝑠 = (𝑘‘𝑦) → ((𝑆 ↾_t 𝑠) ∈ Comp ↔ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))
82	79, 81	anbi12d 641	. . . 4 ⊢ (𝑠 = (𝑘‘𝑦) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp) ↔ (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))
83	77, 82	cmpcovf 23431	. . 3 ⊢ (((𝑆 ↾_t (𝐵 “ 𝐾)) ∈ Comp ∧ ∀𝑥 ∈ ∪ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ∃𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)(∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))))
84	4, 76, 83	syl2anc 593	. 2 ⊢ (𝜑 → ∃𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)(∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))))
85	75	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) → (𝐵 “ 𝐾) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾)))
86	85	eqeq1d 2763	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) → ((𝐵 “ 𝐾) = ∪ 𝑤 ↔ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤))
87	86	biimpar 481	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤) → (𝐵 “ 𝐾) = ∪ 𝑤)
88	36	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑆 ∈ Top)
89		cntop2 23281	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (𝑆 Cn 𝑇) → 𝑇 ∈ Top)
90	7, 89	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ Top)
91	90	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑇 ∈ Top)
92		xkotop 23628	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ↑_ko 𝑆) ∈ Top)
93	88, 91, 92	syl2anc 593	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑇 ↑_ko 𝑆) ∈ Top)
94		cntop1 23280	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → 𝑅 ∈ Top)
95	1, 94	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ Top)
96	95	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑅 ∈ Top)
97		xkotop 23628	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑_ko 𝑅) ∈ Top)
98	96, 88, 97	syl2anc 593	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↑_ko 𝑅) ∈ Top)
99		simprrl 790	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉))
100	99	frnd 6696	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ran 𝑘 ⊆ 𝒫 (^◡𝐴 “ 𝑉))
101		sspwuni 5056	. . . . . . . . . . . 12 ⊢ (ran 𝑘 ⊆ 𝒫 (^◡𝐴 “ 𝑉) ↔ ∪ ran 𝑘 ⊆ (^◡𝐴 “ 𝑉))
102	100, 101	sylib 220	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ (^◡𝐴 “ 𝑉))
103	10	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (^◡𝐴 “ 𝑉) ∈ 𝑆)
104	103, 50	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
105	102, 104	sstrd 3946	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ ∪ 𝑆)
106		ffn 6687	. . . . . . . . . . . . 13 ⊢ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) → 𝑘 Fn 𝑤)
107		fniunfv 7227	. . . . . . . . . . . . 13 ⊢ (𝑘 Fn 𝑤 → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘)
108	99, 106, 107	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘)
109	108	oveq2d 7408	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾_t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = (𝑆 ↾_t ∪ ran 𝑘))
110		simplr 778	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin))
111	110	elin2d 4157	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑤 ∈ Fin)
112		simprrr 791	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))
113		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)
114	113	ralimi 3098	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → ∀𝑦 ∈ 𝑤 (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)
115	112, 114	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)
116	15	fiuncmp 23444	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Top ∧ 𝑤 ∈ Fin ∧ ∀𝑦 ∈ 𝑤 (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → (𝑆 ↾_t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) ∈ Comp)
117	88, 111, 115, 116	syl3anc 1389	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾_t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) ∈ Comp)
118	109, 117	eqeltrrd 2862	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾_t ∪ ran 𝑘) ∈ Comp)
119	8	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑉 ∈ 𝑇)
120	15, 88, 91, 105, 118, 119	xkoopn 23629	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∈ (𝑇 ↑_ko 𝑆))
121		xkococn.k	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ⊆ ∪ 𝑅)
122	121	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐾 ⊆ ∪ 𝑅)
123	2	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑅 ↾_t 𝐾) ∈ Comp)
124	108, 105	eqsstrd 3970	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆)
125		iunss 5001	. . . . . . . . . . . . 13 ⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆)
126	124, 125	sylib 220	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆)
127	15	ntropn 23089	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ Top ∧ (𝑘‘𝑦) ⊆ ∪ 𝑆) → ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
128	127	ex 416	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Top → ((𝑘‘𝑦) ⊆ ∪ 𝑆 → ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆))
129	128	ralimdv 3175	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ Top → (∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆))
130	88, 126, 129	sylc 65	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
131		iunopn 22938	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Top ∧ ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
132	88, 130, 131	syl2anc 593	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
133	21, 96, 88, 122, 123, 132	xkoopn 23629	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ∈ (𝑆 ↑_ko 𝑅))
134		txopn 23642	. . . . . . . . 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 849	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)))
136		imaeq1 6041	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝑎 “ ∪ ran 𝑘) = (𝐴 “ ∪ ran 𝑘))
137	136	sseq1d 3967	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((𝑎 “ ∪ ran 𝑘) ⊆ 𝑉 ↔ (𝐴 “ ∪ ran 𝑘) ⊆ 𝑉))
138	7	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐴 ∈ (𝑆 Cn 𝑇))
139		imaiun 7225	. . . . . . . . . . . 12 ⊢ (𝐴 “ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦))
140	108	imaeq2d 6046	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐴 “ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = (𝐴 “ ∪ ran 𝑘))
141	139, 140	eqtr3id 2810	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) = (𝐴 “ ∪ ran 𝑘))
142	108, 102	eqsstrd 3970	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉))
143	19	ad2antrr 736	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → Fun 𝐴)
144	99, 106	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑘 Fn 𝑤)
145	27	ad2antrr 736	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → dom 𝐴 = ∪ 𝑆)
146	105, 145	sseqtrrd 3973	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ dom 𝐴)
147		simpl1 1204	. . . . . . . . . . . . . . . 16 ⊢ (((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → Fun 𝐴)
148	107	3ad2ant2 1146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘)
149		simp3 1150	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪ ran 𝑘 ⊆ dom 𝐴)
150	148, 149	eqsstrd 3970	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴)
151		iunss 5001	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴)
152	150, 151	sylib 220	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴)
153	152	r19.21bi 3253	. . . . . . . . . . . . . . . 16 ⊢ (((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → (𝑘‘𝑦) ⊆ dom 𝐴)
154		funimass3 7031	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐴 ∧ (𝑘‘𝑦) ⊆ dom 𝐴) → ((𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
155	147, 153, 154	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ (((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → ((𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
156	155	ralbidva 3182	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → (∀𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
157		iunss 5001	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∀𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉)
158		iunss 5001	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉) ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉))
159	156, 157, 158	3bitr4g 316	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
160	143, 144, 146, 159	syl3anc 1389	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
161	142, 160	mpbird 259	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉)
162	141, 161	eqsstrrd 3971	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐴 “ ∪ ran 𝑘) ⊆ 𝑉)
163	137, 138, 162	elrabd 3652	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐴 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉})
164		imaeq1 6041	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝑏 “ 𝐾) = (𝐵 “ 𝐾))
165	164	sseq1d 3967	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ↔ (𝐵 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))
166	1	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐵 ∈ (𝑅 Cn 𝑆))
167		simprl 780	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) = ∪ 𝑤)
168		uniiun 5015	. . . . . . . . . . . 12 ⊢ ∪ 𝑤 = ∪ 𝑦 ∈ 𝑤 𝑦
169	167, 168	eqtrdi 2812	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) = ∪ 𝑦 ∈ 𝑤 𝑦)
170		simpl 486	. . . . . . . . . . . . 13 ⊢ ((𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)))
171	170	ralimi 3098	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → ∀𝑦 ∈ 𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)))
172		ss2iun 4967	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) → ∪ 𝑦 ∈ 𝑤 𝑦 ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
173	112, 171, 172	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 𝑦 ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
174	169, 173	eqsstrd 3970	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
175	165, 166, 174	elrabd 3652	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐵 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})
176	163, 175	opelxpd 5684	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}))
177		imaeq1 6041	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑢 → (𝑎 “ ∪ ran 𝑘) = (𝑢 “ ∪ ran 𝑘))
178	177	sseq1d 3967	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑢 → ((𝑎 “ ∪ ran 𝑘) ⊆ 𝑉 ↔ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉))
179	178	elrab 3650	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ↔ (𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉))
180		imaeq1 6041	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑣 → (𝑏 “ 𝐾) = (𝑣 “ 𝐾))
181	180	sseq1d 3967	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑣 → ((𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ↔ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))
182	181	elrab 3650	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ↔ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))
183	179, 182	anbi12i 637	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ↔ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))))
184		simprll 788	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → 𝑢 ∈ (𝑆 Cn 𝑇))
185		simprrl 790	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → 𝑣 ∈ (𝑅 Cn 𝑆))
186		coeq1 5827	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑢 → (𝑓 ∘ 𝑔) = (𝑢 ∘ 𝑔))
187		coeq2 5828	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑣 → (𝑢 ∘ 𝑔) = (𝑢 ∘ 𝑣))
188		xkococn.1	. . . . . . . . . . . . . . 15 ⊢ 𝐹 = (𝑓 ∈ (𝑆 Cn 𝑇), 𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝑓 ∘ 𝑔))
189		vex 3457	. . . . . . . . . . . . . . . 16 ⊢ 𝑢 ∈ V
190		vex 3457	. . . . . . . . . . . . . . . 16 ⊢ 𝑣 ∈ V
191	189, 190	coex 7907	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∘ 𝑣) ∈ V
192	186, 187, 188, 191	ovmpo 7552	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ 𝑣 ∈ (𝑅 Cn 𝑆)) → (𝑢𝐹𝑣) = (𝑢 ∘ 𝑣))
193	184, 185, 192	syl2anc 593	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢𝐹𝑣) = (𝑢 ∘ 𝑣))
194		imaeq1 6041	. . . . . . . . . . . . . . 15 ⊢ (ℎ = (𝑢 ∘ 𝑣) → (ℎ “ 𝐾) = ((𝑢 ∘ 𝑣) “ 𝐾))
195	194	sseq1d 3967	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑢 ∘ 𝑣) → ((ℎ “ 𝐾) ⊆ 𝑉 ↔ ((𝑢 ∘ 𝑣) “ 𝐾) ⊆ 𝑉))
196		cnco 23306	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ (𝑅 Cn 𝑆) ∧ 𝑢 ∈ (𝑆 Cn 𝑇)) → (𝑢 ∘ 𝑣) ∈ (𝑅 Cn 𝑇))
197	185, 184, 196	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 ∘ 𝑣) ∈ (𝑅 Cn 𝑇))
198		imaco 6234	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∘ 𝑣) “ 𝐾) = (𝑢 “ (𝑣 “ 𝐾))
199		simprrr 791	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
200	15	ntrss2 23097	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ Top ∧ (𝑘‘𝑦) ⊆ ∪ 𝑆) → ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦))
201	200	ex 416	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑆 ∈ Top → ((𝑘‘𝑦) ⊆ ∪ 𝑆 → ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦)))
202	201	ralimdv 3175	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ∈ Top → (∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦)))
203	88, 126, 202	sylc 65	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦))
204		ss2iun 4967	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦))
205	203, 204	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦))
206	205, 108	sseqtrd 3972	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ ran 𝑘)
207	206	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ ran 𝑘)
208	199, 207	sstrd 3946	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑣 “ 𝐾) ⊆ ∪ ran 𝑘)
209		imass2 6088	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 “ 𝐾) ⊆ ∪ ran 𝑘 → (𝑢 “ (𝑣 “ 𝐾)) ⊆ (𝑢 “ ∪ ran 𝑘))
210	208, 209	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ (𝑣 “ 𝐾)) ⊆ (𝑢 “ ∪ ran 𝑘))
211		simprlr 789	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉)
212	210, 211	sstrd 3946	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ (𝑣 “ 𝐾)) ⊆ 𝑉)
213	198, 212	eqsstrid 3974	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → ((𝑢 ∘ 𝑣) “ 𝐾) ⊆ 𝑉)
214	195, 197, 213	elrabd 3652	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 ∘ 𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
215	193, 214	eqeltrd 2861	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
216	183, 215	sylan2b 603	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) → (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
217	216	ralrimivva 3204	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
218	188	mpofun 7516	. . . . . . . . . . 11 ⊢ Fun 𝐹
219		ssrab2 4033	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇)
220		ssrab2 4033	. . . . . . . . . . . . 13 ⊢ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ⊆ (𝑅 Cn 𝑆)
221		xpss12 5660	. . . . . . . . . . . . 13 ⊢ (({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ⊆ (𝑅 Cn 𝑆)) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆)))
222	219, 220, 221	mp2an 702	. . . . . . . . . . . 12 ⊢ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))
223		vex 3457	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
224		vex 3457	. . . . . . . . . . . . . 14 ⊢ 𝑔 ∈ V
225	223, 224	coex 7907	. . . . . . . . . . . . 13 ⊢ (𝑓 ∘ 𝑔) ∈ V
226	188, 225	dmmpo 8048	. . . . . . . . . . . 12 ⊢ dom 𝐹 = ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))
227	222, 226	sseqtrri 3985	. . . . . . . . . . 11 ⊢ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹
228		funimassov 7569	. . . . . . . . . . 11 ⊢ ((Fun 𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))
229	218, 227, 228	mp2an 702	. . . . . . . . . 10 ⊢ ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
230	217, 229	sylibr 236	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
231		funimass3 7031	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))
232	218, 227, 231	mp2an 702	. . . . . . . . 9 ⊢ ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))
233	230, 232	sylib 220	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))
234		eleq2 2850	. . . . . . . . . 10 ⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → (⟨𝐴, 𝐵⟩ ∈ 𝑧 ↔ ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})))
235		sseq1 3961	. . . . . . . . . 10 ⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → (𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))
236	234, 235	anbi12d 641	. . . . . . . . 9 ⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → ((⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})) ↔ (⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
237	236	rspcev 3581	. . . . . . . 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 847	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))
239	238	expr 460	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ (𝐵 “ 𝐾) = ∪ 𝑤) → ((𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
240	239	exlimdv 1952	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ (𝐵 “ 𝐾) = ∪ 𝑤) → (∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
241	87, 240	syldan 600	. . . 4 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤) → (∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
242	241	expimpd 457	. . 3 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) → ((∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
243	242	rexlimdva 3162	. 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 208 ∧ wa 399 ∧ w3a 1097 = wceq 1559 ∃wex 1798 ∈ wcel 2141 ∀wral 3075 ∃wrex 3085 {crab 3413 Vcvv 3453 ∩ cin 3903 ⊆ wss 3904 𝒫 cpw 4554 ⟨cop 4587 ∪ cuni 4864 ∪ ciun 4948 × cxp 5643 ^◡ccnv 5644 dom cdm 5645 ran crn 5646 “ cima 5648 ∘ ccom 5649 Fun wfun 6511 Fn wfn 6512 ⟶wf 6513 ‘cfv 6517 (class class class)co 7392 ∈ cmpo 7394 Fincfn 8923 ↾_t crest 17432 Topctop 22933 intcnt 23057 Cn ccn 23264 Compccmp 23426 𝑛-Locally cnlly 23505 ×_t ctx 23600 ↑_ko cxko 23601

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5321 ax-pr 5389 ax-un 7714

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3076 df-rex 3086 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-int 4905 df-iun 4950 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5540 df-eprel 5545 df-po 5553 df-so 5554 df-fr 5598 df-we 5600 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-ord 6345 df-on 6346 df-lim 6347 df-suc 6348 df-iota 6473 df-fun 6519 df-fn 6520 df-f 6521 df-f1 6522 df-fo 6523 df-f1o 6524 df-fv 6525 df-ov 7395 df-oprab 7396 df-mpo 7397 df-om 7843 df-1st 7966 df-2nd 7967 df-1o 8432 df-map 8805 df-en 8924 df-dom 8925 df-fin 8927 df-fi 9354 df-rest 17434 df-topgen 17455 df-top 22934 df-topon 22951 df-bases 22986 df-ntr 23060 df-nei 23138 df-cn 23267 df-cmp 23427 df-nlly 23507 df-tx 23602 df-xko 23603

This theorem is referenced by: xkococn 23700

W3C validator