Proof of Theorem hdmap1cbv
Step | Hyp | Ref
| Expression |
1 | | hdmap1cbv.l |
. 2
⊢ 𝐿 = (𝑥 ∈ V ↦ if((2nd
‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))) |
2 | | fveq2 6774 |
. . . . 5
⊢ (𝑥 = 𝑦 → (2nd ‘𝑥) = (2nd ‘𝑦)) |
3 | 2 | eqeq1d 2740 |
. . . 4
⊢ (𝑥 = 𝑦 → ((2nd ‘𝑥) = 0 ↔ (2nd
‘𝑦) = 0
)) |
4 | 2 | sneqd 4573 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → {(2nd ‘𝑥)} = {(2nd
‘𝑦)}) |
5 | 4 | fveq2d 6778 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑁‘{(2nd ‘𝑥)}) = (𝑁‘{(2nd ‘𝑦)})) |
6 | 5 | fveq2d 6778 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝑀‘(𝑁‘{(2nd ‘𝑦)}))) |
7 | 6 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ↔ (𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{ℎ}))) |
8 | | 2fveq3 6779 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (1st
‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦))) |
9 | 8, 2 | oveq12d 7293 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥)) =
((1st ‘(1st ‘𝑦)) − (2nd
‘𝑦))) |
10 | 9 | sneqd 4573 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → {((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))} =
{((1st ‘(1st ‘𝑦)) − (2nd
‘𝑦))}) |
11 | 10 | fveq2d 6778 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))}) = (𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) |
12 | 11 | fveq2d 6778 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))}))) |
13 | | 2fveq3 6779 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (2nd
‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦))) |
14 | 13 | oveq1d 7290 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((2nd
‘(1st ‘𝑥))𝑅ℎ) = ((2nd ‘(1st
‘𝑦))𝑅ℎ)) |
15 | 14 | sneqd 4573 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → {((2nd
‘(1st ‘𝑥))𝑅ℎ)} = {((2nd ‘(1st
‘𝑦))𝑅ℎ)}) |
16 | 15 | fveq2d 6778 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅ℎ)})) |
17 | 12, 16 | eqeq12d 2754 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}) ↔ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅ℎ)}))) |
18 | 7, 17 | anbi12d 631 |
. . . . 5
⊢ (𝑥 = 𝑦 → (((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})) ↔ ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅ℎ)})))) |
19 | 18 | riotabidv 7234 |
. . . 4
⊢ (𝑥 = 𝑦 → (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))) = (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅ℎ)})))) |
20 | 3, 19 | ifbieq2d 4485 |
. . 3
⊢ (𝑥 = 𝑦 → if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)})))) = if((2nd ‘𝑦) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅ℎ)}))))) |
21 | 20 | cbvmptv 5187 |
. 2
⊢ (𝑥 ∈ V ↦
if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))) = (𝑦 ∈ V ↦ if((2nd
‘𝑦) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅ℎ)}))))) |
22 | | sneq 4571 |
. . . . . . . 8
⊢ (ℎ = 𝑖 → {ℎ} = {𝑖}) |
23 | 22 | fveq2d 6778 |
. . . . . . 7
⊢ (ℎ = 𝑖 → (𝐽‘{ℎ}) = (𝐽‘{𝑖})) |
24 | 23 | eqeq2d 2749 |
. . . . . 6
⊢ (ℎ = 𝑖 → ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{ℎ}) ↔ (𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{𝑖}))) |
25 | | oveq2 7283 |
. . . . . . . . 9
⊢ (ℎ = 𝑖 → ((2nd
‘(1st ‘𝑦))𝑅ℎ) = ((2nd ‘(1st
‘𝑦))𝑅𝑖)) |
26 | 25 | sneqd 4573 |
. . . . . . . 8
⊢ (ℎ = 𝑖 → {((2nd
‘(1st ‘𝑦))𝑅ℎ)} = {((2nd ‘(1st
‘𝑦))𝑅𝑖)}) |
27 | 26 | fveq2d 6778 |
. . . . . . 7
⊢ (ℎ = 𝑖 → (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅ℎ)}) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅𝑖)})) |
28 | 27 | eqeq2d 2749 |
. . . . . 6
⊢ (ℎ = 𝑖 → ((𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅ℎ)}) ↔ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅𝑖)}))) |
29 | 24, 28 | anbi12d 631 |
. . . . 5
⊢ (ℎ = 𝑖 → (((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅ℎ)})) ↔ ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅𝑖)})))) |
30 | 29 | cbvriotavw 7242 |
. . . 4
⊢
(℩ℎ
∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅ℎ)}))) = (℩𝑖 ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅𝑖)}))) |
31 | | ifeq2 4464 |
. . . 4
⊢
((℩ℎ
∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅ℎ)}))) = (℩𝑖 ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅𝑖)}))) → if((2nd ‘𝑦) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅ℎ)})))) = if((2nd ‘𝑦) = 0 , 𝑄, (℩𝑖 ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅𝑖)}))))) |
32 | 30, 31 | ax-mp 5 |
. . 3
⊢
if((2nd ‘𝑦) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅ℎ)})))) = if((2nd ‘𝑦) = 0 , 𝑄, (℩𝑖 ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅𝑖)})))) |
33 | 32 | mpteq2i 5179 |
. 2
⊢ (𝑦 ∈ V ↦
if((2nd ‘𝑦) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅ℎ)}))))) = (𝑦 ∈ V ↦ if((2nd
‘𝑦) = 0 , 𝑄, (℩𝑖 ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅𝑖)}))))) |
34 | 1, 21, 33 | 3eqtri 2770 |
1
⊢ 𝐿 = (𝑦 ∈ V ↦ if((2nd
‘𝑦) = 0 , 𝑄, (℩𝑖 ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑦)})) = (𝐽‘{𝑖}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑦)) − (2nd
‘𝑦))})) = (𝐽‘{((2nd
‘(1st ‘𝑦))𝑅𝑖)}))))) |