Metamath Proof Explorer

Theorem gsumvalx

Description: Expand out the substitutions in df-gsum . (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses gsumval.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumval.z ⊢ 0 = ( 0g ‘ 𝐺 )
gsumval.p ⊢ + = ( +g ‘ 𝐺 )
gsumval.o ⊢ 𝑂 = { 𝑠 ∈ 𝐵 ∣ ∀ 𝑡 ∈ 𝐵 ( ( 𝑠 + 𝑡 ) = 𝑡 ∧ ( 𝑡 + 𝑠 ) = 𝑡 ) }
gsumval.w ⊢ ( 𝜑 → 𝑊 = ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) )
gsumval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
gsumvalx.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
gsumvalx.a ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
Assertion gsumvalx ( 𝜑 → ( 𝐺 Σg 𝐹 ) = if ( ran 𝐹 ⊆ 𝑂 , 0 , if ( 𝐴 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumval.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumval.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsumval.p ⊢ + = ( +g ‘ 𝐺 )
4 gsumval.o ⊢ 𝑂 = { 𝑠 ∈ 𝐵 ∣ ∀ 𝑡 ∈ 𝐵 ( ( 𝑠 + 𝑡 ) = 𝑡 ∧ ( 𝑡 + 𝑠 ) = 𝑡 ) }
5 gsumval.w ⊢ ( 𝜑 → 𝑊 = ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) )
6 gsumval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
7 gsumvalx.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
8 gsumvalx.a ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
9 df-gsum ⊢ Σg = ( 𝑤 ∈ V , 𝑔 ∈ V ↦ ⦋ { 𝑥 ∈ ( Base ‘ 𝑤 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 ) } / 𝑜 ⦌ if ( ran 𝑔 ⊆ 𝑜 , ( 0g ‘ 𝑤 ) , if ( dom 𝑔 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑔 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑔 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 [ ( ◡ 𝑔 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) ) ) )
10 9 a1i ⊢ ( 𝜑 → Σg = ( 𝑤 ∈ V , 𝑔 ∈ V ↦ ⦋ { 𝑥 ∈ ( Base ‘ 𝑤 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 ) } / 𝑜 ⦌ if ( ran 𝑔 ⊆ 𝑜 , ( 0g ‘ 𝑤 ) , if ( dom 𝑔 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑔 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑔 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 [ ( ◡ 𝑔 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) ) ) ) )
11 simprl ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → 𝑤 = 𝐺 )
12 11 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → ( Base ‘ 𝑤 ) = ( Base ‘ 𝐺 ) )
13 12 1 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → ( Base ‘ 𝑤 ) = 𝐵 )
14 11 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → ( +g ‘ 𝑤 ) = ( +g ‘ 𝐺 ) )
15 14 3 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → ( +g ‘ 𝑤 ) = + )
16 15 oveqd ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = ( 𝑥 + 𝑦 ) )
17 16 eqeq1d ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → ( ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 ↔ ( 𝑥 + 𝑦 ) = 𝑦 ) )
18 15 oveqd ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = ( 𝑦 + 𝑥 ) )
19 18 eqeq1d ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → ( ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 ↔ ( 𝑦 + 𝑥 ) = 𝑦 ) )
20 17 19 anbi12d ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → ( ( ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 ) ↔ ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) )
21 13 20 raleqbidv ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) )
22 13 21 rabeqbidv ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → { 𝑥 ∈ ( Base ‘ 𝑤 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 ) } = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) } )
23 oveq2 ⊢ ( 𝑡 = 𝑦 → ( 𝑠 + 𝑡 ) = ( 𝑠 + 𝑦 ) )
24 id ⊢ ( 𝑡 = 𝑦 → 𝑡 = 𝑦 )
25 23 24 eqeq12d ⊢ ( 𝑡 = 𝑦 → ( ( 𝑠 + 𝑡 ) = 𝑡 ↔ ( 𝑠 + 𝑦 ) = 𝑦 ) )
26 oveq1 ⊢ ( 𝑡 = 𝑦 → ( 𝑡 + 𝑠 ) = ( 𝑦 + 𝑠 ) )
27 26 24 eqeq12d ⊢ ( 𝑡 = 𝑦 → ( ( 𝑡 + 𝑠 ) = 𝑡 ↔ ( 𝑦 + 𝑠 ) = 𝑦 ) )
28 25 27 anbi12d ⊢ ( 𝑡 = 𝑦 → ( ( ( 𝑠 + 𝑡 ) = 𝑡 ∧ ( 𝑡 + 𝑠 ) = 𝑡 ) ↔ ( ( 𝑠 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑠 ) = 𝑦 ) ) )
29 28 cbvralvw ⊢ ( ∀ 𝑡 ∈ 𝐵 ( ( 𝑠 + 𝑡 ) = 𝑡 ∧ ( 𝑡 + 𝑠 ) = 𝑡 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝑠 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑠 ) = 𝑦 ) )
30 oveq1 ⊢ ( 𝑠 = 𝑥 → ( 𝑠 + 𝑦 ) = ( 𝑥 + 𝑦 ) )
31 30 eqeq1d ⊢ ( 𝑠 = 𝑥 → ( ( 𝑠 + 𝑦 ) = 𝑦 ↔ ( 𝑥 + 𝑦 ) = 𝑦 ) )
32 31 ovanraleqv ⊢ ( 𝑠 = 𝑥 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑠 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑠 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) )
33 29 32 bitrid ⊢ ( 𝑠 = 𝑥 → ( ∀ 𝑡 ∈ 𝐵 ( ( 𝑠 + 𝑡 ) = 𝑡 ∧ ( 𝑡 + 𝑠 ) = 𝑡 ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) )
34 33 cbvrabv ⊢ { 𝑠 ∈ 𝐵 ∣ ∀ 𝑡 ∈ 𝐵 ( ( 𝑠 + 𝑡 ) = 𝑡 ∧ ( 𝑡 + 𝑠 ) = 𝑡 ) } = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) }
35 4 34 eqtri ⊢ 𝑂 = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) }
36 22 35 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → { 𝑥 ∈ ( Base ‘ 𝑤 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 ) } = 𝑂 )
37 36 csbeq1d ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → ⦋ { 𝑥 ∈ ( Base ‘ 𝑤 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 ) } / 𝑜 ⦌ if ( ran 𝑔 ⊆ 𝑜 , ( 0g ‘ 𝑤 ) , if ( dom 𝑔 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑔 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑔 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 [ ( ◡ 𝑔 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) ) ) = ⦋ 𝑂 / 𝑜 ⦌ if ( ran 𝑔 ⊆ 𝑜 , ( 0g ‘ 𝑤 ) , if ( dom 𝑔 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑔 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑔 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 [ ( ◡ 𝑔 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) ) ) )
38 1 fvexi ⊢ 𝐵 ∈ V
39 4 38 rabex2 ⊢ 𝑂 ∈ V
40 39 a1i ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → 𝑂 ∈ V )
41 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → 𝑔 = 𝐹 )
42 41 rneqd ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ran 𝑔 = ran 𝐹 )
43 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → 𝑜 = 𝑂 )
44 42 43 sseq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( ran 𝑔 ⊆ 𝑜 ↔ ran 𝐹 ⊆ 𝑂 ) )
45 11 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → 𝑤 = 𝐺 )
46 45 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( 0g ‘ 𝑤 ) = ( 0g ‘ 𝐺 ) )
47 46 2 eqtr4di ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( 0g ‘ 𝑤 ) = 0 )
48 41 dmeqd ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → dom 𝑔 = dom 𝐹 )
49 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → dom 𝐹 = 𝐴 )
50 48 49 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → dom 𝑔 = 𝐴 )
51 50 eleq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( dom 𝑔 ∈ ran ... ↔ 𝐴 ∈ ran ... ) )
52 50 eqeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( dom 𝑔 = ( 𝑚 ... 𝑛 ) ↔ 𝐴 = ( 𝑚 ... 𝑛 ) ) )
53 15 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( +g ‘ 𝑤 ) = + )
54 53 seqeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑔 ) = seq 𝑚 ( + , 𝑔 ) )
55 41 seqeq3d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → seq 𝑚 ( + , 𝑔 ) = seq 𝑚 ( + , 𝐹 ) )
56 54 55 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑔 ) = seq 𝑚 ( + , 𝐹 ) )
57 56 fveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑔 ) ‘ 𝑛 ) = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) )
58 57 eqeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑔 ) ‘ 𝑛 ) ↔ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) )
59 52 58 anbi12d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( ( dom 𝑔 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑔 ) ‘ 𝑛 ) ) ↔ ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) )
60 59 rexbidv ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑔 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑔 ) ‘ 𝑛 ) ) ↔ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) )
61 60 exbidv ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑔 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑔 ) ‘ 𝑛 ) ) ↔ ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) )
62 61 iotabidv ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑔 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑔 ) ‘ 𝑛 ) ) ) = ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) )
63 43 difeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( V ∖ 𝑜 ) = ( V ∖ 𝑂 ) )
64 63 imaeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( ◡ 𝐹 “ ( V ∖ 𝑜 ) ) = ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) )
65 41 cnveqd ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ◡ 𝑔 = ◡ 𝐹 )
66 65 imaeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( ◡ 𝑔 “ ( V ∖ 𝑜 ) ) = ( ◡ 𝐹 “ ( V ∖ 𝑜 ) ) )
67 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → 𝑊 = ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) )
68 64 66 67 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( ◡ 𝑔 “ ( V ∖ 𝑜 ) ) = 𝑊 )
69 68 sbceq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( [ ( ◡ 𝑔 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ↔ [ 𝑊 / 𝑦 ] ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) )
70 cnvexg ⊢ ( 𝐹 ∈ 𝑋 → ◡ 𝐹 ∈ V )
71 imaexg ⊢ ( ◡ 𝐹 ∈ V → ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ∈ V )
72 7 70 71 3syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ∈ V )
73 5 72 eqeltrd ⊢ ( 𝜑 → 𝑊 ∈ V )
74 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → 𝑊 ∈ V )
75 fveq2 ⊢ ( 𝑦 = 𝑊 → ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑊 ) )
76 75 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) ∧ 𝑦 = 𝑊 ) → ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑊 ) )
77 76 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) ∧ 𝑦 = 𝑊 ) → ( 1 ... ( ♯ ‘ 𝑦 ) ) = ( 1 ... ( ♯ ‘ 𝑊 ) ) )
78 77 f1oeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) ∧ 𝑦 = 𝑊 ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ↔ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑦 ) )
79 f1oeq3 ⊢ ( 𝑦 = 𝑊 → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑦 ↔ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) )
80 79 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) ∧ 𝑦 = 𝑊 ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑦 ↔ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) )
81 78 80 bitrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) ∧ 𝑦 = 𝑊 ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ↔ 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ) )
82 53 seqeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) = seq 1 ( + , ( 𝑔 ∘ 𝑓 ) ) )
83 41 coeq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( 𝑔 ∘ 𝑓 ) = ( 𝐹 ∘ 𝑓 ) )
84 83 seqeq3d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → seq 1 ( + , ( 𝑔 ∘ 𝑓 ) ) = seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) )
85 82 84 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) = seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) )
86 85 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) ∧ 𝑦 = 𝑊 ) → seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) = seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) )
87 86 76 fveq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) ∧ 𝑦 = 𝑊 ) → ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑦 ) ) = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) )
88 87 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) ∧ 𝑦 = 𝑊 ) → ( 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ↔ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) )
89 81 88 anbi12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) ∧ 𝑦 = 𝑊 ) → ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ↔ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) )
90 74 89 sbcied ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( [ 𝑊 / 𝑦 ] ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ↔ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) )
91 69 90 bitrd ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( [ ( ◡ 𝑔 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ↔ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) )
92 91 exbidv ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( ∃ 𝑓 [ ( ◡ 𝑔 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) )
93 92 iotabidv ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → ( ℩ 𝑥 ∃ 𝑓 [ ( ◡ 𝑔 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) = ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) )
94 51 62 93 ifbieq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → if ( dom 𝑔 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑔 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑔 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 [ ( ◡ 𝑔 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) ) = if ( 𝐴 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ) )
95 44 47 94 ifbieq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) ∧ 𝑜 = 𝑂 ) → if ( ran 𝑔 ⊆ 𝑜 , ( 0g ‘ 𝑤 ) , if ( dom 𝑔 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑔 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑔 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 [ ( ◡ 𝑔 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) ) ) = if ( ran 𝐹 ⊆ 𝑂 , 0 , if ( 𝐴 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ) ) )
96 40 95 csbied ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → ⦋ 𝑂 / 𝑜 ⦌ if ( ran 𝑔 ⊆ 𝑜 , ( 0g ‘ 𝑤 ) , if ( dom 𝑔 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑔 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑔 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 [ ( ◡ 𝑔 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) ) ) = if ( ran 𝐹 ⊆ 𝑂 , 0 , if ( 𝐴 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ) ) )
97 37 96 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → ⦋ { 𝑥 ∈ ( Base ‘ 𝑤 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 ) } / 𝑜 ⦌ if ( ran 𝑔 ⊆ 𝑜 , ( 0g ‘ 𝑤 ) , if ( dom 𝑔 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑔 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑔 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 [ ( ◡ 𝑔 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑔 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) ) ) = if ( ran 𝐹 ⊆ 𝑂 , 0 , if ( 𝐴 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ) ) )
98 6 elexd ⊢ ( 𝜑 → 𝐺 ∈ V )
99 7 elexd ⊢ ( 𝜑 → 𝐹 ∈ V )
100 2 fvexi ⊢ 0 ∈ V
101 iotaex ⊢ ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) ∈ V
102 iotaex ⊢ ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ∈ V
103 101 102 ifex ⊢ if ( 𝐴 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ) ∈ V
104 100 103 ifex ⊢ if ( ran 𝐹 ⊆ 𝑂 , 0 , if ( 𝐴 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ) ) ∈ V
105 104 a1i ⊢ ( 𝜑 → if ( ran 𝐹 ⊆ 𝑂 , 0 , if ( 𝐴 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ) ) ∈ V )
106 10 97 98 99 105 ovmpod ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = if ( ran 𝐹 ⊆ 𝑂 , 0 , if ( 𝐴 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ) ) )