# Metamath Proof Explorer

## Theorem mapdhval

Description: Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses mapdh.q ${⊢}{Q}={0}_{{C}}$
mapdh.i
mapdh.x ${⊢}{\phi }\to {X}\in {A}$
mapdh.f ${⊢}{\phi }\to {F}\in {B}$
mapdh.y ${⊢}{\phi }\to {Y}\in {E}$
Assertion mapdhval

### Proof

Step Hyp Ref Expression
1 mapdh.q ${⊢}{Q}={0}_{{C}}$
2 mapdh.i
3 mapdh.x ${⊢}{\phi }\to {X}\in {A}$
4 mapdh.f ${⊢}{\phi }\to {F}\in {B}$
5 mapdh.y ${⊢}{\phi }\to {Y}\in {E}$
6 otex ${⊢}⟨{X},{F},{Y}⟩\in \mathrm{V}$
7 fveq2 ${⊢}{x}=⟨{X},{F},{Y}⟩\to {2}^{nd}\left({x}\right)={2}^{nd}\left(⟨{X},{F},{Y}⟩\right)$
8 7 eqeq1d
9 7 sneqd ${⊢}{x}=⟨{X},{F},{Y}⟩\to \left\{{2}^{nd}\left({x}\right)\right\}=\left\{{2}^{nd}\left(⟨{X},{F},{Y}⟩\right)\right\}$
10 9 fveq2d ${⊢}{x}=⟨{X},{F},{Y}⟩\to {N}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)={N}\left(\left\{{2}^{nd}\left(⟨{X},{F},{Y}⟩\right)\right\}\right)$
11 10 fveqeq2d ${⊢}{x}=⟨{X},{F},{Y}⟩\to \left({M}\left({N}\left(\left\{{2}^{nd}\left({x}\right)\right\}\right)\right)={J}\left(\left\{{h}\right\}\right)↔{M}\left({N}\left(\left\{{2}^{nd}\left(⟨{X},{F},{Y}⟩\right)\right\}\right)\right)={J}\left(\left\{{h}\right\}\right)\right)$
12 fveq2 ${⊢}{x}=⟨{X},{F},{Y}⟩\to {1}^{st}\left({x}\right)={1}^{st}\left(⟨{X},{F},{Y}⟩\right)$
13 12 fveq2d ${⊢}{x}=⟨{X},{F},{Y}⟩\to {1}^{st}\left({1}^{st}\left({x}\right)\right)={1}^{st}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right)$
14 13 7 oveq12d
15 14 sneqd
16 15 fveq2d
17 16 fveq2d
18 12 fveq2d ${⊢}{x}=⟨{X},{F},{Y}⟩\to {2}^{nd}\left({1}^{st}\left({x}\right)\right)={2}^{nd}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right)$
19 18 oveq1d ${⊢}{x}=⟨{X},{F},{Y}⟩\to {2}^{nd}\left({1}^{st}\left({x}\right)\right){R}{h}={2}^{nd}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right){R}{h}$
20 19 sneqd ${⊢}{x}=⟨{X},{F},{Y}⟩\to \left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){R}{h}\right\}=\left\{{2}^{nd}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right){R}{h}\right\}$
21 20 fveq2d ${⊢}{x}=⟨{X},{F},{Y}⟩\to {J}\left(\left\{{2}^{nd}\left({1}^{st}\left({x}\right)\right){R}{h}\right\}\right)={J}\left(\left\{{2}^{nd}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right){R}{h}\right\}\right)$
22 17 21 eqeq12d
23 11 22 anbi12d
24 23 riotabidv
25 8 24 ifbieq2d
26 1 fvexi ${⊢}{Q}\in \mathrm{V}$
27 riotaex
28 26 27 ifex
29 25 2 28 fvmpt
30 6 29 mp1i
31 ot3rdg ${⊢}{Y}\in {E}\to {2}^{nd}\left(⟨{X},{F},{Y}⟩\right)={Y}$
32 5 31 syl ${⊢}{\phi }\to {2}^{nd}\left(⟨{X},{F},{Y}⟩\right)={Y}$
33 32 eqeq1d
34 32 sneqd ${⊢}{\phi }\to \left\{{2}^{nd}\left(⟨{X},{F},{Y}⟩\right)\right\}=\left\{{Y}\right\}$
35 34 fveq2d ${⊢}{\phi }\to {N}\left(\left\{{2}^{nd}\left(⟨{X},{F},{Y}⟩\right)\right\}\right)={N}\left(\left\{{Y}\right\}\right)$
36 35 fveqeq2d ${⊢}{\phi }\to \left({M}\left({N}\left(\left\{{2}^{nd}\left(⟨{X},{F},{Y}⟩\right)\right\}\right)\right)={J}\left(\left\{{h}\right\}\right)↔{M}\left({N}\left(\left\{{Y}\right\}\right)\right)={J}\left(\left\{{h}\right\}\right)\right)$
37 ot1stg ${⊢}\left({X}\in {A}\wedge {F}\in {B}\wedge {Y}\in {E}\right)\to {1}^{st}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right)={X}$
38 3 4 5 37 syl3anc ${⊢}{\phi }\to {1}^{st}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right)={X}$
39 38 32 oveq12d
40 39 sneqd
41 40 fveq2d
42 41 fveq2d
43 ot2ndg ${⊢}\left({X}\in {A}\wedge {F}\in {B}\wedge {Y}\in {E}\right)\to {2}^{nd}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right)={F}$
44 3 4 5 43 syl3anc ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right)={F}$
45 44 oveq1d ${⊢}{\phi }\to {2}^{nd}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right){R}{h}={F}{R}{h}$
46 45 sneqd ${⊢}{\phi }\to \left\{{2}^{nd}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right){R}{h}\right\}=\left\{{F}{R}{h}\right\}$
47 46 fveq2d ${⊢}{\phi }\to {J}\left(\left\{{2}^{nd}\left({1}^{st}\left(⟨{X},{F},{Y}⟩\right)\right){R}{h}\right\}\right)={J}\left(\left\{{F}{R}{h}\right\}\right)$
48 42 47 eqeq12d
49 36 48 anbi12d
50 49 riotabidv
51 33 50 ifbieq2d
52 30 51 eqtrd