| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eluzelz |
⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) → 𝑛 ∈ ℤ ) |
| 2 |
1
|
adantl |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) → 𝑛 ∈ ℤ ) |
| 3 |
|
nfra1 |
⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) |
| 4 |
|
rsp |
⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( 𝑘 ∈ 𝐴 → ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ) ) |
| 5 |
4
|
adantr |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ 𝐴 → ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ) ) |
| 6 |
|
ifeq1 |
⊢ ( ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐵 ) , ( I ‘ 1 ) ) = if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐶 ) , ( I ‘ 1 ) ) ) |
| 7 |
5 6
|
syl6 |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐵 ) , ( I ‘ 1 ) ) = if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐶 ) , ( I ‘ 1 ) ) ) ) |
| 8 |
|
iffalse |
⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐵 ) , ( I ‘ 1 ) ) = ( I ‘ 1 ) ) |
| 9 |
|
iffalse |
⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐶 ) , ( I ‘ 1 ) ) = ( I ‘ 1 ) ) |
| 10 |
8 9
|
eqtr4d |
⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐵 ) , ( I ‘ 1 ) ) = if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐶 ) , ( I ‘ 1 ) ) ) |
| 11 |
7 10
|
pm2.61d1 |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑘 ∈ ℤ ) → if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐵 ) , ( I ‘ 1 ) ) = if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐶 ) , ( I ‘ 1 ) ) ) |
| 12 |
|
fvif |
⊢ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) = if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐵 ) , ( I ‘ 1 ) ) |
| 13 |
|
fvif |
⊢ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) = if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐶 ) , ( I ‘ 1 ) ) |
| 14 |
11 12 13
|
3eqtr4g |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑘 ∈ ℤ ) → ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) = ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) |
| 15 |
3 14
|
mpteq2da |
⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) = ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ) |
| 16 |
15
|
adantr |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) = ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ) |
| 17 |
16
|
fveq1d |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ‘ 𝑥 ) ) |
| 18 |
17
|
adantlr |
⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ‘ 𝑥 ) ) |
| 19 |
|
eqid |
⊢ ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) |
| 20 |
|
eqid |
⊢ ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) = ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) |
| 21 |
19 20
|
fvmptex |
⊢ ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ‘ 𝑥 ) |
| 22 |
|
eqid |
⊢ ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) |
| 23 |
|
eqid |
⊢ ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) = ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) |
| 24 |
22 23
|
fvmptex |
⊢ ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ‘ 𝑥 ) |
| 25 |
18 21 24
|
3eqtr4g |
⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ‘ 𝑥 ) ) |
| 26 |
2 25
|
seqfeq |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) → seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) = seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ) |
| 27 |
26
|
breq1d |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ↔ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ) |
| 28 |
27
|
anbi2d |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ) ) |
| 29 |
28
|
exbidv |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ) ) |
| 30 |
29
|
rexbidva |
⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ) ) |
| 31 |
30
|
adantr |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ) ) |
| 32 |
|
simpr |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℤ ) |
| 33 |
15
|
adantr |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) = ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ) |
| 34 |
33
|
fveq1d |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ‘ 𝑥 ) ) |
| 35 |
34 21 24
|
3eqtr4g |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ‘ 𝑥 ) ) |
| 36 |
35
|
adantlr |
⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ‘ 𝑥 ) ) |
| 37 |
32 36
|
seqfeq |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) = seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ) |
| 38 |
37
|
breq1d |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → ( seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ↔ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ) |
| 39 |
31 38
|
3anbi23d |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ↔ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ) ) |
| 40 |
39
|
rexbidva |
⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ↔ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ) ) |
| 41 |
|
simplr |
⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → 𝑚 ∈ ℕ ) |
| 42 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
| 43 |
41 42
|
eleqtrdi |
⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → 𝑚 ∈ ( ℤ≥ ‘ 1 ) ) |
| 44 |
|
f1of |
⊢ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 → 𝑓 : ( 1 ... 𝑚 ) ⟶ 𝐴 ) |
| 45 |
44
|
ad2antlr |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → 𝑓 : ( 1 ... 𝑚 ) ⟶ 𝐴 ) |
| 46 |
|
ffvelcdm |
⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) ⟶ 𝐴 ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐴 ) |
| 47 |
45 46
|
sylancom |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐴 ) |
| 48 |
|
simplll |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ) |
| 49 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) |
| 50 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) |
| 51 |
49 50
|
nfeq |
⊢ Ⅎ 𝑘 ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) |
| 52 |
|
csbeq1a |
⊢ ( 𝑘 = ( 𝑓 ‘ 𝑥 ) → ( I ‘ 𝐵 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) ) |
| 53 |
|
csbeq1a |
⊢ ( 𝑘 = ( 𝑓 ‘ 𝑥 ) → ( I ‘ 𝐶 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) ) |
| 54 |
52 53
|
eqeq12d |
⊢ ( 𝑘 = ( 𝑓 ‘ 𝑥 ) → ( ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ↔ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) ) ) |
| 55 |
51 54
|
rspc |
⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) ) ) |
| 56 |
47 48 55
|
sylc |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) ) |
| 57 |
|
fvex |
⊢ ( 𝑓 ‘ 𝑥 ) ∈ V |
| 58 |
|
csbfv2g |
⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ V → ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ) ) |
| 59 |
57 58
|
ax-mp |
⊢ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ) |
| 60 |
|
csbfv2g |
⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ V → ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 ) ) |
| 61 |
57 60
|
ax-mp |
⊢ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 ) |
| 62 |
56 59 61
|
3eqtr3g |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 ) ) |
| 63 |
|
elfznn |
⊢ ( 𝑥 ∈ ( 1 ... 𝑚 ) → 𝑥 ∈ ℕ ) |
| 64 |
63
|
adantl |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → 𝑥 ∈ ℕ ) |
| 65 |
|
fveq2 |
⊢ ( 𝑛 = 𝑥 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑥 ) ) |
| 66 |
65
|
csbeq1d |
⊢ ( 𝑛 = 𝑥 → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ) |
| 67 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) |
| 68 |
66 67
|
fvmpti |
⊢ ( 𝑥 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ‘ 𝑥 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ) ) |
| 69 |
64 68
|
syl |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ‘ 𝑥 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ) ) |
| 70 |
65
|
csbeq1d |
⊢ ( 𝑛 = 𝑥 → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 ) |
| 71 |
|
eqid |
⊢ ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) |
| 72 |
70 71
|
fvmpti |
⊢ ( 𝑥 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ‘ 𝑥 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 ) ) |
| 73 |
64 72
|
syl |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ‘ 𝑥 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 ) ) |
| 74 |
62 69 73
|
3eqtr4d |
⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ‘ 𝑥 ) = ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ‘ 𝑥 ) ) |
| 75 |
43 74
|
seqfveq |
⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) |
| 76 |
75
|
eqeq2d |
⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → ( 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ↔ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) |
| 77 |
76
|
pm5.32da |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) |
| 78 |
77
|
exbidv |
⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) |
| 79 |
78
|
rexbidva |
⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) |
| 80 |
40 79
|
orbi12d |
⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 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 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) ) |
| 81 |
80
|
iotabidv |
⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 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 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) ) |
| 82 |
|
df-prod |
⊢ ∏ 𝑘 ∈ 𝐴 𝐵 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ) |
| 83 |
|
df-prod |
⊢ ∏ 𝑘 ∈ 𝐴 𝐶 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) |
| 84 |
81 82 83
|
3eqtr4g |
⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑘 ∈ 𝐴 𝐶 ) |