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	$⊢ I = (x \in V ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})))))$
	mapdh.x	$⊢ φ \to X \in A$
	mapdh.f	$⊢ φ \to F \in B$
	mapdh.y	$⊢ φ \to Y \in E$
Assertion	mapdhval	$⊢ φ \to I (⟨X, F, Y⟩) = if (Y = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{Y\})) = J (\{h\}) \land M (N (\{X \underset{˙}{-} Y\})) = J (\{F R h\}))))$

Proof

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

Metamath Proof Explorer

Theorem mapdhval

Proof