Step | Hyp | Ref
| Expression |
1 | | df-prod 15496 |
. 2
⊢
∏𝑘 ∈
𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) |
2 | | fvex 6749 |
. . 3
⊢ (seq1(
· , 𝐺)‘𝑀) ∈ V |
3 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑗if(𝑘 ∈ 𝐴, 𝐵, 1) |
4 | | nfv 1922 |
. . . . . . . . . 10
⊢
Ⅎ𝑘 𝑗 ∈ 𝐴 |
5 | | nfcsb1v 3851 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 |
6 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑘1 |
7 | 4, 5, 6 | nfif 4484 |
. . . . . . . . 9
⊢
Ⅎ𝑘if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 1) |
8 | | eleq1w 2821 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴)) |
9 | | csbeq1a 3840 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → 𝐵 = ⦋𝑗 / 𝑘⦌𝐵) |
10 | 8, 9 | ifbieq1d 4478 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → if(𝑘 ∈ 𝐴, 𝐵, 1) = if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 1)) |
11 | 3, 7, 10 | cbvmpt 5171 |
. . . . . . . 8
⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑗 ∈ ℤ ↦ if(𝑗 ∈ 𝐴, ⦋𝑗 / 𝑘⦌𝐵, 1)) |
12 | | fprod.4 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
13 | 12 | ralrimiva 3106 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
14 | 5 | nfel1 2921 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ |
15 | 9 | eleq1d 2823 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝐵 ∈ ℂ ↔ ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ)) |
16 | 14, 15 | rspc 3538 |
. . . . . . . . 9
⊢ (𝑗 ∈ 𝐴 → (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ)) |
17 | 13, 16 | mpan9 510 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ⦋𝑗 / 𝑘⦌𝐵 ∈ ℂ) |
18 | | fveq2 6736 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑖 → (𝑓‘𝑛) = (𝑓‘𝑖)) |
19 | 18 | csbeq1d 3830 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵) |
20 | | csbcow 3841 |
. . . . . . . . . 10
⊢
⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑘⦌𝐵 |
21 | 19, 20 | eqtr4di 2797 |
. . . . . . . . 9
⊢ (𝑛 = 𝑖 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵) |
22 | 21 | cbvmptv 5173 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦
⦋(𝑓‘𝑛) / 𝑘⦌𝐵) = (𝑖 ∈ ℕ ↦ ⦋(𝑓‘𝑖) / 𝑗⦌⦋𝑗 / 𝑘⦌𝐵) |
23 | 11, 17, 22 | prodmo 15526 |
. . . . . . 7
⊢ (𝜑 → ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) |
24 | | fprod.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℕ) |
25 | | fprod.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:(1...𝑀)–1-1-onto→𝐴) |
26 | | f1of 6680 |
. . . . . . . . . . . 12
⊢ (𝐹:(1...𝑀)–1-1-onto→𝐴 → 𝐹:(1...𝑀)⟶𝐴) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:(1...𝑀)⟶𝐴) |
28 | | ovex 7265 |
. . . . . . . . . . 11
⊢
(1...𝑀) ∈
V |
29 | | fex 7061 |
. . . . . . . . . . 11
⊢ ((𝐹:(1...𝑀)⟶𝐴 ∧ (1...𝑀) ∈ V) → 𝐹 ∈ V) |
30 | 27, 28, 29 | sylancl 589 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ V) |
31 | | nnuz 12502 |
. . . . . . . . . . . . 13
⊢ ℕ =
(ℤ≥‘1) |
32 | 24, 31 | eleqtrdi 2849 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
33 | | fprod.5 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐺‘𝑛) = 𝐶) |
34 | | elfznn 13166 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (1...𝑀) → 𝑛 ∈ ℕ) |
35 | | fvex 6749 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺‘𝑛) ∈ V |
36 | 33, 35 | eqeltrrdi 2848 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → 𝐶 ∈ V) |
37 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ ↦ 𝐶) = (𝑛 ∈ ℕ ↦ 𝐶) |
38 | 37 | fvmpt2 6848 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ℕ ∧ 𝐶 ∈ V) → ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) = 𝐶) |
39 | 34, 36, 38 | syl2an2 686 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) = 𝐶) |
40 | 33, 39 | eqtr4d 2781 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑀)) → (𝐺‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛)) |
41 | 40 | ralrimiva 3106 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛)) |
42 | | nffvmpt1 6747 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑛((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘) |
43 | 42 | nfeq2 2922 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛(𝐺‘𝑘) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘) |
44 | | fveq2 6736 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘)) |
45 | | fveq2 6736 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑘 → ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘)) |
46 | 44, 45 | eqeq12d 2754 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑘 → ((𝐺‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) ↔ (𝐺‘𝑘) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘))) |
47 | 43, 46 | rspc 3538 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑀) → (∀𝑛 ∈ (1...𝑀)(𝐺‘𝑛) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑛) → (𝐺‘𝑘) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘))) |
48 | 41, 47 | mpan9 510 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑀)) → (𝐺‘𝑘) = ((𝑛 ∈ ℕ ↦ 𝐶)‘𝑘)) |
49 | 32, 48 | seqfveq 13627 |
. . . . . . . . . . 11
⊢ (𝜑 → (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀)) |
50 | 25, 49 | jca 515 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀))) |
51 | | f1oeq1 6668 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → (𝑓:(1...𝑀)–1-1-onto→𝐴 ↔ 𝐹:(1...𝑀)–1-1-onto→𝐴)) |
52 | | fveq1 6735 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = 𝐹 → (𝑓‘𝑛) = (𝐹‘𝑛)) |
53 | 52 | csbeq1d 3830 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝐹 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝐹‘𝑛) / 𝑘⦌𝐵) |
54 | | fvex 6749 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹‘𝑛) ∈ V |
55 | | fprod.1 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = (𝐹‘𝑛) → 𝐵 = 𝐶) |
56 | 54, 55 | csbie 3862 |
. . . . . . . . . . . . . . . 16
⊢
⦋(𝐹‘𝑛) / 𝑘⦌𝐵 = 𝐶 |
57 | 53, 56 | eqtrdi 2795 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝐹 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = 𝐶) |
58 | 57 | mpteq2dv 5166 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝐹 → (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) = (𝑛 ∈ ℕ ↦ 𝐶)) |
59 | 58 | seqeq3d 13609 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝐹 → seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)) = seq1( · , (𝑛 ∈ ℕ ↦ 𝐶))) |
60 | 59 | fveq1d 6738 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝐹 → (seq1( · , (𝑛 ∈ ℕ ↦
⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀)) |
61 | 60 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → ((seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀) ↔ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀))) |
62 | 51, 61 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐹 → ((𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀)) ↔ (𝐹:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ 𝐶))‘𝑀)))) |
63 | 30, 50, 62 | spcedv 3526 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀))) |
64 | | oveq2 7240 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑀 → (1...𝑚) = (1...𝑀)) |
65 | 64 | f1oeq2d 6676 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑀 → (𝑓:(1...𝑚)–1-1-onto→𝐴 ↔ 𝑓:(1...𝑀)–1-1-onto→𝐴)) |
66 | | fveq2 6736 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑀 → (seq1( · , (𝑛 ∈ ℕ ↦
⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀)) |
67 | 66 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑀 → ((seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) ↔ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀))) |
68 | 65, 67 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑀 → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ (𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀)))) |
69 | 68 | exbidv 1929 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑀 → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀)))) |
70 | 69 | rspcev 3550 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℕ ∧
∃𝑓(𝑓:(1...𝑀)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑀))) → ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) |
71 | 24, 63, 70 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) |
72 | 71 | olcd 874 |
. . . . . . 7
⊢ (𝜑 → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) |
73 | | breq2 5072 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (seq1( · , 𝐺)‘𝑀) → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , 𝐺)‘𝑀))) |
74 | 73 | 3anbi3d 1444 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (seq1( · , 𝐺)‘𝑀) → ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , 𝐺)‘𝑀)))) |
75 | 74 | rexbidv 3224 |
. . . . . . . . . . . 12
⊢ (𝑥 = (seq1( · , 𝐺)‘𝑀) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , 𝐺)‘𝑀)))) |
76 | | eqeq1 2742 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (seq1( · , 𝐺)‘𝑀) → (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) ↔ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) |
77 | 76 | anbi2d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (seq1( · , 𝐺)‘𝑀) → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ (𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) |
78 | 77 | exbidv 1929 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (seq1( · , 𝐺)‘𝑀) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) |
79 | 78 | rexbidv 3224 |
. . . . . . . . . . . 12
⊢ (𝑥 = (seq1( · , 𝐺)‘𝑀) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) |
80 | 75, 79 | orbi12d 919 |
. . . . . . . . . . 11
⊢ (𝑥 = (seq1( · , 𝐺)‘𝑀) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))) |
81 | 80 | moi2 3644 |
. . . . . . . . . 10
⊢ ((((seq1(
· , 𝐺)‘𝑀) ∈ V ∧ ∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) ∧ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))) → 𝑥 = (seq1( · , 𝐺)‘𝑀)) |
82 | 2, 81 | mpanl1 700 |
. . . . . . . . 9
⊢
((∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ∧ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))) → 𝑥 = (seq1( · , 𝐺)‘𝑀)) |
83 | 82 | ancom2s 650 |
. . . . . . . 8
⊢
((∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ∧ ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))) → 𝑥 = (seq1( · , 𝐺)‘𝑀)) |
84 | 83 | expr 460 |
. . . . . . 7
⊢
((∃*𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ∧ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ (seq1( · , 𝐺)‘𝑀)) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ (seq1( · , 𝐺)‘𝑀) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) → 𝑥 = (seq1( · , 𝐺)‘𝑀))) |
85 | 23, 72, 84 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) → 𝑥 = (seq1( · , 𝐺)‘𝑀))) |
86 | 72, 80 | syl5ibrcom 250 |
. . . . . 6
⊢ (𝜑 → (𝑥 = (seq1( · , 𝐺)‘𝑀) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))) |
87 | 85, 86 | impbid 215 |
. . . . 5
⊢ (𝜑 → ((∃𝑚 ∈ ℤ (𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ↔ 𝑥 = (seq1( · , 𝐺)‘𝑀))) |
88 | 87 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (seq1( · , 𝐺)‘𝑀) ∈ V) → ((∃𝑚 ∈ ℤ (𝐴 ⊆
(ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ↔ 𝑥 = (seq1( · , 𝐺)‘𝑀))) |
89 | 88 | iota5 6381 |
. . 3
⊢ ((𝜑 ∧ (seq1( · , 𝐺)‘𝑀) ∈ V) → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) = (seq1( · , 𝐺)‘𝑀)) |
90 | 2, 89 | mpan2 691 |
. 2
⊢ (𝜑 → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈
(ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) = (seq1( · , 𝐺)‘𝑀)) |
91 | 1, 90 | eqtrid 2790 |
1
⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = (seq1( · , 𝐺)‘𝑀)) |