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 23602

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 23340	. . . 4 ⊢ ((𝐵 ∈ (𝑅 Cn 𝑆) ∧ (𝑅 ↾_t 𝐾) ∈ Comp) → (𝑆 ↾_t (𝐵 “ 𝐾)) ∈ Comp)
4	1, 2, 3	syl2anc 584	. . 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 23208	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝑆 Cn 𝑇) ∧ 𝑉 ∈ 𝑇) → (^◡𝐴 “ 𝑉) ∈ 𝑆)
10	7, 8, 9	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐴 “ 𝑉) ∈ 𝑆)
11	10	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → (^◡𝐴 “ 𝑉) ∈ 𝑆)
12		imaco 6245	. . . . . . . . . . 11 ⊢ ((𝐴 ∘ 𝐵) “ 𝐾) = (𝐴 “ (𝐵 “ 𝐾))
13		xkococn.i	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 ∘ 𝐵) “ 𝐾) ⊆ 𝑉)
14	12, 13	eqsstrrid 4003	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉)
15		eqid 2736	. . . . . . . . . . . . 13 ⊢ ∪ 𝑆 = ∪ 𝑆
16		eqid 2736	. . . . . . . . . . . . 13 ⊢ ∪ 𝑇 = ∪ 𝑇
17	15, 16	cnf 23189	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (𝑆 Cn 𝑇) → 𝐴:∪ 𝑆⟶∪ 𝑇)
18		ffun 6714	. . . . . . . . . . . 12 ⊢ (𝐴:∪ 𝑆⟶∪ 𝑇 → Fun 𝐴)
19	7, 17, 18	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → Fun 𝐴)
20		imassrn 6063	. . . . . . . . . . . . 13 ⊢ (𝐵 “ 𝐾) ⊆ ran 𝐵
21		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑅 = ∪ 𝑅
22	21, 15	cnf 23189	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → 𝐵:∪ 𝑅⟶∪ 𝑆)
23		frn 6718	. . . . . . . . . . . . . 14 ⊢ (𝐵:∪ 𝑅⟶∪ 𝑆 → ran 𝐵 ⊆ ∪ 𝑆)
24	1, 22, 23	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ran 𝐵 ⊆ ∪ 𝑆)
25	20, 24	sstrid 3975	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ ∪ 𝑆)
26		fdm 6720	. . . . . . . . . . . . 13 ⊢ (𝐴:∪ 𝑆⟶∪ 𝑇 → dom 𝐴 = ∪ 𝑆)
27	7, 17, 26	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → dom 𝐴 = ∪ 𝑆)
28	25, 27	sseqtrrd 4001	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ dom 𝐴)
29		funimass3 7049	. . . . . . . . . . 11 ⊢ ((Fun 𝐴 ∧ (𝐵 “ 𝐾) ⊆ dom 𝐴) → ((𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉 ↔ (𝐵 “ 𝐾) ⊆ (^◡𝐴 “ 𝑉)))
30	19, 28, 29	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 “ (𝐵 “ 𝐾)) ⊆ 𝑉 ↔ (𝐵 “ 𝐾) ⊆ (^◡𝐴 “ 𝑉)))
31	14, 30	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 “ 𝐾) ⊆ (^◡𝐴 “ 𝑉))
32	31	sselda 3963	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → 𝑥 ∈ (^◡𝐴 “ 𝑉))
33		nlly2i 23419	. . . . . . . 8 ⊢ ((𝑆 ∈ 𝑛-Locally Comp ∧ (^◡𝐴 “ 𝑉) ∈ 𝑆 ∧ 𝑥 ∈ (^◡𝐴 “ 𝑉)) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))
34	6, 11, 32, 33	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))
35		nllytop 23416	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ 𝑛-Locally Comp → 𝑆 ∈ Top)
36	5, 35	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ Top)
37	36	ad3antrrr 730	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑆 ∈ Top)
38		imaexg 7914	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → (𝐵 “ 𝐾) ∈ V)
39	1, 38	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵 “ 𝐾) ∈ V)
40	39	ad3antrrr 730	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝐵 “ 𝐾) ∈ V)
41		simprl 770	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑢 ∈ 𝑆)
42		elrestr 17447	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Top ∧ (𝐵 “ 𝐾) ∈ V ∧ 𝑢 ∈ 𝑆) → (𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾_t (𝐵 “ 𝐾)))
43	37, 40, 41, 42	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾_t (𝐵 “ 𝐾)))
44		simprr1 1222	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑥 ∈ 𝑢)
45		simpllr 775	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝐵 “ 𝐾))
46	44, 45	elind 4180	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)))
47		inss1 4217	. . . . . . . . . . . 12 ⊢ (𝑢 ∩ (𝐵 “ 𝐾)) ⊆ 𝑢
48		elpwi 4587	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉) → 𝑠 ⊆ (^◡𝐴 “ 𝑉))
49	48	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑠 ⊆ (^◡𝐴 “ 𝑉))
50		elssuni 4918	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝐴 “ 𝑉) ∈ 𝑆 → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
51	10, 50	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
52	51	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
53	49, 52	sstrd 3974	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑠 ⊆ ∪ 𝑆)
54		simprr2 1223	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑢 ⊆ 𝑠)
55	15	ssntr 23001	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ Top ∧ 𝑠 ⊆ ∪ 𝑆) ∧ (𝑢 ∈ 𝑆 ∧ 𝑢 ⊆ 𝑠)) → 𝑢 ⊆ ((int‘𝑆)‘𝑠))
56	37, 53, 41, 54, 55	syl22anc 838	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → 𝑢 ⊆ ((int‘𝑆)‘𝑠))
57	47, 56	sstrid 3975	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠))
58		simprr3 1224	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → (𝑆 ↾_t 𝑠) ∈ Comp)
59	57, 58	jca 511	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))
60		eleq2 2824	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾))))
61		cleq1lem 15006	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp) ↔ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
62	60, 61	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑢 ∩ (𝐵 “ 𝐾)) → ((𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ (𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)) ∧ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))))
63	62	rspcev 3606	. . . . . . . . . 10 ⊢ (((𝑢 ∩ (𝐵 “ 𝐾)) ∈ (𝑆 ↾_t (𝐵 “ 𝐾)) ∧ (𝑥 ∈ (𝑢 ∩ (𝐵 “ 𝐾)) ∧ ((𝑢 ∩ (𝐵 “ 𝐾)) ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
64	43, 46, 59, 63	syl12anc 836	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) ∧ (𝑢 ∈ 𝑆 ∧ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
65	64	rexlimdvaa 3143	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) ∧ 𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)) → (∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp) → ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))))
66	65	reximdva 3154	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑢 ∈ 𝑆 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝑆 ↾_t 𝑠) ∈ Comp) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))))
67	34, 66	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 “ 𝐾)) → ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
68		rexcom 3275	. . . . . . 7 ⊢ (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ ∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
69		r19.42v 3177	. . . . . . . 8 ⊢ (∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑥 ∈ 𝑦 ∧ (𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)) ↔ (𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
70	69	rexbii 3084	. . . . . . 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 3133	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ (𝐵 “ 𝐾)∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
74	15	restuni 23105	. . . . 5 ⊢ ((𝑆 ∈ Top ∧ (𝐵 “ 𝐾) ⊆ ∪ 𝑆) → (𝐵 “ 𝐾) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾)))
75	36, 25, 74	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝐵 “ 𝐾) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾)))
76	73, 75	raleqtrdv 3311	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ∪ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp)))
77		eqid 2736	. . . 4 ⊢ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾))
78		fveq2 6881	. . . . . 6 ⊢ (𝑠 = (𝑘‘𝑦) → ((int‘𝑆)‘𝑠) = ((int‘𝑆)‘(𝑘‘𝑦)))
79	78	sseq2d 3996	. . . . 5 ⊢ (𝑠 = (𝑘‘𝑦) → (𝑦 ⊆ ((int‘𝑆)‘𝑠) ↔ 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦))))
80		oveq2 7418	. . . . . 6 ⊢ (𝑠 = (𝑘‘𝑦) → (𝑆 ↾_t 𝑠) = (𝑆 ↾_t (𝑘‘𝑦)))
81	80	eleq1d 2820	. . . . 5 ⊢ (𝑠 = (𝑘‘𝑦) → ((𝑆 ↾_t 𝑠) ∈ Comp ↔ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))
82	79, 81	anbi12d 632	. . . 4 ⊢ (𝑠 = (𝑘‘𝑦) → ((𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp) ↔ (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))
83	77, 82	cmpcovf 23334	. . 3 ⊢ (((𝑆 ↾_t (𝐵 “ 𝐾)) ∈ Comp ∧ ∀𝑥 ∈ ∪ (𝑆 ↾_t (𝐵 “ 𝐾))∃𝑦 ∈ (𝑆 ↾_t (𝐵 “ 𝐾))(𝑥 ∈ 𝑦 ∧ ∃𝑠 ∈ 𝒫 (^◡𝐴 “ 𝑉)(𝑦 ⊆ ((int‘𝑆)‘𝑠) ∧ (𝑆 ↾_t 𝑠) ∈ Comp))) → ∃𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)(∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))))
84	4, 76, 83	syl2anc 584	. 2 ⊢ (𝜑 → ∃𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)(∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤 ∧ ∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))))
85	75	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) → (𝐵 “ 𝐾) = ∪ (𝑆 ↾_t (𝐵 “ 𝐾)))
86	85	eqeq1d 2738	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) → ((𝐵 “ 𝐾) = ∪ 𝑤 ↔ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤))
87	86	biimpar 477	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ∪ (𝑆 ↾_t (𝐵 “ 𝐾)) = ∪ 𝑤) → (𝐵 “ 𝐾) = ∪ 𝑤)
88	36	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑆 ∈ Top)
89		cntop2 23184	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ (𝑆 Cn 𝑇) → 𝑇 ∈ Top)
90	7, 89	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ Top)
91	90	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑇 ∈ Top)
92		xkotop 23531	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ↑_ko 𝑆) ∈ Top)
93	88, 91, 92	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑇 ↑_ko 𝑆) ∈ Top)
94		cntop1 23183	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ (𝑅 Cn 𝑆) → 𝑅 ∈ Top)
95	1, 94	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ Top)
96	95	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑅 ∈ Top)
97		xkotop 23531	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑_ko 𝑅) ∈ Top)
98	96, 88, 97	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↑_ko 𝑅) ∈ Top)
99		simprrl 780	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉))
100	99	frnd 6719	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ran 𝑘 ⊆ 𝒫 (^◡𝐴 “ 𝑉))
101		sspwuni 5081	. . . . . . . . . . . 12 ⊢ (ran 𝑘 ⊆ 𝒫 (^◡𝐴 “ 𝑉) ↔ ∪ ran 𝑘 ⊆ (^◡𝐴 “ 𝑉))
102	100, 101	sylib 218	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ (^◡𝐴 “ 𝑉))
103	10	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (^◡𝐴 “ 𝑉) ∈ 𝑆)
104	103, 50	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (^◡𝐴 “ 𝑉) ⊆ ∪ 𝑆)
105	102, 104	sstrd 3974	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ ∪ 𝑆)
106		ffn 6711	. . . . . . . . . . . . 13 ⊢ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) → 𝑘 Fn 𝑤)
107		fniunfv 7244	. . . . . . . . . . . . 13 ⊢ (𝑘 Fn 𝑤 → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘)
108	99, 106, 107	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘)
109	108	oveq2d 7426	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾_t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = (𝑆 ↾_t ∪ ran 𝑘))
110		simplr 768	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin))
111	110	elin2d 4185	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑤 ∈ Fin)
112		simprrr 781	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp))
113		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)
114	113	ralimi 3074	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → ∀𝑦 ∈ 𝑤 (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)
115	112, 114	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)
116	15	fiuncmp 23347	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Top ∧ 𝑤 ∈ Fin ∧ ∀𝑦 ∈ 𝑤 (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → (𝑆 ↾_t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) ∈ Comp)
117	88, 111, 115, 116	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾_t ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) ∈ Comp)
118	109, 117	eqeltrrd 2836	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑆 ↾_t ∪ ran 𝑘) ∈ Comp)
119	8	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑉 ∈ 𝑇)
120	15, 88, 91, 105, 118, 119	xkoopn 23532	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∈ (𝑇 ↑_ko 𝑆))
121		xkococn.k	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ⊆ ∪ 𝑅)
122	121	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐾 ⊆ ∪ 𝑅)
123	2	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝑅 ↾_t 𝐾) ∈ Comp)
124	108, 105	eqsstrd 3998	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆)
125		iunss 5026	. . . . . . . . . . . . 13 ⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆)
126	124, 125	sylib 218	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆)
127	15	ntropn 22992	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ Top ∧ (𝑘‘𝑦) ⊆ ∪ 𝑆) → ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
128	127	ex 412	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ Top → ((𝑘‘𝑦) ⊆ ∪ 𝑆 → ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆))
129	128	ralimdv 3155	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ Top → (∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆))
130	88, 126, 129	sylc 65	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
131		iunopn 22841	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ Top ∧ ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
132	88, 130, 131	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ∈ 𝑆)
133	21, 96, 88, 122, 123, 132	xkoopn 23532	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ∈ (𝑆 ↑_ko 𝑅))
134		txopn 23545	. . . . . . . . 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 838	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅)))
136		imaeq1 6047	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝑎 “ ∪ ran 𝑘) = (𝐴 “ ∪ ran 𝑘))
137	136	sseq1d 3995	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((𝑎 “ ∪ ran 𝑘) ⊆ 𝑉 ↔ (𝐴 “ ∪ ran 𝑘) ⊆ 𝑉))
138	7	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐴 ∈ (𝑆 Cn 𝑇))
139		imaiun 7242	. . . . . . . . . . . 12 ⊢ (𝐴 “ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦))
140	108	imaeq2d 6052	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐴 “ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦)) = (𝐴 “ ∪ ran 𝑘))
141	139, 140	eqtr3id 2785	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) = (𝐴 “ ∪ ran 𝑘))
142	108, 102	eqsstrd 3998	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉))
143	19	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → Fun 𝐴)
144	99, 106	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝑘 Fn 𝑤)
145	27	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → dom 𝐴 = ∪ 𝑆)
146	105, 145	sseqtrrd 4001	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ ran 𝑘 ⊆ dom 𝐴)
147		simpl1 1192	. . . . . . . . . . . . . . . 16 ⊢ (((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → Fun 𝐴)
148	107	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) = ∪ ran 𝑘)
149		simp3 1138	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪ ran 𝑘 ⊆ dom 𝐴)
150	148, 149	eqsstrd 3998	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴)
151		iunss 5026	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴)
152	150, 151	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ dom 𝐴)
153	152	r19.21bi 3238	. . . . . . . . . . . . . . . 16 ⊢ (((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → (𝑘‘𝑦) ⊆ dom 𝐴)
154		funimass3 7049	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐴 ∧ (𝑘‘𝑦) ⊆ dom 𝐴) → ((𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
155	147, 153, 154	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) ∧ 𝑦 ∈ 𝑤) → ((𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
156	155	ralbidva 3162	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → (∀𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
157		iunss 5026	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∀𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉)
158		iunss 5026	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉) ↔ ∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉))
159	156, 157, 158	3bitr4g 314	. . . . . . . . . . . . 13 ⊢ ((Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴) → (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
160	143, 144, 146, 159	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉 ↔ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ (^◡𝐴 “ 𝑉)))
161	142, 160	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 (𝐴 “ (𝑘‘𝑦)) ⊆ 𝑉)
162	141, 161	eqsstrrd 3999	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐴 “ ∪ ran 𝑘) ⊆ 𝑉)
163	137, 138, 162	elrabd 3678	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐴 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉})
164		imaeq1 6047	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (𝑏 “ 𝐾) = (𝐵 “ 𝐾))
165	164	sseq1d 3995	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ↔ (𝐵 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))
166	1	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐵 ∈ (𝑅 Cn 𝑆))
167		simprl 770	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) = ∪ 𝑤)
168		uniiun 5039	. . . . . . . . . . . 12 ⊢ ∪ 𝑤 = ∪ 𝑦 ∈ 𝑤 𝑦
169	167, 168	eqtrdi 2787	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) = ∪ 𝑦 ∈ 𝑤 𝑦)
170		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)))
171	170	ralimi 3074	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp) → ∀𝑦 ∈ 𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)))
172		ss2iun 4991	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ 𝑤 𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) → ∪ 𝑦 ∈ 𝑤 𝑦 ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
173	112, 171, 172	3syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 𝑦 ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
174	169, 173	eqsstrd 3998	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → (𝐵 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
175	165, 166, 174	elrabd 3678	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → 𝐵 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})
176	163, 175	opelxpd 5698	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}))
177		imaeq1 6047	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑢 → (𝑎 “ ∪ ran 𝑘) = (𝑢 “ ∪ ran 𝑘))
178	177	sseq1d 3995	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑢 → ((𝑎 “ ∪ ran 𝑘) ⊆ 𝑉 ↔ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉))
179	178	elrab 3676	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ↔ (𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉))
180		imaeq1 6047	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑣 → (𝑏 “ 𝐾) = (𝑣 “ 𝐾))
181	180	sseq1d 3995	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑣 → ((𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ↔ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))
182	181	elrab 3676	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ↔ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))
183	179, 182	anbi12i 628	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ↔ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))))
184		simprll 778	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → 𝑢 ∈ (𝑆 Cn 𝑇))
185		simprrl 780	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → 𝑣 ∈ (𝑅 Cn 𝑆))
186		coeq1 5842	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑢 → (𝑓 ∘ 𝑔) = (𝑢 ∘ 𝑔))
187		coeq2 5843	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = 𝑣 → (𝑢 ∘ 𝑔) = (𝑢 ∘ 𝑣))
188		xkococn.1	. . . . . . . . . . . . . . 15 ⊢ 𝐹 = (𝑓 ∈ (𝑆 Cn 𝑇), 𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝑓 ∘ 𝑔))
189		vex 3468	. . . . . . . . . . . . . . . 16 ⊢ 𝑢 ∈ V
190		vex 3468	. . . . . . . . . . . . . . . 16 ⊢ 𝑣 ∈ V
191	189, 190	coex 7931	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∘ 𝑣) ∈ V
192	186, 187, 188, 191	ovmpo 7572	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ 𝑣 ∈ (𝑅 Cn 𝑆)) → (𝑢𝐹𝑣) = (𝑢 ∘ 𝑣))
193	184, 185, 192	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢𝐹𝑣) = (𝑢 ∘ 𝑣))
194		imaeq1 6047	. . . . . . . . . . . . . . 15 ⊢ (ℎ = (𝑢 ∘ 𝑣) → (ℎ “ 𝐾) = ((𝑢 ∘ 𝑣) “ 𝐾))
195	194	sseq1d 3995	. . . . . . . . . . . . . 14 ⊢ (ℎ = (𝑢 ∘ 𝑣) → ((ℎ “ 𝐾) ⊆ 𝑉 ↔ ((𝑢 ∘ 𝑣) “ 𝐾) ⊆ 𝑉))
196		cnco 23209	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ (𝑅 Cn 𝑆) ∧ 𝑢 ∈ (𝑆 Cn 𝑇)) → (𝑢 ∘ 𝑣) ∈ (𝑅 Cn 𝑇))
197	185, 184, 196	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 ∘ 𝑣) ∈ (𝑅 Cn 𝑇))
198		imaco 6245	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∘ 𝑣) “ 𝐾) = (𝑢 “ (𝑣 “ 𝐾))
199		simprrr 781	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)))
200	15	ntrss2 23000	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 ∈ Top ∧ (𝑘‘𝑦) ⊆ ∪ 𝑆) → ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦))
201	200	ex 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑆 ∈ Top → ((𝑘‘𝑦) ⊆ ∪ 𝑆 → ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦)))
202	201	ralimdv 3155	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ∈ Top → (∀𝑦 ∈ 𝑤 (𝑘‘𝑦) ⊆ ∪ 𝑆 → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦)))
203	88, 126, 202	sylc 65	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦))
204		ss2iun 4991	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ (𝑘‘𝑦) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦))
205	203, 204	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦)) ⊆ ∪ 𝑦 ∈ 𝑤 (𝑘‘𝑦))
206	205, 108	sseqtrd 4000	. . . . . . . . . . . . . . . . . . 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 3974	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑣 “ 𝐾) ⊆ ∪ ran 𝑘)
209		imass2 6094	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑣 “ 𝐾) ⊆ ∪ ran 𝑘 → (𝑢 “ (𝑣 “ 𝐾)) ⊆ (𝑢 “ ∪ ran 𝑘))
210	208, 209	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ (𝑣 “ 𝐾)) ⊆ (𝑢 “ ∪ ran 𝑘))
211		simprlr 779	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉)
212	210, 211	sstrd 3974	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 “ (𝑣 “ 𝐾)) ⊆ 𝑉)
213	198, 212	eqsstrid 4002	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → ((𝑢 ∘ 𝑣) “ 𝐾) ⊆ 𝑉)
214	195, 197, 213	elrabd 3678	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢 ∘ 𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
215	193, 214	eqeltrd 2835	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ ((𝑢 ∈ (𝑆 Cn 𝑇) ∧ (𝑢 “ ∪ ran 𝑘) ⊆ 𝑉) ∧ (𝑣 ∈ (𝑅 Cn 𝑆) ∧ (𝑣 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))))) → (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
216	183, 215	sylan2b 594	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) ∧ (𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ∧ 𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) → (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
217	216	ralrimivva 3188	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ ((𝐵 “ 𝐾) = ∪ 𝑤 ∧ (𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)))) → ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})
218	188	mpofun 7536	. . . . . . . . . . 11 ⊢ Fun 𝐹
219		ssrab2 4060	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇)
220		ssrab2 4060	. . . . . . . . . . . . 13 ⊢ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ⊆ (𝑅 Cn 𝑆)
221		xpss12 5674	. . . . . . . . . . . . 13 ⊢ (({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} ⊆ (𝑆 Cn 𝑇) ∧ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} ⊆ (𝑅 Cn 𝑆)) → ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆)))
222	219, 220, 221	mp2an 692	. . . . . . . . . . . 12 ⊢ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))
223		vex 3468	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
224		vex 3468	. . . . . . . . . . . . . 14 ⊢ 𝑔 ∈ V
225	223, 224	coex 7931	. . . . . . . . . . . . 13 ⊢ (𝑓 ∘ 𝑔) ∈ V
226	188, 225	dmmpo 8075	. . . . . . . . . . . 12 ⊢ dom 𝐹 = ((𝑆 Cn 𝑇) × (𝑅 Cn 𝑆))
227	222, 226	sseqtrri 4013	. . . . . . . . . . 11 ⊢ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹
228		funimassov 7589	. . . . . . . . . . 11 ⊢ ((Fun 𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ∀𝑢 ∈ {𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉}∀𝑣 ∈ {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))} (𝑢𝐹𝑣) ∈ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))
229	218, 227, 228	mp2an 692	. . . . . . . . . 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 7049	. . . . . . . . . 10 ⊢ ((Fun 𝐹 ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ dom 𝐹) → ((𝐹 “ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})) ⊆ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉} ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))
232	218, 227, 231	mp2an 692	. . . . . . . . 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 2824	. . . . . . . . . 10 ⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → (⟨𝐴, 𝐵⟩ ∈ 𝑧 ↔ ⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))})))
235		sseq1 3989	. . . . . . . . . 10 ⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → (𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}) ↔ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})))
236	234, 235	anbi12d 632	. . . . . . . . 9 ⊢ (𝑧 = ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) → ((⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉})) ↔ (⟨𝐴, 𝐵⟩ ∈ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ∧ ({𝑎 ∈ (𝑆 Cn 𝑇) ∣ (𝑎 “ ∪ ran 𝑘) ⊆ 𝑉} × {𝑏 ∈ (𝑅 Cn 𝑆) ∣ (𝑏 “ 𝐾) ⊆ ∪ 𝑦 ∈ 𝑤 ((int‘𝑆)‘(𝑘‘𝑦))}) ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
237	236	rspcev 3606	. . . . . . . 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 836	. . . . . . 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 1933	. . . . 5 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝒫 (𝑆 ↾_t (𝐵 “ 𝐾)) ∩ Fin)) ∧ (𝐵 “ 𝐾) = ∪ 𝑤) → (∃𝑘(𝑘:𝑤⟶𝒫 (^◡𝐴 “ 𝑉) ∧ ∀𝑦 ∈ 𝑤 (𝑦 ⊆ ((int‘𝑆)‘(𝑘‘𝑦)) ∧ (𝑆 ↾_t (𝑘‘𝑦)) ∈ Comp)) → ∃𝑧 ∈ ((𝑇 ↑_ko 𝑆) ×_t (𝑆 ↑_ko 𝑅))(⟨𝐴, 𝐵⟩ ∈ 𝑧 ∧ 𝑧 ⊆ (^◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))))
241	87, 240	syldan 591	. . . 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 3142	. 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 1086 = wceq 1540 ∃wex 1779 ∈ wcel 2109 ∀wral 3052 ∃wrex 3061 {crab 3420 Vcvv 3464 ∩ cin 3930 ⊆ wss 3931 𝒫 cpw 4580 ⟨cop 4612 ∪ cuni 4888 ∪ ciun 4972 × cxp 5657 ^◡ccnv 5658 dom cdm 5659 ran crn 5660 “ cima 5662 ∘ ccom 5663 Fun wfun 6530 Fn wfn 6531 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ∈ cmpo 7412 Fincfn 8964 ↾_t crest 17439 Topctop 22836 intcnt 22960 Cn ccn 23167 Compccmp 23329 𝑛-Locally cnlly 23408 ×_t ctx 23503 ↑_ko cxko 23504

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3062 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-1st 7993 df-2nd 7994 df-1o 8485 df-map 8847 df-en 8965 df-dom 8966 df-fin 8968 df-fi 9428 df-rest 17441 df-topgen 17462 df-top 22837 df-topon 22854 df-bases 22889 df-ntr 22963 df-nei 23041 df-cn 23170 df-cmp 23330 df-nlly 23410 df-tx 23505 df-xko 23506

This theorem is referenced by: xkococn 23603

W3C validator