elmsta

Description: Property of being a statement. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mstapst.p	$⊢ P = mPreSt (T)$
	mstapst.s	$⊢ S = mStat (T)$
	elmsta.v	$⊢ V = mVars (T)$
	elmsta.z	$⊢ Z = ⋃ V [H \cup \{A\}]$
Assertion	elmsta	$⊢ ⟨D, H, A⟩ \in S \leftrightarrow (⟨D, H, A⟩ \in P \land D \subseteq Z \times Z)$

Proof

Step	Hyp	Ref	Expression
1		mstapst.p	$⊢ P = mPreSt (T)$
2		mstapst.s	$⊢ S = mStat (T)$
3		elmsta.v	$⊢ V = mVars (T)$
4		elmsta.z	$⊢ Z = ⋃ V [H \cup \{A\}]$
5	1 2	mstapst	$⊢ S \subseteq P$
6	5	sseli	$⊢ ⟨D, H, A⟩ \in S \to ⟨D, H, A⟩ \in P$
7		eqid	$⊢ mStRed (T) = mStRed (T)$
8	3 1 7 4	msrval	$⊢ ⟨D, H, A⟩ \in P \to mStRed (T) (⟨D, H, A⟩) = ⟨D \cap (Z \times Z), H, A⟩$
9	6 8	syl	$⊢ ⟨D, H, A⟩ \in S \to mStRed (T) (⟨D, H, A⟩) = ⟨D \cap (Z \times Z), H, A⟩$
10	7 2	msrid	$⊢ ⟨D, H, A⟩ \in S \to mStRed (T) (⟨D, H, A⟩) = ⟨D, H, A⟩$
11	9 10	eqtr3d	$⊢ ⟨D, H, A⟩ \in S \to ⟨D \cap (Z \times Z), H, A⟩ = ⟨D, H, A⟩$
12	11	fveq2d	$⊢ ⟨D, H, A⟩ \in S \to 1^{st} (⟨D \cap (Z \times Z), H, A⟩) = 1^{st} (⟨D, H, A⟩)$
13	12	fveq2d	$⊢ ⟨D, H, A⟩ \in S \to 1^{st} (1^{st} (⟨D \cap (Z \times Z), H, A⟩)) = 1^{st} (1^{st} (⟨D, H, A⟩))$
14		inss1	$⊢ D \cap (Z \times Z) \subseteq D$
15	1	mpstrcl	$⊢ ⟨D, H, A⟩ \in P \to (D \in V \land H \in V \land A \in V)$
16	6 15	syl	$⊢ ⟨D, H, A⟩ \in S \to (D \in V \land H \in V \land A \in V)$
17	16	simp1d	$⊢ ⟨D, H, A⟩ \in S \to D \in V$
18		ssexg	$⊢ (D \cap (Z \times Z) \subseteq D \land D \in V) \to D \cap (Z \times Z) \in V$
19	14 17 18	sylancr	$⊢ ⟨D, H, A⟩ \in S \to D \cap (Z \times Z) \in V$
20	16	simp2d	$⊢ ⟨D, H, A⟩ \in S \to H \in V$
21	16	simp3d	$⊢ ⟨D, H, A⟩ \in S \to A \in V$
22		ot1stg	$⊢ (D \cap (Z \times Z) \in V \land H \in V \land A \in V) \to 1^{st} (1^{st} (⟨D \cap (Z \times Z), H, A⟩)) = D \cap (Z \times Z)$
23	19 20 21 22	syl3anc	$⊢ ⟨D, H, A⟩ \in S \to 1^{st} (1^{st} (⟨D \cap (Z \times Z), H, A⟩)) = D \cap (Z \times Z)$
24		ot1stg	$⊢ (D \in V \land H \in V \land A \in V) \to 1^{st} (1^{st} (⟨D, H, A⟩)) = D$
25	16 24	syl	$⊢ ⟨D, H, A⟩ \in S \to 1^{st} (1^{st} (⟨D, H, A⟩)) = D$
26	13 23 25	3eqtr3d	$⊢ ⟨D, H, A⟩ \in S \to D \cap (Z \times Z) = D$
27		inss2	$⊢ D \cap (Z \times Z) \subseteq Z \times Z$
28	26 27	eqsstrrdi	$⊢ ⟨D, H, A⟩ \in S \to D \subseteq Z \times Z$
29	6 28	jca	$⊢ ⟨D, H, A⟩ \in S \to (⟨D, H, A⟩ \in P \land D \subseteq Z \times Z)$
30	8	adantr	$⊢ (⟨D, H, A⟩ \in P \land D \subseteq Z \times Z) \to mStRed (T) (⟨D, H, A⟩) = ⟨D \cap (Z \times Z), H, A⟩$
31		simpr	$⊢ (⟨D, H, A⟩ \in P \land D \subseteq Z \times Z) \to D \subseteq Z \times Z$
32		dfss2	$⊢ D \subseteq Z \times Z \leftrightarrow D \cap (Z \times Z) = D$
33	31 32	sylib	$⊢ (⟨D, H, A⟩ \in P \land D \subseteq Z \times Z) \to D \cap (Z \times Z) = D$
34	33	oteq1d	$⊢ (⟨D, H, A⟩ \in P \land D \subseteq Z \times Z) \to ⟨D \cap (Z \times Z), H, A⟩ = ⟨D, H, A⟩$
35	30 34	eqtrd	$⊢ (⟨D, H, A⟩ \in P \land D \subseteq Z \times Z) \to mStRed (T) (⟨D, H, A⟩) = ⟨D, H, A⟩$
36	1 7	msrf	$⊢ mStRed (T) : P ⟶ P$
37		ffn	$⊢ mStRed (T) : P ⟶ P \to mStRed (T) Fn P$
38	36 37	ax-mp	$⊢ mStRed (T) Fn P$
39		simpl	$⊢ (⟨D, H, A⟩ \in P \land D \subseteq Z \times Z) \to ⟨D, H, A⟩ \in P$
40		fnfvelrn	$⊢ (mStRed (T) Fn P \land ⟨D, H, A⟩ \in P) \to mStRed (T) (⟨D, H, A⟩) \in ran mStRed (T)$
41	38 39 40	sylancr	$⊢ (⟨D, H, A⟩ \in P \land D \subseteq Z \times Z) \to mStRed (T) (⟨D, H, A⟩) \in ran mStRed (T)$
42	35 41	eqeltrrd	$⊢ (⟨D, H, A⟩ \in P \land D \subseteq Z \times Z) \to ⟨D, H, A⟩ \in ran mStRed (T)$
43	7 2	mstaval	$⊢ S = ran mStRed (T)$
44	42 43	eleqtrrdi	$⊢ (⟨D, H, A⟩ \in P \land D \subseteq Z \times Z) \to ⟨D, H, A⟩ \in S$
45	29 44	impbii	$⊢ ⟨D, H, A⟩ \in S \leftrightarrow (⟨D, H, A⟩ \in P \land D \subseteq Z \times Z)$

Metamath Proof Explorer

Theorem elmsta

Proof