Metamath Proof Explorer

Theorem xkococnlem

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)

Ref Expression
Hypotheses 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 xkococnlem ( 𝜑 → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) )

Proof

Step Hyp Ref Expression
1 xkococn.1 ⊢ 𝐹 = ( 𝑓 ∈ ( 𝑆 Cn 𝑇 ) , 𝑔 ∈ ( 𝑅 Cn 𝑆 ) ↦ ( 𝑓 ∘ 𝑔 ) )
2 xkococn.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑛-Locally Comp )
3 xkococn.k ⊢ ( 𝜑 → 𝐾 ⊆ ∪ 𝑅 )
4 xkococn.c ⊢ ( 𝜑 → ( 𝑅 ↾t 𝐾 ) ∈ Comp )
5 xkococn.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑇 )
6 xkococn.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝑆 Cn 𝑇 ) )
7 xkococn.b ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑅 Cn 𝑆 ) )
8 xkococn.i ⊢ ( 𝜑 → ( ( 𝐴 ∘ 𝐵 ) “ 𝐾 ) ⊆ 𝑉 )
9 imacmp ⊢ ( ( 𝐵 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑅 ↾t 𝐾 ) ∈ Comp ) → ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∈ Comp )
10 7 4 9 syl2anc ⊢ ( 𝜑 → ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∈ Comp )
11 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) → 𝑆 ∈ 𝑛-Locally Comp )
12 cnima ⊢ ( ( 𝐴 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑉 ∈ 𝑇 ) → ( ◡ 𝐴 “ 𝑉 ) ∈ 𝑆 )
13 6 5 12 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐴 “ 𝑉 ) ∈ 𝑆 )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) → ( ◡ 𝐴 “ 𝑉 ) ∈ 𝑆 )
15 imaco ⊢ ( ( 𝐴 ∘ 𝐵 ) “ 𝐾 ) = ( 𝐴 “ ( 𝐵 “ 𝐾 ) )
16 15 8 eqsstrrid ⊢ ( 𝜑 → ( 𝐴 “ ( 𝐵 “ 𝐾 ) ) ⊆ 𝑉 )
17 eqid ⊢ ∪ 𝑆 = ∪ 𝑆
18 eqid ⊢ ∪ 𝑇 = ∪ 𝑇
19 17 18 cnf ⊢ ( 𝐴 ∈ ( 𝑆 Cn 𝑇 ) → 𝐴 : ∪ 𝑆 ⟶ ∪ 𝑇 )
20 ffun ⊢ ( 𝐴 : ∪ 𝑆 ⟶ ∪ 𝑇 → Fun 𝐴 )
21 6 19 20 3syl ⊢ ( 𝜑 → Fun 𝐴 )
22 imassrn ⊢ ( 𝐵 “ 𝐾 ) ⊆ ran 𝐵
23 eqid ⊢ ∪ 𝑅 = ∪ 𝑅
24 23 17 cnf ⊢ ( 𝐵 ∈ ( 𝑅 Cn 𝑆 ) → 𝐵 : ∪ 𝑅 ⟶ ∪ 𝑆 )
25 frn ⊢ ( 𝐵 : ∪ 𝑅 ⟶ ∪ 𝑆 → ran 𝐵 ⊆ ∪ 𝑆 )
26 7 24 25 3syl ⊢ ( 𝜑 → ran 𝐵 ⊆ ∪ 𝑆 )
27 22 26 sstrid ⊢ ( 𝜑 → ( 𝐵 “ 𝐾 ) ⊆ ∪ 𝑆 )
28 fdm ⊢ ( 𝐴 : ∪ 𝑆 ⟶ ∪ 𝑇 → dom 𝐴 = ∪ 𝑆 )
29 6 19 28 3syl ⊢ ( 𝜑 → dom 𝐴 = ∪ 𝑆 )
30 27 29 sseqtrrd ⊢ ( 𝜑 → ( 𝐵 “ 𝐾 ) ⊆ dom 𝐴 )
31 funimass3 ⊢ ( ( Fun 𝐴 ∧ ( 𝐵 “ 𝐾 ) ⊆ dom 𝐴 ) → ( ( 𝐴 “ ( 𝐵 “ 𝐾 ) ) ⊆ 𝑉 ↔ ( 𝐵 “ 𝐾 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) ) )
32 21 30 31 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 “ ( 𝐵 “ 𝐾 ) ) ⊆ 𝑉 ↔ ( 𝐵 “ 𝐾 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) ) )
33 16 32 mpbid ⊢ ( 𝜑 → ( 𝐵 “ 𝐾 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) )
34 33 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) → 𝑥 ∈ ( ◡ 𝐴 “ 𝑉 ) )
35 nlly2i ⊢ ( ( 𝑆 ∈ 𝑛-Locally Comp ∧ ( ◡ 𝐴 “ 𝑉 ) ∈ 𝑆 ∧ 𝑥 ∈ ( ◡ 𝐴 “ 𝑉 ) ) → ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∃ 𝑢 ∈ 𝑆 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) )
36 11 14 34 35 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) → ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∃ 𝑢 ∈ 𝑆 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) )
37 nllytop ⊢ ( 𝑆 ∈ 𝑛-Locally Comp → 𝑆 ∈ Top )
38 2 37 syl ⊢ ( 𝜑 → 𝑆 ∈ Top )
39 38 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑆 ∈ Top )
40 imaexg ⊢ ( 𝐵 ∈ ( 𝑅 Cn 𝑆 ) → ( 𝐵 “ 𝐾 ) ∈ V )
41 7 40 syl ⊢ ( 𝜑 → ( 𝐵 “ 𝐾 ) ∈ V )
42 41 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝐵 “ 𝐾 ) ∈ V )
43 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑢 ∈ 𝑆 )
44 elrestr ⊢ ( ( 𝑆 ∈ Top ∧ ( 𝐵 “ 𝐾 ) ∈ V ∧ 𝑢 ∈ 𝑆 ) → ( 𝑢 ∩ ( 𝐵 “ 𝐾 ) ) ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) )
45 39 42 43 44 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑢 ∩ ( 𝐵 “ 𝐾 ) ) ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) )
46 simprr1 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑥 ∈ 𝑢 )
47 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑥 ∈ ( 𝐵 “ 𝐾 ) )
48 46 47 elind ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑥 ∈ ( 𝑢 ∩ ( 𝐵 “ 𝐾 ) ) )
49 inss1 ⊢ ( 𝑢 ∩ ( 𝐵 “ 𝐾 ) ) ⊆ 𝑢
50 elpwi ⊢ ( 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) → 𝑠 ⊆ ( ◡ 𝐴 “ 𝑉 ) )
51 50 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑠 ⊆ ( ◡ 𝐴 “ 𝑉 ) )
52 elssuni ⊢ ( ( ◡ 𝐴 “ 𝑉 ) ∈ 𝑆 → ( ◡ 𝐴 “ 𝑉 ) ⊆ ∪ 𝑆 )
53 13 52 syl ⊢ ( 𝜑 → ( ◡ 𝐴 “ 𝑉 ) ⊆ ∪ 𝑆 )
54 53 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → ( ◡ 𝐴 “ 𝑉 ) ⊆ ∪ 𝑆 )
55 51 54 sstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑠 ⊆ ∪ 𝑆 )
56 simprr2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑢 ⊆ 𝑠 )
57 17 ssntr ⊢ ( ( ( 𝑆 ∈ Top ∧ 𝑠 ⊆ ∪ 𝑆 ) ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑢 ⊆ 𝑠 ) ) → 𝑢 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) )
58 39 55 43 56 57 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → 𝑢 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) )
59 49 58 sstrid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑢 ∩ ( 𝐵 “ 𝐾 ) ) ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) )
60 simprr3 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → ( 𝑆 ↾t 𝑠 ) ∈ Comp )
61 59 60 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → ( ( 𝑢 ∩ ( 𝐵 “ 𝐾 ) ) ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) )
62 eleq2 ⊢ ( 𝑦 = ( 𝑢 ∩ ( 𝐵 “ 𝐾 ) ) → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ( 𝑢 ∩ ( 𝐵 “ 𝐾 ) ) ) )
63 cleq1lem ⊢ ( 𝑦 = ( 𝑢 ∩ ( 𝐵 “ 𝐾 ) ) → ( ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ↔ ( ( 𝑢 ∩ ( 𝐵 “ 𝐾 ) ) ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) )
64 62 63 anbi12d ⊢ ( 𝑦 = ( 𝑢 ∩ ( 𝐵 “ 𝐾 ) ) → ( ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ↔ ( 𝑥 ∈ ( 𝑢 ∩ ( 𝐵 “ 𝐾 ) ) ∧ ( ( 𝑢 ∩ ( 𝐵 “ 𝐾 ) ) ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) )
65 64 rspcev ⊢ ( ( ( 𝑢 ∩ ( 𝐵 “ 𝐾 ) ) ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∧ ( 𝑥 ∈ ( 𝑢 ∩ ( 𝐵 “ 𝐾 ) ) ∧ ( ( 𝑢 ∩ ( 𝐵 “ 𝐾 ) ) ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) )
66 45 48 61 65 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ) ∧ ( 𝑢 ∈ 𝑆 ∧ ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) )
67 66 rexlimdvaa ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) ∧ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ) → ( ∃ 𝑢 ∈ 𝑆 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) → ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) )
68 67 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) → ( ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∃ 𝑢 ∈ 𝑆 ( 𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) → ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) )
69 36 68 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) → ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) )
70 rexcom ⊢ ( ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ↔ ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) )
71 r19.42v ⊢ ( ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) )
72 71 rexbii ⊢ ( ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ↔ ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) )
73 70 72 bitri ⊢ ( ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ↔ ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) )
74 69 73 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ) → ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) )
75 74 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) )
76 17 restuni ⊢ ( ( 𝑆 ∈ Top ∧ ( 𝐵 “ 𝐾 ) ⊆ ∪ 𝑆 ) → ( 𝐵 “ 𝐾 ) = ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) )
77 38 27 76 syl2anc ⊢ ( 𝜑 → ( 𝐵 “ 𝐾 ) = ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) )
78 77 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝐵 “ 𝐾 ) ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ↔ ∀ 𝑥 ∈ ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) )
79 75 78 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) )
80 eqid ⊢ ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) = ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) )
81 fveq2 ⊢ ( 𝑠 = ( 𝑘 ‘ 𝑦 ) → ( ( int ‘ 𝑆 ) ‘ 𝑠 ) = ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) )
82 81 sseq2d ⊢ ( 𝑠 = ( 𝑘 ‘ 𝑦 ) → ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ↔ 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) )
83 oveq2 ⊢ ( 𝑠 = ( 𝑘 ‘ 𝑦 ) → ( 𝑆 ↾t 𝑠 ) = ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) )
84 83 eleq1d ⊢ ( 𝑠 = ( 𝑘 ‘ 𝑦 ) → ( ( 𝑆 ↾t 𝑠 ) ∈ Comp ↔ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) )
85 82 84 anbi12d ⊢ ( 𝑠 = ( 𝑘 ‘ 𝑦 ) → ( ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ↔ ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) )
86 80 85 cmpcovf ⊢ ( ( ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∈ Comp ∧ ∀ 𝑥 ∈ ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → ∃ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ( ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) = ∪ 𝑤 ∧ ∃ 𝑘 ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) )
87 10 79 86 syl2anc ⊢ ( 𝜑 → ∃ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ( ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) = ∪ 𝑤 ∧ ∃ 𝑘 ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) )
88 77 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) → ( 𝐵 “ 𝐾 ) = ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) )
89 88 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) → ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ↔ ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) = ∪ 𝑤 ) )
90 89 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) = ∪ 𝑤 ) → ( 𝐵 “ 𝐾 ) = ∪ 𝑤 )
91 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝑆 ∈ Top )
92 cntop2 ⊢ ( 𝐴 ∈ ( 𝑆 Cn 𝑇 ) → 𝑇 ∈ Top )
93 6 92 syl ⊢ ( 𝜑 → 𝑇 ∈ Top )
94 93 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝑇 ∈ Top )
95 xkotop ⊢ ( ( 𝑆 ∈ Top ∧ 𝑇 ∈ Top ) → ( 𝑇 ↑ko 𝑆 ) ∈ Top )
96 91 94 95 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝑇 ↑ko 𝑆 ) ∈ Top )
97 cntop1 ⊢ ( 𝐵 ∈ ( 𝑅 Cn 𝑆 ) → 𝑅 ∈ Top )
98 7 97 syl ⊢ ( 𝜑 → 𝑅 ∈ Top )
99 98 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝑅 ∈ Top )
100 xkotop ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) ∈ Top )
101 99 91 100 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝑆 ↑ko 𝑅 ) ∈ Top )
102 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) )
103 102 frnd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ran 𝑘 ⊆ 𝒫 ( ◡ 𝐴 “ 𝑉 ) )
104 sspwuni ⊢ ( ran 𝑘 ⊆ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ↔ ∪ ran 𝑘 ⊆ ( ◡ 𝐴 “ 𝑉 ) )
105 103 104 sylib ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ ran 𝑘 ⊆ ( ◡ 𝐴 “ 𝑉 ) )
106 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( ◡ 𝐴 “ 𝑉 ) ∈ 𝑆 )
107 106 52 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( ◡ 𝐴 “ 𝑉 ) ⊆ ∪ 𝑆 )
108 105 107 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ ran 𝑘 ⊆ ∪ 𝑆 )
109 ffn ⊢ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) → 𝑘 Fn 𝑤 )
110 fniunfv ⊢ ( 𝑘 Fn 𝑤 → ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) = ∪ ran 𝑘 )
111 102 109 110 3syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) = ∪ ran 𝑘 )
112 111 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝑆 ↾t ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ) = ( 𝑆 ↾t ∪ ran 𝑘 ) )
113 simplr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) )
114 113 elin2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝑤 ∈ Fin )
115 simprrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) )
116 simpr ⊢ ( ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) → ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp )
117 116 ralimi ⊢ ( ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) → ∀ 𝑦 ∈ 𝑤 ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp )
118 115 117 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∀ 𝑦 ∈ 𝑤 ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp )
119 17 fiuncmp ⊢ ( ( 𝑆 ∈ Top ∧ 𝑤 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) → ( 𝑆 ↾t ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ) ∈ Comp )
120 91 114 118 119 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝑆 ↾t ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ) ∈ Comp )
121 112 120 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝑆 ↾t ∪ ran 𝑘 ) ∈ Comp )
122 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝑉 ∈ 𝑇 )
123 17 91 94 108 121 122 xkoopn ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ∈ ( 𝑇 ↑ko 𝑆 ) )
124 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝐾 ⊆ ∪ 𝑅 )
125 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝑅 ↾t 𝐾 ) ∈ Comp )
126 111 108 eqsstrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 )
127 iunss ⊢ ( ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 ↔ ∀ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 )
128 126 127 sylib ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∀ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 )
129 17 ntropn ⊢ ( ( 𝑆 ∈ Top ∧ ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 ) → ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∈ 𝑆 )
130 129 ex ⊢ ( 𝑆 ∈ Top → ( ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 → ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∈ 𝑆 ) )
131 130 ralimdv ⊢ ( 𝑆 ∈ Top → ( ∀ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 → ∀ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∈ 𝑆 ) )
132 91 128 131 sylc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∀ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∈ 𝑆 )
133 iunopn ⊢ ( ( 𝑆 ∈ Top ∧ ∀ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∈ 𝑆 ) → ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∈ 𝑆 )
134 91 132 133 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∈ 𝑆 )
135 23 99 91 124 125 134 xkoopn ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ∈ ( 𝑆 ↑ko 𝑅 ) )
136 txopn ⊢ ( ( ( ( 𝑇 ↑ko 𝑆 ) ∈ Top ∧ ( 𝑆 ↑ko 𝑅 ) ∈ Top ) ∧ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ∈ ( 𝑇 ↑ko 𝑆 ) ∧ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ∈ ( 𝑆 ↑ko 𝑅 ) ) ) → ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) )
137 96 101 123 135 136 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) )
138 imaeq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 “ ∪ ran 𝑘 ) = ( 𝐴 “ ∪ ran 𝑘 ) )
139 138 sseq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 ↔ ( 𝐴 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) )
140 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝐴 ∈ ( 𝑆 Cn 𝑇 ) )
141 imaiun ⊢ ( 𝐴 “ ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ) = ∪ 𝑦 ∈ 𝑤 ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) )
142 111 imaeq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝐴 “ ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ) = ( 𝐴 “ ∪ ran 𝑘 ) )
143 141 142 eqtr3id ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) = ( 𝐴 “ ∪ ran 𝑘 ) )
144 111 105 eqsstrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) )
145 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → Fun 𝐴 )
146 102 109 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝑘 Fn 𝑤 )
147 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → dom 𝐴 = ∪ 𝑆 )
148 108 147 sseqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ ran 𝑘 ⊆ dom 𝐴 )
149 simpl1 ⊢ ( ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) ∧ 𝑦 ∈ 𝑤 ) → Fun 𝐴 )
150 110 3ad2ant2 ⊢ ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) → ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) = ∪ ran 𝑘 )
151 simp3 ⊢ ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) → ∪ ran 𝑘 ⊆ dom 𝐴 )
152 150 151 eqsstrd ⊢ ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) → ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ dom 𝐴 )
153 iunss ⊢ ( ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ dom 𝐴 ↔ ∀ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ dom 𝐴 )
154 152 153 sylib ⊢ ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) → ∀ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ dom 𝐴 )
155 154 r19.21bi ⊢ ( ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) ∧ 𝑦 ∈ 𝑤 ) → ( 𝑘 ‘ 𝑦 ) ⊆ dom 𝐴 )
156 funimass3 ⊢ ( ( Fun 𝐴 ∧ ( 𝑘 ‘ 𝑦 ) ⊆ dom 𝐴 ) → ( ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) ⊆ 𝑉 ↔ ( 𝑘 ‘ 𝑦 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) ) )
157 149 155 156 syl2anc ⊢ ( ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) ∧ 𝑦 ∈ 𝑤 ) → ( ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) ⊆ 𝑉 ↔ ( 𝑘 ‘ 𝑦 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) ) )
158 157 ralbidva ⊢ ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) → ( ∀ 𝑦 ∈ 𝑤 ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) ⊆ 𝑉 ↔ ∀ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) ) )
159 iunss ⊢ ( ∪ 𝑦 ∈ 𝑤 ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) ⊆ 𝑉 ↔ ∀ 𝑦 ∈ 𝑤 ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) ⊆ 𝑉 )
160 iunss ⊢ ( ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) ↔ ∀ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) )
161 158 159 160 3bitr4g ⊢ ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) → ( ∪ 𝑦 ∈ 𝑤 ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) ⊆ 𝑉 ↔ ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) ) )
162 145 146 148 161 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( ∪ 𝑦 ∈ 𝑤 ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) ⊆ 𝑉 ↔ ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) ) )
163 144 162 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) ⊆ 𝑉 )
164 143 163 eqsstrrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝐴 “ ∪ ran 𝑘 ) ⊆ 𝑉 )
165 139 140 164 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝐴 ∈ { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } )
166 imaeq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 “ 𝐾 ) = ( 𝐵 “ 𝐾 ) )
167 166 sseq1d ⊢ ( 𝑏 = 𝐵 → ( ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ↔ ( 𝐵 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) )
168 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝐵 ∈ ( 𝑅 Cn 𝑆 ) )
169 simprl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝐵 “ 𝐾 ) = ∪ 𝑤 )
170 uniiun ⊢ ∪ 𝑤 = ∪ 𝑦 ∈ 𝑤 𝑦
171 169 170 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝐵 “ 𝐾 ) = ∪ 𝑦 ∈ 𝑤 𝑦 )
172 simpl ⊢ ( ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) → 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) )
173 172 ralimi ⊢ ( ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) → ∀ 𝑦 ∈ 𝑤 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) )
174 ss2iun ⊢ ( ∀ 𝑦 ∈ 𝑤 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) → ∪ 𝑦 ∈ 𝑤 𝑦 ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) )
175 115 173 174 3syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 𝑦 ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) )
176 171 175 eqsstrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝐵 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) )
177 167 168 176 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝐵 ∈ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } )
178 165 177 opelxpd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) )
179 imaeq1 ⊢ ( 𝑎 = 𝑢 → ( 𝑎 “ ∪ ran 𝑘 ) = ( 𝑢 “ ∪ ran 𝑘 ) )
180 179 sseq1d ⊢ ( 𝑎 = 𝑢 → ( ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 ↔ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) )
181 180 elrab ⊢ ( 𝑢 ∈ { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ↔ ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) )
182 imaeq1 ⊢ ( 𝑏 = 𝑣 → ( 𝑏 “ 𝐾 ) = ( 𝑣 “ 𝐾 ) )
183 182 sseq1d ⊢ ( 𝑏 = 𝑣 → ( ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ↔ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) )
184 183 elrab ⊢ ( 𝑣 ∈ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ↔ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) )
185 181 184 anbi12i ⊢ ( ( 𝑢 ∈ { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ∧ 𝑣 ∈ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ↔ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) )
186 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → 𝑢 ∈ ( 𝑆 Cn 𝑇 ) )
187 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → 𝑣 ∈ ( 𝑅 Cn 𝑆 ) )
188 coeq1 ⊢ ( 𝑓 = 𝑢 → ( 𝑓 ∘ 𝑔 ) = ( 𝑢 ∘ 𝑔 ) )
189 coeq2 ⊢ ( 𝑔 = 𝑣 → ( 𝑢 ∘ 𝑔 ) = ( 𝑢 ∘ 𝑣 ) )
190 vex ⊢ 𝑢 ∈ V
191 vex ⊢ 𝑣 ∈ V
192 190 191 coex ⊢ ( 𝑢 ∘ 𝑣 ) ∈ V
193 188 189 1 192 ovmpo ⊢ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ) → ( 𝑢 𝐹 𝑣 ) = ( 𝑢 ∘ 𝑣 ) )
194 186 187 193 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑢 𝐹 𝑣 ) = ( 𝑢 ∘ 𝑣 ) )
195 imaeq1 ⊢ ( ℎ = ( 𝑢 ∘ 𝑣 ) → ( ℎ “ 𝐾 ) = ( ( 𝑢 ∘ 𝑣 ) “ 𝐾 ) )
196 195 sseq1d ⊢ ( ℎ = ( 𝑢 ∘ 𝑣 ) → ( ( ℎ “ 𝐾 ) ⊆ 𝑉 ↔ ( ( 𝑢 ∘ 𝑣 ) “ 𝐾 ) ⊆ 𝑉 ) )
197 cnco ⊢ ( ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ) → ( 𝑢 ∘ 𝑣 ) ∈ ( 𝑅 Cn 𝑇 ) )
198 187 186 197 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑢 ∘ 𝑣 ) ∈ ( 𝑅 Cn 𝑇 ) )
199 imaco ⊢ ( ( 𝑢 ∘ 𝑣 ) “ 𝐾 ) = ( 𝑢 “ ( 𝑣 “ 𝐾 ) )
200 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) )
201 17 ntrss2 ⊢ ( ( 𝑆 ∈ Top ∧ ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 ) → ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ( 𝑘 ‘ 𝑦 ) )
202 201 ex ⊢ ( 𝑆 ∈ Top → ( ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 → ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ( 𝑘 ‘ 𝑦 ) ) )
203 202 ralimdv ⊢ ( 𝑆 ∈ Top → ( ∀ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 → ∀ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ( 𝑘 ‘ 𝑦 ) ) )
204 91 128 203 sylc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∀ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ( 𝑘 ‘ 𝑦 ) )
205 ss2iun ⊢ ( ∀ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ( 𝑘 ‘ 𝑦 ) → ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) )
206 204 205 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) )
207 206 111 sseqtrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ∪ ran 𝑘 )
208 207 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ∪ ran 𝑘 )
209 200 208 sstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑣 “ 𝐾 ) ⊆ ∪ ran 𝑘 )
210 imass2 ⊢ ( ( 𝑣 “ 𝐾 ) ⊆ ∪ ran 𝑘 → ( 𝑢 “ ( 𝑣 “ 𝐾 ) ) ⊆ ( 𝑢 “ ∪ ran 𝑘 ) )
211 209 210 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑢 “ ( 𝑣 “ 𝐾 ) ) ⊆ ( 𝑢 “ ∪ ran 𝑘 ) )
212 simprlr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 )
213 211 212 sstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑢 “ ( 𝑣 “ 𝐾 ) ) ⊆ 𝑉 )
214 199 213 eqsstrid ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( ( 𝑢 ∘ 𝑣 ) “ 𝐾 ) ⊆ 𝑉 )
215 196 198 214 elrabd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑢 ∘ 𝑣 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } )
216 194 215 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑢 𝐹 𝑣 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } )
217 185 216 sylan2b ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( 𝑢 ∈ { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ∧ 𝑣 ∈ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ) → ( 𝑢 𝐹 𝑣 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } )
218 217 ralrimivva ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∀ 𝑢 ∈ { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ∀ 𝑣 ∈ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ( 𝑢 𝐹 𝑣 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } )
219 1 mpofun ⊢ Fun 𝐹
220 ssrab2 ⊢ { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ⊆ ( 𝑆 Cn 𝑇 )
221 ssrab2 ⊢ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ⊆ ( 𝑅 Cn 𝑆 )
222 xpss12 ⊢ ( ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ⊆ ( 𝑆 Cn 𝑇 ) ∧ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ⊆ ( 𝑅 Cn 𝑆 ) ) → ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) ) )
223 220 221 222 mp2an ⊢ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) )
224 vex ⊢ 𝑓 ∈ V
225 vex ⊢ 𝑔 ∈ V
226 224 225 coex ⊢ ( 𝑓 ∘ 𝑔 ) ∈ V
227 1 226 dmmpo ⊢ dom 𝐹 = ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) )
228 223 227 sseqtrri ⊢ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ dom 𝐹
229 funimassov ⊢ ( ( Fun 𝐹 ∧ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ) ⊆ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ↔ ∀ 𝑢 ∈ { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ∀ 𝑣 ∈ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ( 𝑢 𝐹 𝑣 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) )
230 219 228 229 mp2an ⊢ ( ( 𝐹 “ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ) ⊆ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ↔ ∀ 𝑢 ∈ { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ∀ 𝑣 ∈ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ( 𝑢 𝐹 𝑣 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } )
231 218 230 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝐹 “ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ) ⊆ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } )
232 funimass3 ⊢ ( ( Fun 𝐹 ∧ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ) ⊆ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ↔ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) )
233 219 228 232 mp2an ⊢ ( ( 𝐹 “ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ) ⊆ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ↔ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) )
234 231 233 sylib ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) )
235 eleq2 ⊢ ( 𝑧 = ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ) )
236 sseq1 ⊢ ( 𝑧 = ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) → ( 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ↔ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) )
237 235 236 anbi12d ⊢ ( 𝑧 = ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ∧ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) ) )
238 237 rspcev ⊢ ( ( ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ∧ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) ) → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) )
239 137 178 234 238 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) )
240 239 expr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ) → ( ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) ) )
241 240 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ) → ( ∃ 𝑘 ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) ) )
242 90 241 syldan ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) = ∪ 𝑤 ) → ( ∃ 𝑘 ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) ) )
243 242 expimpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) → ( ( ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) = ∪ 𝑤 ∧ ∃ 𝑘 ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) ) )
244 243 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ( ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) = ∪ 𝑤 ∧ ∃ 𝑘 ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) ) )
245 87 244 mpd ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) )