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 23634

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 23372	. . . 4 ⊢ ((𝐵 ∈ (𝑅 Cn 𝑆) ∧ (𝑅 ↾_t 𝐾) ∈ Comp) → (𝑆 ↾_t (𝐵 “ 𝐾)) ∈ Comp)
4	1, 2, 3	syl2anc 585	. . 3 ⊢ (𝜑 → (𝑆 ↾_t (𝐵 “ 𝐾)) ∈ Comp)
5		xkococn.s	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ 𝑛-Locally Comp)
6	5	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → 𝑆 ∈ 𝑛-Locally Comp)
7		xkococn.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ (𝑆 Cn 𝑇))
8		xkococn.v	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ 𝑇)
9		cnima 23240	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑆 Cn 𝑇) ∧ 𝑉 ∈ 𝑇) → (^◡𝐴 “ 𝑉) ∈ 𝑆)
10	7, 8, 9	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐴 “ 𝑉) ∈ 𝑆)
11	10	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → (^◡𝐴 “ 𝑉) ∈ 𝑆)
12		imaco 6209	. . . . . . . . . . 11 ⊢ ((𝐴 ∘ 𝐵) “ 𝐾) = (𝐴 “ (𝐵 “ 𝐾))
13		xkococn.i	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 ∘ 𝐵) “ 𝐾) ⊆ 𝑉)
14	12, 13	eqsstrrid 3962	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉)
15		eqid 2737	. . . . . . . . . . . . 13 ⊢ ∪ 𝑆 = ∪ 𝑆
16		eqid 2737	. . . . . . . . . . . . 13 ⊢ ∪ 𝑇 = ∪ 𝑇
17	15, 16	cnf 23221	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (𝑆 Cn 𝑇) → 𝐴:∪ 𝑆⟶∪ 𝑇)
18		ffun 6665	. . . . . . . . . . . 12 ⊢ (𝐴:∪ 𝑆⟶∪ 𝑇 → Fun 𝐴)
19	7, 17, 18	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → Fun 𝐴)
20		imassrn 6030	. . . . . . . . . . . . 13 ⊢ (𝐵 “ 𝐾) ⊆ ran 𝐵
21		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑅 = ∪ 𝑅
22	21, 15	cnf 23221	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → 𝐵:∪ 𝑅⟶∪ 𝑆)
23		frn 6669	. . . . . . . . . . . . . 14 ⊢ (𝐵:∪ 𝑅⟶∪ 𝑆 → ran 𝐵 ⊆ ∪ 𝑆)
24	1, 22, 23	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐵 ⊆ ∪ 𝑆)
25	20, 24	sstrid 3934	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ ∪ 𝑆)
26		fdm 6671	. . . . . . . . . . . . 13 ⊢ (𝐴:∪ 𝑆⟶∪ 𝑇 → dom 𝐴 = ∪ 𝑆)
27	7, 17, 26	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → dom 𝐴 = ∪ 𝑆)
28	25, 27	sseqtrrd 3960	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ dom 𝐴)
29		funimass3 7000	. . . . . . . . . . 11 ⊢ ((Fun 𝐴 ∧ (𝐵 “ 𝐾) ⊆ dom 𝐴) → ((𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉 ↔ (𝐵 “ 𝐾) ⊆ (^◡𝐴 “ 𝑉)))
30	19, 28, 29	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉 ↔ (𝐵 “ 𝐾) ⊆ (^◡𝐴 “ 𝑉)))
31	14, 30	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ (^◡𝐴 “ 𝑉))
32	31	sselda 3922	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → 𝑥 ∈ (^◡𝐴 “ 𝑉))
33		nlly2i 23451	. . . . . . . 8 ⊢ ((𝑆 ∈ 𝑛-Locally Comp ∧ (^◡𝐴 “ 𝑉) ∈ 𝑆 ∧ 𝑥 ∈ (^◡𝐴 “ 𝑉)) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))
34	6, 11, 32, 33	syl3anc 1374	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))
35		nllytop 23448	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ 𝑛-Locally Comp → 𝑆 ∈ Top)
36	5, 35	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ Top)
37	36	ad3antrrr 731	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
38		imaexg 7857	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → (𝐵 “ 𝐾) ∈ V)
39	1, 38	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 “ 𝐾) ∈ V)
40	39	ad3antrrr 731	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝐵 “ 𝐾) ∈ V)
41		simprl 771	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑢 ∈ 𝑆)
42		elrestr 17382	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Top ∧ (𝐵 “ 𝐾) ∈ V ∧ 𝑢 ∈ 𝑆) → (𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾_t (𝐵 “ 𝐾)))
43	37, 40, 41, 42	syl3anc 1374	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾_t (𝐵 “ 𝐾)))
44		simprr1 1223	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑥 ∈ 𝑢)
45		simpllr 776	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝐵 “ 𝐾))
46	44, 45	elind 4141	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)))
47		inss1 4178	. . . . . . . . . . . 12 ⊢ (𝑢 ∩ (𝐵 “ 𝐾)) ⊆ 𝑢
48		elpwi 4549	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉) → 𝑠 ⊆ (^◡𝐴 “ 𝑉))
49	48	ad2antlr 728	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑠 ⊆ (^◡𝐴 “ 𝑉))
50		elssuni 4882	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐴 “ 𝑉) ∈ 𝑆 → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
51	10, 50	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
52	51	ad3antrrr 731	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
53	49, 52	sstrd 3933	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑠 ⊆ ∪ 𝑆)
54		simprr2 1224	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑢 ⊆ 𝑠)
55	15	ssntr 23033	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ Top ∧ 𝑠 ⊆ ∪ 𝑆) ∧ (𝑢 ∈ 𝑆 ∧ 𝑢 ⊆ 𝑠)) → 𝑢 ⊆ ((int‘𝑆)‘𝑠))
56	37, 53, 41, 54, 55	syl22anc 839	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑢 ⊆ ((int‘𝑆)‘𝑠))
57	47, 56	sstrid 3934	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠))
58		simprr3 1225	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝑆 ↾_t 𝑠) ∈ Comp)
59	57, 58	jca 511	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))
60		eleq2 2826	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾))))
61		cleq1lem 14935	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp) ↔ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
62	60, 61	anbi12d 633	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → ((𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ (𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)) ∧ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))))
63	62	rspcev 3565	. . . . . . . . . 10 ⊢ (((𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾_t (𝐵 “ 𝐾)) ∧ (𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)) ∧ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
64	43, 46, 59, 63	syl12anc 837	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
65	64	rexlimdvaa 3140	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) → (∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))))
66	65	reximdva 3151	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))))
67	34, 66	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
68		rexcom 3267	. . . . . . 7 ⊢ (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
69		r19.42v 3170	. . . . . . . 8 ⊢ (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ (𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
70	69	rexbii 3085	. . . . . . 7 ⊢ (∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
71	68, 70	bitri 275	. . . . . 6 ⊢ (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
72	67, 71	sylib 218	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
73	72	ralrimiva 3130	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ (𝐵 “ 𝐾)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
74	15	restuni 23137	. . . . 5 ⊢ ((𝑆 ∈ Top ∧ (𝐵 “ 𝐾) ⊆ ∪ 𝑆) → (𝐵 “ 𝐾) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾)))
75	36, 25, 74	syl2anc 585	. . . 4 ⊢ (𝜑 → (𝐵 “ 𝐾) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾)))
76	73, 75	raleqtrdv 3298	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ∪ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
77		eqid 2737	. . . 4 ⊢ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾))
78		fveq2 6834	. . . . . 6 ⊢ (𝑠 = (𝑘‘𝑦) → ((int‘𝑆)‘𝑠) = ((int‘𝑆)‘(𝑘‘𝑦)))
79	78	sseq2d 3955	. . . . 5 ⊢ (𝑠 = (𝑘‘𝑦) → (𝑦 ⊆ ((int‘𝑆)‘𝑠) ↔ 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦))))
80		oveq2 7368	. . . . . 6 ⊢ (𝑠 = (𝑘‘𝑦) → (𝑆 ↾_t 𝑠) = (𝑆 ↾_t (𝑘‘𝑦)))
81	80	eleq1d 2822	. . . . 5 ⊢ (𝑠 = (𝑘‘𝑦) → ((𝑆 ↾_t 𝑠) ∈ Comp ↔ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))
82	79, 81	anbi12d 633	. . . 4 ⊢ (𝑠 = (𝑘‘𝑦) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp) ↔ (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))
83	77, 82	cmpcovf 23366	. . 3 ⊢ (((𝑆 ↾_t (𝐵 “ 𝐾)) ∈ Comp ∧ ∀𝑥 ∈ ∪ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ∃𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)(∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))))
84	4, 76, 83	syl2anc 585	. 2 ⊢ (𝜑 → ∃𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)(∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))))
85	75	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) → (𝐵 “ 𝐾) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾)))
86	85	eqeq1d 2739	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) → ((𝐵 “ 𝐾) = ∪ 𝑤 ↔ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤))
87	86	biimpar 477	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤) → (𝐵 “ 𝐾) = ∪ 𝑤)
88	36	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑆 ∈ Top)
89		cntop2 23216	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (𝑆 Cn 𝑇) → 𝑇 ∈ Top)
90	7, 89	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ Top)
91	90	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑇 ∈ Top)
92		xkotop 23563	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ↑_ko 𝑆) ∈ Top)
93	88, 91, 92	syl2anc 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑇 ↑_ko 𝑆) ∈ Top)
94		cntop1 23215	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → 𝑅 ∈ Top)
95	1, 94	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ Top)
96	95	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑅 ∈ Top)
97		xkotop 23563	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑_ko 𝑅) ∈ Top)
98	96, 88, 97	syl2anc 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↑_ko 𝑅) ∈ Top)
99		simprrl 781	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉))
100	99	frnd 6670	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ran 𝑘 ⊆ 𝒫 (^◡𝐴 “ 𝑉))
101		sspwuni 5043	. . . . . . . . . . . 12 ⊢ (ran 𝑘 ⊆ 𝒫 (^◡𝐴 “ 𝑉) ↔ ∪ ran 𝑘 ⊆ (^◡𝐴 “ 𝑉))
102	100, 101	sylib 218	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ (^◡𝐴 “ 𝑉))
103	10	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (^◡𝐴 “ 𝑉) ∈ 𝑆)
104	103, 50	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
105	102, 104	sstrd 3933	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ ∪ 𝑆)
106		ffn 6662	. . . . . . . . . . . . 13 ⊢ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) → 𝑘 Fn 𝑤)
107		fniunfv 7195	. . . . . . . . . . . . 13 ⊢ (𝑘 Fn 𝑤 → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘)
108	99, 106, 107	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘)
109	108	oveq2d 7376	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾_t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = (𝑆 ↾_t ∪ ran 𝑘))
110		simplr 769	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin))
111	110	elin2d 4146	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑤 ∈ Fin)
112		simprrr 782	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))
113		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)
114	113	ralimi 3075	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → ∀𝑦 ∈ 𝑤 (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)
115	112, 114	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)
116	15	fiuncmp 23379	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Top ∧ 𝑤 ∈ Fin ∧ ∀𝑦 ∈ 𝑤 (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → (𝑆 ↾_t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) ∈ Comp)
117	88, 111, 115, 116	syl3anc 1374	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾_t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) ∈ Comp)
118	109, 117	eqeltrrd 2838	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾_t ∪ ran 𝑘) ∈ Comp)
119	8	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑉 ∈ 𝑇)
120	15, 88, 91, 105, 118, 119	xkoopn 23564	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∈ (𝑇 ↑_ko 𝑆))
121		xkococn.k	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ⊆ ∪ 𝑅)
122	121	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐾 ⊆ ∪ 𝑅)
123	2	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑅 ↾_t 𝐾) ∈ Comp)
124	108, 105	eqsstrd 3957	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆)
125		iunss 4988	. . . . . . . . . . . . 13 ⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆)
126	124, 125	sylib 218	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆)
127	15	ntropn 23024	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ Top ∧ (𝑘‘𝑦) ⊆ ∪ 𝑆) → ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
128	127	ex 412	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Top → ((𝑘‘𝑦) ⊆ ∪ 𝑆 → ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆))
129	128	ralimdv 3152	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ Top → (∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆))
130	88, 126, 129	sylc 65	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
131		iunopn 22873	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Top ∧ ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
132	88, 130, 131	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
133	21, 96, 88, 122, 123, 132	xkoopn 23564	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ∈ (𝑆 ↑_ko 𝑅))
134		txopn 23577	. . . . . . . . 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 839	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)))
136		imaeq1 6014	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝑎 “ ∪ ran 𝑘) = (𝐴 “ ∪ ran 𝑘))
137	136	sseq1d 3954	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((𝑎 “ ∪ ran 𝑘) ⊆ 𝑉 ↔ (𝐴 “ ∪ ran 𝑘) ⊆ 𝑉))
138	7	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐴 ∈ (𝑆 Cn 𝑇))
139		imaiun 7193	. . . . . . . . . . . 12 ⊢ (𝐴 “ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦))
140	108	imaeq2d 6019	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐴 “ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = (𝐴 “ ∪ ran 𝑘))
141	139, 140	eqtr3id 2786	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) = (𝐴 “ ∪ ran 𝑘))
142	108, 102	eqsstrd 3957	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉))
143	19	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → Fun 𝐴)
144	99, 106	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑘 Fn 𝑤)
145	27	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → dom 𝐴 = ∪ 𝑆)
146	105, 145	sseqtrrd 3960	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ dom 𝐴)
147		simpl1 1193	. . . . . . . . . . . . . . . 16 ⊢ (((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → Fun 𝐴)
148	107	3ad2ant2 1135	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘)
149		simp3 1139	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪ ran 𝑘 ⊆ dom 𝐴)
150	148, 149	eqsstrd 3957	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴)
151		iunss 4988	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴)
152	150, 151	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴)
153	152	r19.21bi 3230	. . . . . . . . . . . . . . . 16 ⊢ (((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → (𝑘‘𝑦) ⊆ dom 𝐴)
154		funimass3 7000	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐴 ∧ (𝑘‘𝑦) ⊆ dom 𝐴) → ((𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
155	147, 153, 154	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → ((𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
156	155	ralbidva 3159	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → (∀𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
157		iunss 4988	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∀𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉)
158		iunss 4988	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉) ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉))
159	156, 157, 158	3bitr4g 314	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
160	143, 144, 146, 159	syl3anc 1374	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
161	142, 160	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉)
162	141, 161	eqsstrrd 3958	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐴 “ ∪ ran 𝑘) ⊆ 𝑉)
163	137, 138, 162	elrabd 3637	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐴 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉})
164		imaeq1 6014	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝑏 “ 𝐾) = (𝐵 “ 𝐾))
165	164	sseq1d 3954	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ↔ (𝐵 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))
166	1	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐵 ∈ (𝑅 Cn 𝑆))
167		simprl 771	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) = ∪ 𝑤)
168		uniiun 5002	. . . . . . . . . . . 12 ⊢ ∪ 𝑤 = ∪ 𝑦 ∈ 𝑤 𝑦
169	167, 168	eqtrdi 2788	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) = ∪ 𝑦 ∈ 𝑤 𝑦)
170		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)))
171	170	ralimi 3075	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → ∀𝑦 ∈ 𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)))
172		ss2iun 4953	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) → ∪ 𝑦 ∈ 𝑤 𝑦 ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
173	112, 171, 172	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 𝑦 ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
174	169, 173	eqsstrd 3957	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
175	165, 166, 174	elrabd 3637	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐵 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})
176	163, 175	opelxpd 5663	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}))
177		imaeq1 6014	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑢 → (𝑎 “ ∪ ran 𝑘) = (𝑢 “ ∪ ran 𝑘))
178	177	sseq1d 3954	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑢 → ((𝑎 “ ∪ ran 𝑘) ⊆ 𝑉 ↔ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉))
179	178	elrab 3635	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ↔ (𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉))
180		imaeq1 6014	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑣 → (𝑏 “ 𝐾) = (𝑣 “ 𝐾))
181	180	sseq1d 3954	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑣 → ((𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ↔ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))
182	181	elrab 3635	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ↔ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))
183	179, 182	anbi12i 629	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ↔ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))))
184		simprll 779	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → 𝑢 ∈ (𝑆 Cn 𝑇))
185		simprrl 781	. . . . . . . . . . . . . 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 3434	. . . . . . . . . . . . . . . 16 ⊢ 𝑢 ∈ V
190		vex 3434	. . . . . . . . . . . . . . . 16 ⊢ 𝑣 ∈ V
191	189, 190	coex 7874	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∘ 𝑣) ∈ V
192	186, 187, 188, 191	ovmpo 7520	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ 𝑣 ∈ (𝑅 Cn 𝑆)) → (𝑢𝐹𝑣) = (𝑢 ∘ 𝑣))
193	184, 185, 192	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢𝐹𝑣) = (𝑢 ∘ 𝑣))
194		imaeq1 6014	. . . . . . . . . . . . . . 15 ⊢ (ℎ = (𝑢 ∘ 𝑣) → (ℎ “ 𝐾) = ((𝑢 ∘ 𝑣) “ 𝐾))
195	194	sseq1d 3954	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑢 ∘ 𝑣) → ((ℎ “ 𝐾) ⊆ 𝑉 ↔ ((𝑢 ∘ 𝑣) “ 𝐾) ⊆ 𝑉))
196		cnco 23241	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ (𝑅 Cn 𝑆) ∧ 𝑢 ∈ (𝑆 Cn 𝑇)) → (𝑢 ∘ 𝑣) ∈ (𝑅 Cn 𝑇))
197	185, 184, 196	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 ∘ 𝑣) ∈ (𝑅 Cn 𝑇))
198		imaco 6209	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∘ 𝑣) “ 𝐾) = (𝑢 “ (𝑣 “ 𝐾))
199		simprrr 782	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
200	15	ntrss2 23032	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ Top ∧ (𝑘‘𝑦) ⊆ ∪ 𝑆) → ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦))
201	200	ex 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑆 ∈ Top → ((𝑘‘𝑦) ⊆ ∪ 𝑆 → ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦)))
202	201	ralimdv 3152	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ∈ Top → (∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦)))
203	88, 126, 202	sylc 65	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦))
204		ss2iun 4953	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦))
205	203, 204	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦))
206	205, 108	sseqtrd 3959	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ ran 𝑘)
207	206	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ ran 𝑘)
208	199, 207	sstrd 3933	. . . . . . . . . . . . . . . . 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 780	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉)
212	210, 211	sstrd 3933	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ (𝑣 “ 𝐾)) ⊆ 𝑉)
213	198, 212	eqsstrid 3961	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → ((𝑢 ∘ 𝑣) “ 𝐾) ⊆ 𝑉)
214	195, 197, 213	elrabd 3637	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 ∘ 𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
215	193, 214	eqeltrd 2837	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
216	183, 215	sylan2b 595	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) → (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
217	216	ralrimivva 3181	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
218	188	mpofun 7484	. . . . . . . . . . 11 ⊢ Fun 𝐹
219		ssrab2 4021	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇)
220		ssrab2 4021	. . . . . . . . . . . . 13 ⊢ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ⊆ (𝑅 Cn 𝑆)
221		xpss12 5639	. . . . . . . . . . . . 13 ⊢ (({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ⊆ (𝑅 Cn 𝑆)) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆)))
222	219, 220, 221	mp2an 693	. . . . . . . . . . . 12 ⊢ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))
223		vex 3434	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
224		vex 3434	. . . . . . . . . . . . . 14 ⊢ 𝑔 ∈ V
225	223, 224	coex 7874	. . . . . . . . . . . . 13 ⊢ (𝑓 ∘ 𝑔) ∈ V
226	188, 225	dmmpo 8017	. . . . . . . . . . . 12 ⊢ dom 𝐹 = ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))
227	222, 226	sseqtrri 3972	. . . . . . . . . . 11 ⊢ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹
228		funimassov 7537	. . . . . . . . . . 11 ⊢ ((Fun 𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))
229	218, 227, 228	mp2an 693	. . . . . . . . . 10 ⊢ ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
230	217, 229	sylibr 234	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
231		funimass3 7000	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))
232	218, 227, 231	mp2an 693	. . . . . . . . 9 ⊢ ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))
233	230, 232	sylib 218	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))
234		eleq2 2826	. . . . . . . . . 10 ⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → (⟨𝐴, 𝐵⟩ ∈ 𝑧 ↔ ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})))
235		sseq1 3948	. . . . . . . . . 10 ⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → (𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))
236	234, 235	anbi12d 633	. . . . . . . . 9 ⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → ((⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})) ↔ (⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
237	236	rspcev 3565	. . . . . . . 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 837	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))
239	238	expr 456	. . . . . 6 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ (𝐵 “ 𝐾) = ∪ 𝑤) → ((𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
240	239	exlimdv 1935	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ (𝐵 “ 𝐾) = ∪ 𝑤) → (∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
241	87, 240	syldan 592	. . . 4 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤) → (∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
242	241	expimpd 453	. . 3 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) → ((∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
243	242	rexlimdva 3139	. 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 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ∀wral 3052 ∃wrex 3062 {crab 3390 Vcvv 3430 ∩ cin 3889 ⊆ wss 3890 𝒫 cpw 4542 ⟨cop 4574 ∪ cuni 4851 ∪ ciun 4934 × cxp 5622 ^◡ccnv 5623 dom cdm 5624 ran crn 5625 “ cima 5627 ∘ ccom 5628 Fun wfun 6486 Fn wfn 6487 ⟶wf 6488 ‘cfv 6492 (class class class)co 7360 ∈ cmpo 7362 Fincfn 8886 ↾_t crest 17374 Topctop 22868 intcnt 22992 Cn ccn 23199 Compccmp 23361 𝑛-Locally cnlly 23440 ×_t ctx 23535 ↑_ko cxko 23536

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 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 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-1o 8398 df-map 8768 df-en 8887 df-dom 8888 df-fin 8890 df-fi 9317 df-rest 17376 df-topgen 17397 df-top 22869 df-topon 22886 df-bases 22921 df-ntr 22995 df-nei 23073 df-cn 23202 df-cmp 23362 df-nlly 23442 df-tx 23537 df-xko 23538

This theorem is referenced by: xkococn 23635

W3C validator