Metamath Proof Explorer

Theorem fprod

Description: The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017)

Ref Expression
Hypotheses fprod.1 ⊢ ( 𝑘 = ( 𝐹 ‘ 𝑛 ) → 𝐵 = 𝐶 )
fprod.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fprod.3 ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 )
fprod.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
fprod.5 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑛 ) = 𝐶 )
Assertion fprod ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 fprod.1 ⊢ ( 𝑘 = ( 𝐹 ‘ 𝑛 ) → 𝐵 = 𝐶 )
2 fprod.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3 fprod.3 ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 )
4 fprod.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
5 fprod.5 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑛 ) = 𝐶 )
6 df-prod ⊢ ∏ 𝑘 ∈ 𝐴 𝐵 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) )
7 fvex ⊢ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ∈ V
8 nfcv ⊢ Ⅎ 𝑗 if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 )
9 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝐴
10 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
11 nfcv ⊢ Ⅎ 𝑘 1
12 9 10 11 nfif ⊢ Ⅎ 𝑘 if ( 𝑗 ∈ 𝐴 , ⦋ 𝑗 / 𝑘 ⦌ 𝐵 , 1 )
13 eleq1w ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴 ) )
14 csbeq1a ⊢ ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
15 13 14 ifbieq1d ⊢ ( 𝑘 = 𝑗 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = if ( 𝑗 ∈ 𝐴 , ⦋ 𝑗 / 𝑘 ⦌ 𝐵 , 1 ) )
16 8 12 15 cbvmpt ⊢ ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) = ( 𝑗 ∈ ℤ ↦ if ( 𝑗 ∈ 𝐴 , ⦋ 𝑗 / 𝑘 ⦌ 𝐵 , 1 ) )
17 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ )
18 10 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ
19 14 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
20 18 19 rspc ⊢ ( 𝑗 ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
21 17 20 mpan9 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℂ )
22 fveq2 ⊢ ( 𝑛 = 𝑖 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑖 ) )
23 22 csbeq1d ⊢ ( 𝑛 = 𝑖 → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ 𝑖 ) / 𝑘 ⦌ 𝐵 )
24 csbcow ⊢ ⦋ ( 𝑓 ‘ 𝑖 ) / 𝑗 ⦌ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ 𝑖 ) / 𝑘 ⦌ 𝐵
25 23 24 syl6eqr ⊢ ( 𝑛 = 𝑖 → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ 𝑖 ) / 𝑗 ⦌ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
26 25 cbvmptv ⊢ ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) = ( 𝑖 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑖 ) / 𝑗 ⦌ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
27 16 21 26 prodmo ⊢ ( 𝜑 → ∃* 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) )
28 f1of ⊢ ( 𝐹 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 → 𝐹 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
29 3 28 syl ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
30 ovex ⊢ ( 1 ... 𝑀 ) ∈ V
31 fex ⊢ ( ( 𝐹 : ( 1 ... 𝑀 ) ⟶ 𝐴 ∧ ( 1 ... 𝑀 ) ∈ V ) → 𝐹 ∈ V )
32 29 30 31 sylancl ⊢ ( 𝜑 → 𝐹 ∈ V )
33 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
34 2 33 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
35 elfznn ⊢ ( 𝑛 ∈ ( 1 ... 𝑀 ) → 𝑛 ∈ ℕ )
36 fvex ⊢ ( 𝐺 ‘ 𝑛 ) ∈ V
37 5 36 eqeltrrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → 𝐶 ∈ V )
38 eqid ⊢ ( 𝑛 ∈ ℕ ↦ 𝐶 ) = ( 𝑛 ∈ ℕ ↦ 𝐶 )
39 38 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐶 ∈ V ) → ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑛 ) = 𝐶 )
40 35 37 39 syl2an2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑛 ) = 𝐶 )
41 5 40 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑛 ) )
42 41 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ( 1 ... 𝑀 ) ( 𝐺 ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑛 ) )
43 nffvmpt1 ⊢ Ⅎ 𝑛 ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑘 )
44 43 nfeq2 ⊢ Ⅎ 𝑛 ( 𝐺 ‘ 𝑘 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑘 )
45 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑘 ) )
46 fveq2 ⊢ ( 𝑛 = 𝑘 → ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑘 ) )
47 45 46 eqeq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐺 ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑛 ) ↔ ( 𝐺 ‘ 𝑘 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑘 ) ) )
48 44 47 rspc ⊢ ( 𝑘 ∈ ( 1 ... 𝑀 ) → ( ∀ 𝑛 ∈ ( 1 ... 𝑀 ) ( 𝐺 ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑛 ) → ( 𝐺 ‘ 𝑘 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑘 ) ) )
49 42 48 mpan9 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝑘 ) = ( ( 𝑛 ∈ ℕ ↦ 𝐶 ) ‘ 𝑘 ) )
50 34 49 seqfveq ⊢ ( 𝜑 → ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ 𝐶 ) ) ‘ 𝑀 ) )
51 3 50 jca ⊢ ( 𝜑 → ( 𝐹 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ 𝐶 ) ) ‘ 𝑀 ) ) )
52 f1oeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ↔ 𝐹 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ) )
53 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) )
54 53 csbeq1d ⊢ ( 𝑓 = 𝐹 → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 )
55 fvex ⊢ ( 𝐹 ‘ 𝑛 ) ∈ V
56 55 1 csbie ⊢ ⦋ ( 𝐹 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = 𝐶
57 54 56 syl6eq ⊢ ( 𝑓 = 𝐹 → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = 𝐶 )
58 57 mpteq2dv ⊢ ( 𝑓 = 𝐹 → ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) = ( 𝑛 ∈ ℕ ↦ 𝐶 ) )
59 58 seqeq3d ⊢ ( 𝑓 = 𝐹 → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) = seq 1 ( · , ( 𝑛 ∈ ℕ ↦ 𝐶 ) ) )
60 59 fveq1d ⊢ ( 𝑓 = 𝐹 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ 𝐶 ) ) ‘ 𝑀 ) )
61 60 eqeq2d ⊢ ( 𝑓 = 𝐹 → ( ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑀 ) ↔ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ 𝐶 ) ) ‘ 𝑀 ) ) )
62 52 61 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑀 ) ) ↔ ( 𝐹 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ 𝐶 ) ) ‘ 𝑀 ) ) ) )
63 32 51 62 spcedv ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑀 ) ) )
64 oveq2 ⊢ ( 𝑚 = 𝑀 → ( 1 ... 𝑚 ) = ( 1 ... 𝑀 ) )
65 64 f1oeq2d ⊢ ( 𝑚 = 𝑀 → ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ↔ 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ) )
66 fveq2 ⊢ ( 𝑚 = 𝑀 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑀 ) )
67 66 eqeq2d ⊢ ( 𝑚 = 𝑀 → ( ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ↔ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑀 ) ) )
68 65 67 anbi12d ⊢ ( 𝑚 = 𝑀 → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑀 ) ) ) )
69 68 exbidv ⊢ ( 𝑚 = 𝑀 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑀 ) ) ) )
70 69 rspcev ⊢ ( ( 𝑀 ∈ ℕ ∧ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑀 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑀 ) ) ) → ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) )
71 2 63 70 syl2anc ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) )
72 71 olcd ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) )
73 breq2 ⊢ ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ↔ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) )
74 73 3anbi3d ⊢ ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ↔ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) ) )
75 74 rexbidv ⊢ ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ↔ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) ) )
76 eqeq1 ⊢ ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ↔ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) )
77 76 anbi2d ⊢ ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) )
78 77 exbidv ⊢ ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) )
79 78 rexbidv ⊢ ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) )
80 75 79 orbi12d ⊢ ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ↔ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ) )
81 80 moi2 ⊢ ( ( ( ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ∈ V ∧ ∃* 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ) ∧ ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ∧ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ) ) → 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) )
82 7 81 mpanl1 ⊢ ( ( ∃* 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ∧ ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ∧ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ) ) → 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) )
83 82 ancom2s ⊢ ( ( ∃* 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ∧ ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ∧ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ) ) → 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) )
84 83 expr ⊢ ( ( ∃* 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ∧ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ) → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) → 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) )
85 27 72 84 syl2anc ⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) → 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) )
86 72 80 syl5ibrcom ⊢ ( 𝜑 → ( 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ) )
87 85 86 impbid ⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ↔ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) )
88 87 adantr ⊢ ( ( 𝜑 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ∈ V ) → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ↔ 𝑥 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ) )
89 88 iota5 ⊢ ( ( 𝜑 ∧ ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) ∈ V ) → ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ) = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) )
90 7 89 mpan2 ⊢ ( 𝜑 → ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ) = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) )
91 6 90 syl5eq ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = ( seq 1 ( · , 𝐺 ) ‘ 𝑀 ) )