Metamath Proof Explorer

Theorem tmdgsum2

Description: For any neighborhood U of n X , there is a neighborhood u of X such that any sum of n elements in u sums to an element of U . (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Hypotheses tmdgsum.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
tmdgsum.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
tmdgsum2.t ⊢ · = ( .g ‘ 𝐺 )
tmdgsum2.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
tmdgsum2.2 ⊢ ( 𝜑 → 𝐺 ∈ TopMnd )
tmdgsum2.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
tmdgsum2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
tmdgsum2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
tmdgsum2.3 ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) · 𝑋 ) ∈ 𝑈 )
Assertion tmdgsum2 ( 𝜑 → ∃ 𝑢 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ ∀ 𝑓 ∈ ( 𝑢 ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 tmdgsum.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
2 tmdgsum.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 tmdgsum2.t ⊢ · = ( .g ‘ 𝐺 )
4 tmdgsum2.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
5 tmdgsum2.2 ⊢ ( 𝜑 → 𝐺 ∈ TopMnd )
6 tmdgsum2.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
7 tmdgsum2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
8 tmdgsum2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9 tmdgsum2.3 ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) · 𝑋 ) ∈ 𝑈 )
10 eqid ⊢ ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ↦ ( 𝐺 Σg 𝑓 ) ) = ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ↦ ( 𝐺 Σg 𝑓 ) )
11 10 mptpreima ⊢ ( ◡ ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ↦ ( 𝐺 Σg 𝑓 ) ) “ 𝑈 ) = { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 }
12 1 2 tmdgsum ⊢ ( ( 𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin ) → ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ↦ ( 𝐺 Σg 𝑓 ) ) ∈ ( ( 𝐽 ↑ko 𝒫 𝐴 ) Cn 𝐽 ) )
13 4 5 6 12 syl3anc ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ↦ ( 𝐺 Σg 𝑓 ) ) ∈ ( ( 𝐽 ↑ko 𝒫 𝐴 ) Cn 𝐽 ) )
14 cnima ⊢ ( ( ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ↦ ( 𝐺 Σg 𝑓 ) ) ∈ ( ( 𝐽 ↑ko 𝒫 𝐴 ) Cn 𝐽 ) ∧ 𝑈 ∈ 𝐽 ) → ( ◡ ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ↦ ( 𝐺 Σg 𝑓 ) ) “ 𝑈 ) ∈ ( 𝐽 ↑ko 𝒫 𝐴 ) )
15 13 7 14 syl2anc ⊢ ( 𝜑 → ( ◡ ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ↦ ( 𝐺 Σg 𝑓 ) ) “ 𝑈 ) ∈ ( 𝐽 ↑ko 𝒫 𝐴 ) )
16 11 15 eqeltrrid ⊢ ( 𝜑 → { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ∈ ( 𝐽 ↑ko 𝒫 𝐴 ) )
17 1 2 tmdtopon ⊢ ( 𝐺 ∈ TopMnd → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
18 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐽 ∈ Top )
19 5 17 18 3syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
20 xkopt ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ) → ( 𝐽 ↑ko 𝒫 𝐴 ) = ( ∏t ‘ ( 𝐴 × { 𝐽 } ) ) )
21 19 6 20 syl2anc ⊢ ( 𝜑 → ( 𝐽 ↑ko 𝒫 𝐴 ) = ( ∏t ‘ ( 𝐴 × { 𝐽 } ) ) )
22 fnconstg ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → ( 𝐴 × { 𝐽 } ) Fn 𝐴 )
23 5 17 22 3syl ⊢ ( 𝜑 → ( 𝐴 × { 𝐽 } ) Fn 𝐴 )
24 eqid ⊢ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) }
25 24 ptval ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐴 × { 𝐽 } ) Fn 𝐴 ) → ( ∏t ‘ ( 𝐴 × { 𝐽 } ) ) = ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ) )
26 6 23 25 syl2anc ⊢ ( 𝜑 → ( ∏t ‘ ( 𝐴 × { 𝐽 } ) ) = ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ) )
27 21 26 eqtrd ⊢ ( 𝜑 → ( 𝐽 ↑ko 𝒫 𝐴 ) = ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ) )
28 16 27 eleqtrd ⊢ ( 𝜑 → { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ∈ ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ) )
29 oveq2 ⊢ ( 𝑓 = ( 𝐴 × { 𝑋 } ) → ( 𝐺 Σg 𝑓 ) = ( 𝐺 Σg ( 𝐴 × { 𝑋 } ) ) )
30 29 eleq1d ⊢ ( 𝑓 = ( 𝐴 × { 𝑋 } ) → ( ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ↔ ( 𝐺 Σg ( 𝐴 × { 𝑋 } ) ) ∈ 𝑈 ) )
31 fconst6g ⊢ ( 𝑋 ∈ 𝐵 → ( 𝐴 × { 𝑋 } ) : 𝐴 ⟶ 𝐵 )
32 8 31 syl ⊢ ( 𝜑 → ( 𝐴 × { 𝑋 } ) : 𝐴 ⟶ 𝐵 )
33 2 fvexi ⊢ 𝐵 ∈ V
34 elmapg ⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ Fin ) → ( ( 𝐴 × { 𝑋 } ) ∈ ( 𝐵 ↑m 𝐴 ) ↔ ( 𝐴 × { 𝑋 } ) : 𝐴 ⟶ 𝐵 ) )
35 33 6 34 sylancr ⊢ ( 𝜑 → ( ( 𝐴 × { 𝑋 } ) ∈ ( 𝐵 ↑m 𝐴 ) ↔ ( 𝐴 × { 𝑋 } ) : 𝐴 ⟶ 𝐵 ) )
36 32 35 mpbird ⊢ ( 𝜑 → ( 𝐴 × { 𝑋 } ) ∈ ( 𝐵 ↑m 𝐴 ) )
37 fconstmpt ⊢ ( 𝐴 × { 𝑋 } ) = ( 𝑘 ∈ 𝐴 ↦ 𝑋 )
38 37 oveq2i ⊢ ( 𝐺 Σg ( 𝐴 × { 𝑋 } ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) )
39 cmnmnd ⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
40 4 39 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
41 2 3 gsumconst ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝐴 ) · 𝑋 ) )
42 40 6 8 41 syl3anc ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( ♯ ‘ 𝐴 ) · 𝑋 ) )
43 38 42 eqtrid ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐴 × { 𝑋 } ) ) = ( ( ♯ ‘ 𝐴 ) · 𝑋 ) )
44 43 9 eqeltrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐴 × { 𝑋 } ) ) ∈ 𝑈 )
45 30 36 44 elrabd ⊢ ( 𝜑 → ( 𝐴 × { 𝑋 } ) ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } )
46 tg2 ⊢ ( ( { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ∈ ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ) ∧ ( 𝐴 × { 𝑋 } ) ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) → ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ( ( 𝐴 × { 𝑋 } ) ∈ 𝑡 ∧ 𝑡 ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) )
47 28 45 46 syl2anc ⊢ ( 𝜑 → ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ( ( 𝐴 × { 𝑋 } ) ∈ 𝑡 ∧ 𝑡 ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) )
48 eleq2 ⊢ ( 𝑡 = 𝑥 → ( ( 𝐴 × { 𝑋 } ) ∈ 𝑡 ↔ ( 𝐴 × { 𝑋 } ) ∈ 𝑥 ) )
49 sseq1 ⊢ ( 𝑡 = 𝑥 → ( 𝑡 ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ↔ 𝑥 ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) )
50 48 49 anbi12d ⊢ ( 𝑡 = 𝑥 → ( ( ( 𝐴 × { 𝑋 } ) ∈ 𝑡 ∧ 𝑡 ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ↔ ( ( 𝐴 × { 𝑋 } ) ∈ 𝑥 ∧ 𝑥 ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) )
51 50 rexab2 ⊢ ( ∃ 𝑡 ∈ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) } ( ( 𝐴 × { 𝑋 } ) ∈ 𝑡 ∧ 𝑡 ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ↔ ∃ 𝑥 ( ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ 𝑥 ∧ 𝑥 ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) )
52 47 51 sylib ⊢ ( 𝜑 → ∃ 𝑥 ( ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ 𝑥 ∧ 𝑥 ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) )
53 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐵 = ∪ 𝐽 )
54 5 17 53 3syl ⊢ ( 𝜑 → 𝐵 = ∪ 𝐽 )
55 54 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → 𝐵 = ∪ 𝐽 )
56 55 ineq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ( 𝐵 ∩ ∩ ran 𝑔 ) = ( ∪ 𝐽 ∩ ∩ ran 𝑔 ) )
57 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → 𝐽 ∈ Top )
58 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → 𝑔 Fn 𝐴 )
59 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) )
60 fvconst2g ⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) = 𝐽 )
61 60 eleq2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ↔ ( 𝑔 ‘ 𝑦 ) ∈ 𝐽 ) )
62 61 ralbidva ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ 𝐽 ) )
63 57 62 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ( ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ 𝐽 ) )
64 59 63 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ 𝐽 )
65 ffnfv ⊢ ( 𝑔 : 𝐴 ⟶ 𝐽 ↔ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ 𝐽 ) )
66 58 64 65 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → 𝑔 : 𝐴 ⟶ 𝐽 )
67 66 frnd ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ran 𝑔 ⊆ 𝐽 )
68 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → 𝐴 ∈ Fin )
69 dffn4 ⊢ ( 𝑔 Fn 𝐴 ↔ 𝑔 : 𝐴 –onto→ ran 𝑔 )
70 58 69 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → 𝑔 : 𝐴 –onto→ ran 𝑔 )
71 fofi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑔 : 𝐴 –onto→ ran 𝑔 ) → ran 𝑔 ∈ Fin )
72 68 70 71 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ran 𝑔 ∈ Fin )
73 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
74 73 rintopn ⊢ ( ( 𝐽 ∈ Top ∧ ran 𝑔 ⊆ 𝐽 ∧ ran 𝑔 ∈ Fin ) → ( ∪ 𝐽 ∩ ∩ ran 𝑔 ) ∈ 𝐽 )
75 57 67 72 74 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ( ∪ 𝐽 ∩ ∩ ran 𝑔 ) ∈ 𝐽 )
76 56 75 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ( 𝐵 ∩ ∩ ran 𝑔 ) ∈ 𝐽 )
77 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → 𝑋 ∈ 𝐵 )
78 fconstmpt ⊢ ( 𝐴 × { 𝑋 } ) = ( 𝑦 ∈ 𝐴 ↦ 𝑋 )
79 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) )
80 78 79 eqeltrrid ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ( 𝑦 ∈ 𝐴 ↦ 𝑋 ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) )
81 mptelixpg ⊢ ( 𝐴 ∈ Fin → ( ( 𝑦 ∈ 𝐴 ↦ 𝑋 ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 𝑋 ∈ ( 𝑔 ‘ 𝑦 ) ) )
82 68 81 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ( ( 𝑦 ∈ 𝐴 ↦ 𝑋 ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 𝑋 ∈ ( 𝑔 ‘ 𝑦 ) ) )
83 80 82 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ∀ 𝑦 ∈ 𝐴 𝑋 ∈ ( 𝑔 ‘ 𝑦 ) )
84 eleq2 ⊢ ( 𝑧 = ( 𝑔 ‘ 𝑦 ) → ( 𝑋 ∈ 𝑧 ↔ 𝑋 ∈ ( 𝑔 ‘ 𝑦 ) ) )
85 84 ralrn ⊢ ( 𝑔 Fn 𝐴 → ( ∀ 𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧 ↔ ∀ 𝑦 ∈ 𝐴 𝑋 ∈ ( 𝑔 ‘ 𝑦 ) ) )
86 58 85 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ( ∀ 𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧 ↔ ∀ 𝑦 ∈ 𝐴 𝑋 ∈ ( 𝑔 ‘ 𝑦 ) ) )
87 83 86 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ∀ 𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧 )
88 elrint ⊢ ( 𝑋 ∈ ( 𝐵 ∩ ∩ ran 𝑔 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑧 ∈ ran 𝑔 𝑋 ∈ 𝑧 ) )
89 77 87 88 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → 𝑋 ∈ ( 𝐵 ∩ ∩ ran 𝑔 ) )
90 33 inex1 ⊢ ( 𝐵 ∩ ∩ ran 𝑔 ) ∈ V
91 ixpconstg ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐵 ∩ ∩ ran 𝑔 ) ∈ V ) → X 𝑦 ∈ 𝐴 ( 𝐵 ∩ ∩ ran 𝑔 ) = ( ( 𝐵 ∩ ∩ ran 𝑔 ) ↑m 𝐴 ) )
92 68 90 91 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → X 𝑦 ∈ 𝐴 ( 𝐵 ∩ ∩ ran 𝑔 ) = ( ( 𝐵 ∩ ∩ ran 𝑔 ) ↑m 𝐴 ) )
93 inss2 ⊢ ( 𝐵 ∩ ∩ ran 𝑔 ) ⊆ ∩ ran 𝑔
94 fnfvelrn ⊢ ( ( 𝑔 Fn 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑦 ) ∈ ran 𝑔 )
95 intss1 ⊢ ( ( 𝑔 ‘ 𝑦 ) ∈ ran 𝑔 → ∩ ran 𝑔 ⊆ ( 𝑔 ‘ 𝑦 ) )
96 94 95 syl ⊢ ( ( 𝑔 Fn 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ∩ ran 𝑔 ⊆ ( 𝑔 ‘ 𝑦 ) )
97 93 96 sstrid ⊢ ( ( 𝑔 Fn 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐵 ∩ ∩ ran 𝑔 ) ⊆ ( 𝑔 ‘ 𝑦 ) )
98 97 ralrimiva ⊢ ( 𝑔 Fn 𝐴 → ∀ 𝑦 ∈ 𝐴 ( 𝐵 ∩ ∩ ran 𝑔 ) ⊆ ( 𝑔 ‘ 𝑦 ) )
99 ss2ixp ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝐵 ∩ ∩ ran 𝑔 ) ⊆ ( 𝑔 ‘ 𝑦 ) → X 𝑦 ∈ 𝐴 ( 𝐵 ∩ ∩ ran 𝑔 ) ⊆ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) )
100 58 98 99 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → X 𝑦 ∈ 𝐴 ( 𝐵 ∩ ∩ ran 𝑔 ) ⊆ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) )
101 92 100 eqsstrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ( ( 𝐵 ∩ ∩ ran 𝑔 ) ↑m 𝐴 ) ⊆ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) )
102 ssrab ⊢ ( X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ↔ ( X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ ( 𝐵 ↑m 𝐴 ) ∧ ∀ 𝑓 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) )
103 102 simprbi ⊢ ( X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } → ∀ 𝑓 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 )
104 103 ad2antll ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ∀ 𝑓 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 )
105 ssralv ⊢ ( ( ( 𝐵 ∩ ∩ ran 𝑔 ) ↑m 𝐴 ) ⊆ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) → ( ∀ 𝑓 ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 → ∀ 𝑓 ∈ ( ( 𝐵 ∩ ∩ ran 𝑔 ) ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) )
106 101 104 105 sylc ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ∀ 𝑓 ∈ ( ( 𝐵 ∩ ∩ ran 𝑔 ) ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 )
107 eleq2 ⊢ ( 𝑢 = ( 𝐵 ∩ ∩ ran 𝑔 ) → ( 𝑋 ∈ 𝑢 ↔ 𝑋 ∈ ( 𝐵 ∩ ∩ ran 𝑔 ) ) )
108 oveq1 ⊢ ( 𝑢 = ( 𝐵 ∩ ∩ ran 𝑔 ) → ( 𝑢 ↑m 𝐴 ) = ( ( 𝐵 ∩ ∩ ran 𝑔 ) ↑m 𝐴 ) )
109 108 raleqdv ⊢ ( 𝑢 = ( 𝐵 ∩ ∩ ran 𝑔 ) → ( ∀ 𝑓 ∈ ( 𝑢 ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ↔ ∀ 𝑓 ∈ ( ( 𝐵 ∩ ∩ ran 𝑔 ) ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) )
110 107 109 anbi12d ⊢ ( 𝑢 = ( 𝐵 ∩ ∩ ran 𝑔 ) → ( ( 𝑋 ∈ 𝑢 ∧ ∀ 𝑓 ∈ ( 𝑢 ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) ↔ ( 𝑋 ∈ ( 𝐵 ∩ ∩ ran 𝑔 ) ∧ ∀ 𝑓 ∈ ( ( 𝐵 ∩ ∩ ran 𝑔 ) ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) ) )
111 110 rspcev ⊢ ( ( ( 𝐵 ∩ ∩ ran 𝑔 ) ∈ 𝐽 ∧ ( 𝑋 ∈ ( 𝐵 ∩ ∩ ran 𝑔 ) ∧ ∀ 𝑓 ∈ ( ( 𝐵 ∩ ∩ ran 𝑔 ) ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ ∀ 𝑓 ∈ ( 𝑢 ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) )
112 76 89 106 111 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ ∀ 𝑓 ∈ ( 𝑢 ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) )
113 112 ex ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) → ( ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) → ∃ 𝑢 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ ∀ 𝑓 ∈ ( 𝑢 ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) ) )
114 113 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) → ( ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) → ∃ 𝑢 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ ∀ 𝑓 ∈ ( 𝑢 ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) ) )
115 eleq2 ⊢ ( 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) → ( ( 𝐴 × { 𝑋 } ) ∈ 𝑥 ↔ ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) )
116 sseq1 ⊢ ( 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) → ( 𝑥 ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ↔ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) )
117 115 116 anbi12d ⊢ ( 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) → ( ( ( 𝐴 × { 𝑋 } ) ∈ 𝑥 ∧ 𝑥 ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ↔ ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) )
118 117 imbi1d ⊢ ( 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) → ( ( ( ( 𝐴 × { 𝑋 } ) ∈ 𝑥 ∧ 𝑥 ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) → ∃ 𝑢 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ ∀ 𝑓 ∈ ( 𝑢 ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) ) ↔ ( ( ( 𝐴 × { 𝑋 } ) ∈ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∧ X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) → ∃ 𝑢 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ ∀ 𝑓 ∈ ( 𝑢 ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) ) ) )
119 114 118 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ) → ( 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) → ( ( ( 𝐴 × { 𝑋 } ) ∈ 𝑥 ∧ 𝑥 ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) → ∃ 𝑢 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ ∀ 𝑓 ∈ ( 𝑢 ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) ) ) )
120 119 expimpd ⊢ ( 𝜑 → ( ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) → ( ( ( 𝐴 × { 𝑋 } ) ∈ 𝑥 ∧ 𝑥 ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) → ∃ 𝑢 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ ∀ 𝑓 ∈ ( 𝑢 ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) ) ) )
121 120 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) → ( ( ( 𝐴 × { 𝑋 } ) ∈ 𝑥 ∧ 𝑥 ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) → ∃ 𝑢 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ ∀ 𝑓 ∈ ( 𝑢 ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) ) ) )
122 121 impd ⊢ ( 𝜑 → ( ( ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ 𝑥 ∧ 𝑥 ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ ∀ 𝑓 ∈ ( 𝑢 ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) ) )
123 122 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑥 ( ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ∈ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴 ∖ 𝑧 ) ( 𝑔 ‘ 𝑦 ) = ∪ ( ( 𝐴 × { 𝐽 } ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦 ∈ 𝐴 ( 𝑔 ‘ 𝑦 ) ) ∧ ( ( 𝐴 × { 𝑋 } ) ∈ 𝑥 ∧ 𝑥 ⊆ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ( 𝐺 Σg 𝑓 ) ∈ 𝑈 } ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ ∀ 𝑓 ∈ ( 𝑢 ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) ) )
124 52 123 mpd ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝐽 ( 𝑋 ∈ 𝑢 ∧ ∀ 𝑓 ∈ ( 𝑢 ↑m 𝐴 ) ( 𝐺 Σg 𝑓 ) ∈ 𝑈 ) )