msrval

Description: Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	msrfval.v	$⊢ V = mVars (T)$
	msrfval.p	$⊢ P = mPreSt (T)$
	msrfval.r	$⊢ R = mStRed (T)$
	msrval.z	$⊢ Z = ⋃ V [H \cup \{A\}]$
Assertion	msrval	$⊢ ⟨D, H, A⟩ \in P \to R (⟨D, H, A⟩) = ⟨D \cap (Z \times Z), H, A⟩$

Proof

Step	Hyp	Ref	Expression
1		msrfval.v	$⊢ V = mVars (T)$
2		msrfval.p	$⊢ P = mPreSt (T)$
3		msrfval.r	$⊢ R = mStRed (T)$
4		msrval.z	$⊢ Z = ⋃ V [H \cup \{A\}]$
5	1 2 3	msrfval	$⊢ R = (s \in P ⟼ ⦋ 2^{nd} (1^{st} (s)) / h ⦌ ⦋ 2^{nd} (s) / a ⦌ ⟨1^{st} (1^{st} (s)) \cap ⦋ ⋃ V [h \cup \{a\}] / z ⦌ (z \times z), h, a⟩)$
6	5	a1i	$⊢ ⟨D, H, A⟩ \in P \to R = (s \in P ⟼ ⦋ 2^{nd} (1^{st} (s)) / h ⦌ ⦋ 2^{nd} (s) / a ⦌ ⟨1^{st} (1^{st} (s)) \cap ⦋ ⋃ V [h \cup \{a\}] / z ⦌ (z \times z), h, a⟩)$
7		fvexd	$⊢ (⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \to 2^{nd} (1^{st} (s)) \in V$
8		fvexd	$⊢ ((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \to 2^{nd} (s) \in V$
9		simpllr	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to s = ⟨D, H, A⟩$
10	9	fveq2d	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to 1^{st} (s) = 1^{st} (⟨D, H, A⟩)$
11	10	fveq2d	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to 1^{st} (1^{st} (s)) = 1^{st} (1^{st} (⟨D, H, A⟩))$
12		eqid	$⊢ mDV (T) = mDV (T)$
13		eqid	$⊢ mEx (T) = mEx (T)$
14	12 13 2	elmpst	$⊢ ⟨D, H, A⟩ \in P \leftrightarrow ((D \subseteq mDV (T) \land D^{-1} = D) \land (H \subseteq mEx (T) \land H \in Fin) \land A \in mEx (T))$
15	14	simp1bi	$⊢ ⟨D, H, A⟩ \in P \to (D \subseteq mDV (T) \land D^{-1} = D)$
16	15	simpld	$⊢ ⟨D, H, A⟩ \in P \to D \subseteq mDV (T)$
17	16	ad3antrrr	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to D \subseteq mDV (T)$
18		fvex	$⊢ mDV (T) \in V$
19	18	ssex	$⊢ D \subseteq mDV (T) \to D \in V$
20	17 19	syl	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to D \in V$
21	14	simp2bi	$⊢ ⟨D, H, A⟩ \in P \to (H \subseteq mEx (T) \land H \in Fin)$
22	21	simprd	$⊢ ⟨D, H, A⟩ \in P \to H \in Fin$
23	22	ad3antrrr	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to H \in Fin$
24	14	simp3bi	$⊢ ⟨D, H, A⟩ \in P \to A \in mEx (T)$
25	24	ad3antrrr	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to A \in mEx (T)$
26		ot1stg	$⊢ (D \in V \land H \in Fin \land A \in mEx (T)) \to 1^{st} (1^{st} (⟨D, H, A⟩)) = D$
27	20 23 25 26	syl3anc	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to 1^{st} (1^{st} (⟨D, H, A⟩)) = D$
28	11 27	eqtrd	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to 1^{st} (1^{st} (s)) = D$
29	1	fvexi	$⊢ V \in V$
30		imaexg	$⊢ V \in V \to V [h \cup \{a\}] \in V$
31	29 30	ax-mp	$⊢ V [h \cup \{a\}] \in V$
32	31	uniex	$⊢ ⋃ V [h \cup \{a\}] \in V$
33	32	a1i	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to ⋃ V [h \cup \{a\}] \in V$
34		id	$⊢ z = ⋃ V [h \cup \{a\}] \to z = ⋃ V [h \cup \{a\}]$
35		simplr	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to h = 2^{nd} (1^{st} (s))$
36	10	fveq2d	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to 2^{nd} (1^{st} (s)) = 2^{nd} (1^{st} (⟨D, H, A⟩))$
37		ot2ndg	$⊢ (D \in V \land H \in Fin \land A \in mEx (T)) \to 2^{nd} (1^{st} (⟨D, H, A⟩)) = H$
38	20 23 25 37	syl3anc	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to 2^{nd} (1^{st} (⟨D, H, A⟩)) = H$
39	35 36 38	3eqtrd	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to h = H$
40		simpr	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to a = 2^{nd} (s)$
41	9	fveq2d	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to 2^{nd} (s) = 2^{nd} (⟨D, H, A⟩)$
42		ot3rdg	$⊢ A \in mEx (T) \to 2^{nd} (⟨D, H, A⟩) = A$
43	25 42	syl	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to 2^{nd} (⟨D, H, A⟩) = A$
44	40 41 43	3eqtrd	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to a = A$
45	44	sneqd	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to \{a\} = \{A\}$
46	39 45	uneq12d	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to h \cup \{a\} = H \cup \{A\}$
47	46	imaeq2d	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to V [h \cup \{a\}] = V [H \cup \{A\}]$
48	47	unieqd	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to ⋃ V [h \cup \{a\}] = ⋃ V [H \cup \{A\}]$
49	48 4	eqtr4di	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to ⋃ V [h \cup \{a\}] = Z$
50	34 49	sylan9eqr	$⊢ ((((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \land z = ⋃ V [h \cup \{a\}]) \to z = Z$
51	50	sqxpeqd	$⊢ ((((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \land z = ⋃ V [h \cup \{a\}]) \to z \times z = Z \times Z$
52	33 51	csbied	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to ⦋ ⋃ V [h \cup \{a\}] / z ⦌ (z \times z) = Z \times Z$
53	28 52	ineq12d	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to 1^{st} (1^{st} (s)) \cap ⦋ ⋃ V [h \cup \{a\}] / z ⦌ (z \times z) = D \cap (Z \times Z)$
54	53 39 44	oteq123d	$⊢ (((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \land a = 2^{nd} (s)) \to ⟨1^{st} (1^{st} (s)) \cap ⦋ ⋃ V [h \cup \{a\}] / z ⦌ (z \times z), h, a⟩ = ⟨D \cap (Z \times Z), H, A⟩$
55	8 54	csbied	$⊢ ((⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \land h = 2^{nd} (1^{st} (s))) \to ⦋ 2^{nd} (s) / a ⦌ ⟨1^{st} (1^{st} (s)) \cap ⦋ ⋃ V [h \cup \{a\}] / z ⦌ (z \times z), h, a⟩ = ⟨D \cap (Z \times Z), H, A⟩$
56	7 55	csbied	$⊢ (⟨D, H, A⟩ \in P \land s = ⟨D, H, A⟩) \to ⦋ 2^{nd} (1^{st} (s)) / h ⦌ ⦋ 2^{nd} (s) / a ⦌ ⟨1^{st} (1^{st} (s)) \cap ⦋ ⋃ V [h \cup \{a\}] / z ⦌ (z \times z), h, a⟩ = ⟨D \cap (Z \times Z), H, A⟩$
57		id	$⊢ ⟨D, H, A⟩ \in P \to ⟨D, H, A⟩ \in P$
58		otex	$⊢ ⟨D \cap (Z \times Z), H, A⟩ \in V$
59	58	a1i	$⊢ ⟨D, H, A⟩ \in P \to ⟨D \cap (Z \times Z), H, A⟩ \in V$
60	6 56 57 59	fvmptd	$⊢ ⟨D, H, A⟩ \in P \to R (⟨D, H, A⟩) = ⟨D \cap (Z \times Z), H, A⟩$

Metamath Proof Explorer

Theorem msrval

Proof