This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 75 77 raleqtrdv ⊢ ( 𝜑 → ∀ 𝑥 ∈ ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) )
79 eqid ⊢ ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) = ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) )
80 fveq2 ⊢ ( 𝑠 = ( 𝑘 ‘ 𝑦 ) → ( ( int ‘ 𝑆 ) ‘ 𝑠 ) = ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) )
81 80 sseq2d ⊢ ( 𝑠 = ( 𝑘 ‘ 𝑦 ) → ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ↔ 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) )
82 oveq2 ⊢ ( 𝑠 = ( 𝑘 ‘ 𝑦 ) → ( 𝑆 ↾t 𝑠 ) = ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) )
83 82 eleq1d ⊢ ( 𝑠 = ( 𝑘 ‘ 𝑦 ) → ( ( 𝑆 ↾t 𝑠 ) ∈ Comp ↔ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) )
84 81 83 anbi12d ⊢ ( 𝑠 = ( 𝑘 ‘ 𝑦 ) → ( ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ↔ ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) )
85 79 84 cmpcovf ⊢ ( ( ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∈ Comp ∧ ∀ 𝑥 ∈ ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∃ 𝑦 ∈ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ( 𝑥 ∈ 𝑦 ∧ ∃ 𝑠 ∈ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ 𝑠 ) ∧ ( 𝑆 ↾t 𝑠 ) ∈ Comp ) ) ) → ∃ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ( ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) = ∪ 𝑤 ∧ ∃ 𝑘 ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) )
86 10 78 85 syl2anc ⊢ ( 𝜑 → ∃ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ( ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) = ∪ 𝑤 ∧ ∃ 𝑘 ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) )
87 77 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) → ( 𝐵 “ 𝐾 ) = ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) )
88 87 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) → ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ↔ ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) = ∪ 𝑤 ) )
89 88 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) = ∪ 𝑤 ) → ( 𝐵 “ 𝐾 ) = ∪ 𝑤 )
90 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝑆 ∈ Top )
91 cntop2 ⊢ ( 𝐴 ∈ ( 𝑆 Cn 𝑇 ) → 𝑇 ∈ Top )
92 6 91 syl ⊢ ( 𝜑 → 𝑇 ∈ Top )
93 92 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝑇 ∈ Top )
94 xkotop ⊢ ( ( 𝑆 ∈ Top ∧ 𝑇 ∈ Top ) → ( 𝑇 ↑ko 𝑆 ) ∈ Top )
95 90 93 94 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝑇 ↑ko 𝑆 ) ∈ Top )
96 cntop1 ⊢ ( 𝐵 ∈ ( 𝑅 Cn 𝑆 ) → 𝑅 ∈ Top )
97 7 96 syl ⊢ ( 𝜑 → 𝑅 ∈ Top )
98 97 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝑅 ∈ Top )
99 xkotop ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑆 ↑ko 𝑅 ) ∈ Top )
100 98 90 99 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝑆 ↑ko 𝑅 ) ∈ Top )
101 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) )
102 101 frnd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ran 𝑘 ⊆ 𝒫 ( ◡ 𝐴 “ 𝑉 ) )
103 sspwuni ⊢ ( ran 𝑘 ⊆ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ↔ ∪ ran 𝑘 ⊆ ( ◡ 𝐴 “ 𝑉 ) )
104 102 103 sylib ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ ran 𝑘 ⊆ ( ◡ 𝐴 “ 𝑉 ) )
105 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( ◡ 𝐴 “ 𝑉 ) ∈ 𝑆 )
106 105 52 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( ◡ 𝐴 “ 𝑉 ) ⊆ ∪ 𝑆 )
107 104 106 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ ran 𝑘 ⊆ ∪ 𝑆 )
108 ffn ⊢ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) → 𝑘 Fn 𝑤 )
109 fniunfv ⊢ ( 𝑘 Fn 𝑤 → ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) = ∪ ran 𝑘 )
110 101 108 109 3syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) = ∪ ran 𝑘 )
111 110 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝑆 ↾t ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ) = ( 𝑆 ↾t ∪ ran 𝑘 ) )
112 simplr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) )
113 112 elin2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝑤 ∈ Fin )
114 simprrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) )
115 simpr ⊢ ( ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) → ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp )
116 115 ralimi ⊢ ( ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) → ∀ 𝑦 ∈ 𝑤 ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp )
117 114 116 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∀ 𝑦 ∈ 𝑤 ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp )
118 17 fiuncmp ⊢ ( ( 𝑆 ∈ Top ∧ 𝑤 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) → ( 𝑆 ↾t ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ) ∈ Comp )
119 90 113 117 118 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝑆 ↾t ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ) ∈ Comp )
120 111 119 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝑆 ↾t ∪ ran 𝑘 ) ∈ Comp )
121 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝑉 ∈ 𝑇 )
122 17 90 93 107 120 121 xkoopn ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ∈ ( 𝑇 ↑ko 𝑆 ) )
123 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝐾 ⊆ ∪ 𝑅 )
124 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝑅 ↾t 𝐾 ) ∈ Comp )
125 110 107 eqsstrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 )
126 iunss ⊢ ( ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 ↔ ∀ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 )
127 125 126 sylib ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∀ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 )
128 17 ntropn ⊢ ( ( 𝑆 ∈ Top ∧ ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 ) → ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∈ 𝑆 )
129 128 ex ⊢ ( 𝑆 ∈ Top → ( ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 → ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∈ 𝑆 ) )
130 129 ralimdv ⊢ ( 𝑆 ∈ Top → ( ∀ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 → ∀ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∈ 𝑆 ) )
131 90 127 130 sylc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∀ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∈ 𝑆 )
132 iunopn ⊢ ( ( 𝑆 ∈ Top ∧ ∀ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∈ 𝑆 ) → ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∈ 𝑆 )
133 90 131 132 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∈ 𝑆 )
134 23 98 90 123 124 133 xkoopn ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ∈ ( 𝑆 ↑ko 𝑅 ) )
135 txopn ⊢ ( ( ( ( 𝑇 ↑ko 𝑆 ) ∈ Top ∧ ( 𝑆 ↑ko 𝑅 ) ∈ Top ) ∧ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ∈ ( 𝑇 ↑ko 𝑆 ) ∧ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ∈ ( 𝑆 ↑ko 𝑅 ) ) ) → ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) )
136 95 100 122 134 135 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) )
137 imaeq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 “ ∪ ran 𝑘 ) = ( 𝐴 “ ∪ ran 𝑘 ) )
138 137 sseq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 ↔ ( 𝐴 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) )
139 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝐴 ∈ ( 𝑆 Cn 𝑇 ) )
140 imaiun ⊢ ( 𝐴 “ ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ) = ∪ 𝑦 ∈ 𝑤 ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) )
141 110 imaeq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝐴 “ ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ) = ( 𝐴 “ ∪ ran 𝑘 ) )
142 140 141 eqtr3id ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) = ( 𝐴 “ ∪ ran 𝑘 ) )
143 110 104 eqsstrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) )
144 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → Fun 𝐴 )
145 101 108 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝑘 Fn 𝑤 )
146 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → dom 𝐴 = ∪ 𝑆 )
147 107 146 sseqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ ran 𝑘 ⊆ dom 𝐴 )
148 simpl1 ⊢ ( ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) ∧ 𝑦 ∈ 𝑤 ) → Fun 𝐴 )
149 109 3ad2ant2 ⊢ ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) → ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) = ∪ ran 𝑘 )
150 simp3 ⊢ ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) → ∪ ran 𝑘 ⊆ dom 𝐴 )
151 149 150 eqsstrd ⊢ ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) → ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ dom 𝐴 )
152 iunss ⊢ ( ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ dom 𝐴 ↔ ∀ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ dom 𝐴 )
153 151 152 sylib ⊢ ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) → ∀ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ dom 𝐴 )
154 153 r19.21bi ⊢ ( ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) ∧ 𝑦 ∈ 𝑤 ) → ( 𝑘 ‘ 𝑦 ) ⊆ dom 𝐴 )
155 funimass3 ⊢ ( ( Fun 𝐴 ∧ ( 𝑘 ‘ 𝑦 ) ⊆ dom 𝐴 ) → ( ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) ⊆ 𝑉 ↔ ( 𝑘 ‘ 𝑦 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) ) )
156 148 154 155 syl2anc ⊢ ( ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) ∧ 𝑦 ∈ 𝑤 ) → ( ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) ⊆ 𝑉 ↔ ( 𝑘 ‘ 𝑦 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) ) )
157 156 ralbidva ⊢ ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) → ( ∀ 𝑦 ∈ 𝑤 ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) ⊆ 𝑉 ↔ ∀ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) ) )
158 iunss ⊢ ( ∪ 𝑦 ∈ 𝑤 ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) ⊆ 𝑉 ↔ ∀ 𝑦 ∈ 𝑤 ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) ⊆ 𝑉 )
159 iunss ⊢ ( ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) ↔ ∀ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) )
160 157 158 159 3bitr4g ⊢ ( ( Fun 𝐴 ∧ 𝑘 Fn 𝑤 ∧ ∪ ran 𝑘 ⊆ dom 𝐴 ) → ( ∪ 𝑦 ∈ 𝑤 ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) ⊆ 𝑉 ↔ ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) ) )
161 144 145 147 160 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( ∪ 𝑦 ∈ 𝑤 ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) ⊆ 𝑉 ↔ ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ( ◡ 𝐴 “ 𝑉 ) ) )
162 143 161 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( 𝐴 “ ( 𝑘 ‘ 𝑦 ) ) ⊆ 𝑉 )
163 142 162 eqsstrrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝐴 “ ∪ ran 𝑘 ) ⊆ 𝑉 )
164 138 139 163 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝐴 ∈ { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } )
165 imaeq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 “ 𝐾 ) = ( 𝐵 “ 𝐾 ) )
166 165 sseq1d ⊢ ( 𝑏 = 𝐵 → ( ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ↔ ( 𝐵 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) )
167 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝐵 ∈ ( 𝑅 Cn 𝑆 ) )
168 simprl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝐵 “ 𝐾 ) = ∪ 𝑤 )
169 uniiun ⊢ ∪ 𝑤 = ∪ 𝑦 ∈ 𝑤 𝑦
170 168 169 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝐵 “ 𝐾 ) = ∪ 𝑦 ∈ 𝑤 𝑦 )
171 simpl ⊢ ( ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) → 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) )
172 171 ralimi ⊢ ( ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) → ∀ 𝑦 ∈ 𝑤 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) )
173 ss2iun ⊢ ( ∀ 𝑦 ∈ 𝑤 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) → ∪ 𝑦 ∈ 𝑤 𝑦 ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) )
174 114 172 173 3syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 𝑦 ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) )
175 170 174 eqsstrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝐵 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) )
176 166 167 175 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → 𝐵 ∈ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } )
177 164 176 opelxpd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) )
178 imaeq1 ⊢ ( 𝑎 = 𝑢 → ( 𝑎 “ ∪ ran 𝑘 ) = ( 𝑢 “ ∪ ran 𝑘 ) )
179 178 sseq1d ⊢ ( 𝑎 = 𝑢 → ( ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 ↔ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) )
180 179 elrab ⊢ ( 𝑢 ∈ { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ↔ ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) )
181 imaeq1 ⊢ ( 𝑏 = 𝑣 → ( 𝑏 “ 𝐾 ) = ( 𝑣 “ 𝐾 ) )
182 181 sseq1d ⊢ ( 𝑏 = 𝑣 → ( ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ↔ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) )
183 182 elrab ⊢ ( 𝑣 ∈ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ↔ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) )
184 180 183 anbi12i ⊢ ( ( 𝑢 ∈ { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ∧ 𝑣 ∈ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ↔ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) )
185 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → 𝑢 ∈ ( 𝑆 Cn 𝑇 ) )
186 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → 𝑣 ∈ ( 𝑅 Cn 𝑆 ) )
187 coeq1 ⊢ ( 𝑓 = 𝑢 → ( 𝑓 ∘ 𝑔 ) = ( 𝑢 ∘ 𝑔 ) )
188 coeq2 ⊢ ( 𝑔 = 𝑣 → ( 𝑢 ∘ 𝑔 ) = ( 𝑢 ∘ 𝑣 ) )
189 vex ⊢ 𝑢 ∈ V
190 vex ⊢ 𝑣 ∈ V
191 189 190 coex ⊢ ( 𝑢 ∘ 𝑣 ) ∈ V
192 187 188 1 191 ovmpo ⊢ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ) → ( 𝑢 𝐹 𝑣 ) = ( 𝑢 ∘ 𝑣 ) )
193 185 186 192 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑢 𝐹 𝑣 ) = ( 𝑢 ∘ 𝑣 ) )
194 imaeq1 ⊢ ( ℎ = ( 𝑢 ∘ 𝑣 ) → ( ℎ “ 𝐾 ) = ( ( 𝑢 ∘ 𝑣 ) “ 𝐾 ) )
195 194 sseq1d ⊢ ( ℎ = ( 𝑢 ∘ 𝑣 ) → ( ( ℎ “ 𝐾 ) ⊆ 𝑉 ↔ ( ( 𝑢 ∘ 𝑣 ) “ 𝐾 ) ⊆ 𝑉 ) )
196 cnco ⊢ ( ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ) → ( 𝑢 ∘ 𝑣 ) ∈ ( 𝑅 Cn 𝑇 ) )
197 186 185 196 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑢 ∘ 𝑣 ) ∈ ( 𝑅 Cn 𝑇 ) )
198 imaco ⊢ ( ( 𝑢 ∘ 𝑣 ) “ 𝐾 ) = ( 𝑢 “ ( 𝑣 “ 𝐾 ) )
199 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) )
200 17 ntrss2 ⊢ ( ( 𝑆 ∈ Top ∧ ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 ) → ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ( 𝑘 ‘ 𝑦 ) )
201 200 ex ⊢ ( 𝑆 ∈ Top → ( ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 → ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ( 𝑘 ‘ 𝑦 ) ) )
202 201 ralimdv ⊢ ( 𝑆 ∈ Top → ( ∀ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) ⊆ ∪ 𝑆 → ∀ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ( 𝑘 ‘ 𝑦 ) ) )
203 90 127 202 sylc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∀ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ( 𝑘 ‘ 𝑦 ) )
204 ss2iun ⊢ ( ∀ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ( 𝑘 ‘ 𝑦 ) → ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) )
205 203 204 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ∪ 𝑦 ∈ 𝑤 ( 𝑘 ‘ 𝑦 ) )
206 205 110 sseqtrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ∪ ran 𝑘 )
207 206 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ⊆ ∪ ran 𝑘 )
208 199 207 sstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑣 “ 𝐾 ) ⊆ ∪ ran 𝑘 )
209 imass2 ⊢ ( ( 𝑣 “ 𝐾 ) ⊆ ∪ ran 𝑘 → ( 𝑢 “ ( 𝑣 “ 𝐾 ) ) ⊆ ( 𝑢 “ ∪ ran 𝑘 ) )
210 208 209 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑢 “ ( 𝑣 “ 𝐾 ) ) ⊆ ( 𝑢 “ ∪ ran 𝑘 ) )
211 simprlr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 )
212 210 211 sstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑢 “ ( 𝑣 “ 𝐾 ) ) ⊆ 𝑉 )
213 198 212 eqsstrid ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( ( 𝑢 ∘ 𝑣 ) “ 𝐾 ) ⊆ 𝑉 )
214 195 197 213 elrabd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑢 ∘ 𝑣 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } )
215 193 214 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( ( 𝑢 ∈ ( 𝑆 Cn 𝑇 ) ∧ ( 𝑢 “ ∪ ran 𝑘 ) ⊆ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝑅 Cn 𝑆 ) ∧ ( 𝑣 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ) ) ) → ( 𝑢 𝐹 𝑣 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } )
216 184 215 sylan2b ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) ∧ ( 𝑢 ∈ { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ∧ 𝑣 ∈ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ) → ( 𝑢 𝐹 𝑣 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } )
217 216 ralrimivva ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∀ 𝑢 ∈ { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ∀ 𝑣 ∈ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ( 𝑢 𝐹 𝑣 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } )
218 1 mpofun ⊢ Fun 𝐹
219 ssrab2 ⊢ { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ⊆ ( 𝑆 Cn 𝑇 )
220 ssrab2 ⊢ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ⊆ ( 𝑅 Cn 𝑆 )
221 xpss12 ⊢ ( ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ⊆ ( 𝑆 Cn 𝑇 ) ∧ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ⊆ ( 𝑅 Cn 𝑆 ) ) → ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) ) )
222 219 220 221 mp2an ⊢ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) )
223 vex ⊢ 𝑓 ∈ V
224 vex ⊢ 𝑔 ∈ V
225 223 224 coex ⊢ ( 𝑓 ∘ 𝑔 ) ∈ V
226 1 225 dmmpo ⊢ dom 𝐹 = ( ( 𝑆 Cn 𝑇 ) × ( 𝑅 Cn 𝑆 ) )
227 222 226 sseqtrri ⊢ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ dom 𝐹
228 funimassov ⊢ ( ( Fun 𝐹 ∧ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ) ⊆ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ↔ ∀ 𝑢 ∈ { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ∀ 𝑣 ∈ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ( 𝑢 𝐹 𝑣 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) )
229 218 227 228 mp2an ⊢ ( ( 𝐹 “ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ) ⊆ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ↔ ∀ 𝑢 ∈ { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } ∀ 𝑣 ∈ { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ( 𝑢 𝐹 𝑣 ) ∈ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } )
230 217 229 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( 𝐹 “ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ) ⊆ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } )
231 funimass3 ⊢ ( ( Fun 𝐹 ∧ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ) ⊆ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ↔ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) )
232 218 227 231 mp2an ⊢ ( ( 𝐹 “ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ) ⊆ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ↔ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) )
233 230 232 sylib ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) )
234 eleq2 ⊢ ( 𝑧 = ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ) )
235 sseq1 ⊢ ( 𝑧 = ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) → ( 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ↔ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) )
236 234 235 anbi12d ⊢ ( 𝑧 = ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ∧ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) ) )
237 236 rspcev ⊢ ( ( ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ∧ ( { 𝑎 ∈ ( 𝑆 Cn 𝑇 ) ∣ ( 𝑎 “ ∪ ran 𝑘 ) ⊆ 𝑉 } × { 𝑏 ∈ ( 𝑅 Cn 𝑆 ) ∣ ( 𝑏 “ 𝐾 ) ⊆ ∪ 𝑦 ∈ 𝑤 ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) } ) ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) ) → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) )
238 136 177 233 237 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ∧ ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) ) → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) )
239 238 expr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ) → ( ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) ) )
240 239 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ( 𝐵 “ 𝐾 ) = ∪ 𝑤 ) → ( ∃ 𝑘 ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) ) )
241 89 240 syldan ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) ∧ ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) = ∪ 𝑤 ) → ( ∃ 𝑘 ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) ) )
242 241 expimpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ) → ( ( ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) = ∪ 𝑤 ∧ ∃ 𝑘 ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) ) )
243 242 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ( 𝒫 ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) ∩ Fin ) ( ∪ ( 𝑆 ↾t ( 𝐵 “ 𝐾 ) ) = ∪ 𝑤 ∧ ∃ 𝑘 ( 𝑘 : 𝑤 ⟶ 𝒫 ( ◡ 𝐴 “ 𝑉 ) ∧ ∀ 𝑦 ∈ 𝑤 ( 𝑦 ⊆ ( ( int ‘ 𝑆 ) ‘ ( 𝑘 ‘ 𝑦 ) ) ∧ ( 𝑆 ↾t ( 𝑘 ‘ 𝑦 ) ) ∈ Comp ) ) ) → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) ) )
244 86 243 mpd ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( ( 𝑇 ↑ko 𝑆 ) ×t ( 𝑆 ↑ko 𝑅 ) ) ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑧 ∧ 𝑧 ⊆ ( ◡ 𝐹 “ { ℎ ∈ ( 𝑅 Cn 𝑇 ) ∣ ( ℎ “ 𝐾 ) ⊆ 𝑉 } ) ) )