Step | Hyp | Ref
| Expression |
1 | | hdmap1cbv.l |
. 2
⊢ 𝐿 = (𝑥 ∈ V ↦ if((2^{nd}
‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)}))))) |
2 | | fveq2 6087 |
. . . . 5
⊢ (𝑥 = 𝑦 → (2^{nd} ‘𝑥) = (2^{nd} ‘𝑦)) |
3 | 2 | eqeq1d 2611 |
. . . 4
⊢ (𝑥 = 𝑦 → ((2^{nd} ‘𝑥) = 0 ↔ (2^{nd}
‘𝑦) = 0
)) |
4 | 2 | sneqd 4136 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → {(2^{nd} ‘𝑥)} = {(2^{nd}
‘𝑦)}) |
5 | 4 | fveq2d 6091 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑁‘{(2^{nd} ‘𝑥)}) = (𝑁‘{(2^{nd} ‘𝑦)})) |
6 | 5 | fveq2d 6091 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝑀‘(𝑁‘{(2^{nd} ‘𝑦)}))) |
7 | 6 | eqeq1d 2611 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ↔ (𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{ℎ}))) |
8 | | fveq2 6087 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (1^{st} ‘𝑥) = (1^{st} ‘𝑦)) |
9 | 8 | fveq2d 6091 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (1^{st}
‘(1^{st} ‘𝑥)) = (1^{st} ‘(1^{st}
‘𝑦))) |
10 | 9, 2 | oveq12d 6544 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥)) =
((1^{st} ‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))) |
11 | 10 | sneqd 4136 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → {((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))} =
{((1^{st} ‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))}) |
12 | 11 | fveq2d 6091 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))}) = (𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) |
13 | 12 | fveq2d 6091 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))}))) |
14 | 8 | fveq2d 6091 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (2^{nd}
‘(1^{st} ‘𝑥)) = (2^{nd} ‘(1^{st}
‘𝑦))) |
15 | 14 | oveq1d 6541 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ) = ((2^{nd} ‘(1^{st}
‘𝑦))𝑅ℎ)) |
16 | 15 | sneqd 4136 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → {((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)} = {((2^{nd} ‘(1^{st}
‘𝑦))𝑅ℎ)}) |
17 | 16 | fveq2d 6091 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)}) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)})) |
18 | 13, 17 | eqeq12d 2624 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)}) ↔ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)}))) |
19 | 7, 18 | anbi12d 742 |
. . . . 5
⊢ (𝑥 = 𝑦 → (((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)})) ↔ ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)})))) |
20 | 19 | riotabidv 6490 |
. . . 4
⊢ (𝑥 = 𝑦 → (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)}))) = (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)})))) |
21 | 3, 20 | ifbieq2d 4060 |
. . 3
⊢ (𝑥 = 𝑦 → if((2^{nd} ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)})))) = if((2^{nd} ‘𝑦) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)}))))) |
22 | 21 | cbvmptv 4672 |
. 2
⊢ (𝑥 ∈ V ↦
if((2^{nd} ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)}))))) = (𝑦 ∈ V ↦ if((2^{nd}
‘𝑦) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)}))))) |
23 | | sneq 4134 |
. . . . . . . 8
⊢ (ℎ = 𝑖 → {ℎ} = {𝑖}) |
24 | 23 | fveq2d 6091 |
. . . . . . 7
⊢ (ℎ = 𝑖 → (𝐽‘{ℎ}) = (𝐽‘{𝑖})) |
25 | 24 | eqeq2d 2619 |
. . . . . 6
⊢ (ℎ = 𝑖 → ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{ℎ}) ↔ (𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{𝑖}))) |
26 | | oveq2 6534 |
. . . . . . . . 9
⊢ (ℎ = 𝑖 → ((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ) = ((2^{nd} ‘(1^{st}
‘𝑦))𝑅𝑖)) |
27 | 26 | sneqd 4136 |
. . . . . . . 8
⊢ (ℎ = 𝑖 → {((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)} = {((2^{nd} ‘(1^{st}
‘𝑦))𝑅𝑖)}) |
28 | 27 | fveq2d 6091 |
. . . . . . 7
⊢ (ℎ = 𝑖 → (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)}) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅𝑖)})) |
29 | 28 | eqeq2d 2619 |
. . . . . 6
⊢ (ℎ = 𝑖 → ((𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)}) ↔ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅𝑖)}))) |
30 | 25, 29 | anbi12d 742 |
. . . . 5
⊢ (ℎ = 𝑖 → (((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)})) ↔ ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅𝑖)})))) |
31 | 30 | cbvriotav 6499 |
. . . 4
⊢
(℩ℎ
∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)}))) = (℩𝑖 ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅𝑖)}))) |
32 | | ifeq2 4040 |
. . . 4
⊢
((℩ℎ
∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)}))) = (℩𝑖 ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅𝑖)}))) → if((2^{nd} ‘𝑦) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)})))) = if((2^{nd} ‘𝑦) = 0 , 𝑄, (℩𝑖 ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅𝑖)}))))) |
33 | 31, 32 | ax-mp 5 |
. . 3
⊢
if((2^{nd} ‘𝑦) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)})))) = if((2^{nd} ‘𝑦) = 0 , 𝑄, (℩𝑖 ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅𝑖)})))) |
34 | 33 | mpteq2i 4663 |
. 2
⊢ (𝑦 ∈ V ↦
if((2^{nd} ‘𝑦) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)}))))) = (𝑦 ∈ V ↦ if((2^{nd}
‘𝑦) = 0 , 𝑄, (℩𝑖 ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅𝑖)}))))) |
35 | 1, 22, 34 | 3eqtri 2635 |
1
⊢ 𝐿 = (𝑦 ∈ V ↦ if((2^{nd}
‘𝑦) = 0 , 𝑄, (℩𝑖 ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅𝑖)}))))) |