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 𝑇 ) ∣ ( 𝐾 ) ⊆ 𝑉 } ) ) )