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 6676 |
. . . . 5
⊢ (𝑥 = 𝑦 → (2^{nd} ‘𝑥) = (2^{nd} ‘𝑦)) |
3 | 2 | eqeq1d 2740 |
. . . 4
⊢ (𝑥 = 𝑦 → ((2^{nd} ‘𝑥) = 0 ↔ (2^{nd}
‘𝑦) = 0
)) |
4 | 2 | sneqd 4528 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → {(2^{nd} ‘𝑥)} = {(2^{nd}
‘𝑦)}) |
5 | 4 | fveq2d 6680 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑁‘{(2^{nd} ‘𝑥)}) = (𝑁‘{(2^{nd} ‘𝑦)})) |
6 | 5 | fveq2d 6680 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝑀‘(𝑁‘{(2^{nd} ‘𝑦)}))) |
7 | 6 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑀‘(𝑁‘{(2^{nd} ‘𝑥)})) = (𝐽‘{ℎ}) ↔ (𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{ℎ}))) |
8 | | 2fveq3 6681 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (1^{st}
‘(1^{st} ‘𝑥)) = (1^{st} ‘(1^{st}
‘𝑦))) |
9 | 8, 2 | oveq12d 7190 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥)) =
((1^{st} ‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))) |
10 | 9 | sneqd 4528 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → {((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))} =
{((1^{st} ‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))}) |
11 | 10 | fveq2d 6680 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))}) = (𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) |
12 | 11 | fveq2d 6680 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))}))) |
13 | | 2fveq3 6681 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (2^{nd}
‘(1^{st} ‘𝑥)) = (2^{nd} ‘(1^{st}
‘𝑦))) |
14 | 13 | oveq1d 7187 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ) = ((2^{nd} ‘(1^{st}
‘𝑦))𝑅ℎ)) |
15 | 14 | sneqd 4528 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → {((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)} = {((2^{nd} ‘(1^{st}
‘𝑦))𝑅ℎ)}) |
16 | 15 | fveq2d 6680 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)}) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)})) |
17 | 12, 16 | eqeq12d 2754 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑥)) − (2^{nd}
‘𝑥))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑥))𝑅ℎ)}) ↔ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)}))) |
18 | 7, 17 | anbi12d 634 |
. . . . 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} ‘𝑦))𝑅ℎ)})))) |
19 | 18 | riotabidv 7131 |
. . . 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} ‘𝑦))𝑅ℎ)})))) |
20 | 3, 19 | ifbieq2d 4440 |
. . 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} ‘𝑦))𝑅ℎ)}))))) |
21 | 20 | cbvmptv 5133 |
. 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} ‘𝑦))𝑅ℎ)}))))) |
22 | | sneq 4526 |
. . . . . . . 8
⊢ (ℎ = 𝑖 → {ℎ} = {𝑖}) |
23 | 22 | fveq2d 6680 |
. . . . . . 7
⊢ (ℎ = 𝑖 → (𝐽‘{ℎ}) = (𝐽‘{𝑖})) |
24 | 23 | eqeq2d 2749 |
. . . . . 6
⊢ (ℎ = 𝑖 → ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{ℎ}) ↔ (𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{𝑖}))) |
25 | | oveq2 7180 |
. . . . . . . . 9
⊢ (ℎ = 𝑖 → ((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ) = ((2^{nd} ‘(1^{st}
‘𝑦))𝑅𝑖)) |
26 | 25 | sneqd 4528 |
. . . . . . . 8
⊢ (ℎ = 𝑖 → {((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)} = {((2^{nd} ‘(1^{st}
‘𝑦))𝑅𝑖)}) |
27 | 26 | fveq2d 6680 |
. . . . . . 7
⊢ (ℎ = 𝑖 → (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)}) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅𝑖)})) |
28 | 27 | eqeq2d 2749 |
. . . . . 6
⊢ (ℎ = 𝑖 → ((𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅ℎ)}) ↔ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅𝑖)}))) |
29 | 24, 28 | anbi12d 634 |
. . . . 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} ‘𝑦))𝑅𝑖)})))) |
30 | 29 | cbvriotavw 7139 |
. . . 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} ‘𝑦))𝑅𝑖)}))) |
31 | | ifeq2 4419 |
. . . 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} ‘𝑦))𝑅𝑖)}))))) |
32 | 30, 31 | 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} ‘𝑦))𝑅𝑖)})))) |
33 | 32 | mpteq2i 5122 |
. 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} ‘𝑦))𝑅𝑖)}))))) |
34 | 1, 21, 33 | 3eqtri 2765 |
1
⊢ 𝐿 = (𝑦 ∈ V ↦ if((2^{nd}
‘𝑦) = 0 , 𝑄, (℩𝑖 ∈ 𝐷 ((𝑀‘(𝑁‘{(2^{nd} ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1^{st}
‘(1^{st} ‘𝑦)) − (2^{nd}
‘𝑦))})) = (𝐽‘{((2^{nd}
‘(1^{st} ‘𝑦))𝑅𝑖)}))))) |