elmsta

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

	Ref	Expression
Hypotheses	mstapst.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
	mstapst.s	⊢ 𝑆 = ( mStat ‘ 𝑇 )
	elmsta.v	⊢ 𝑉 = ( mVars ‘ 𝑇 )
	elmsta.z	⊢ 𝑍 = ∪ ( 𝑉 “ ( 𝐻 ∪ { 𝐴 } ) )
Assertion	elmsta	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 ↔ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐷 ⊆ ( 𝑍 × 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mstapst.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
2		mstapst.s	⊢ 𝑆 = ( mStat ‘ 𝑇 )
3		elmsta.v	⊢ 𝑉 = ( mVars ‘ 𝑇 )
4		elmsta.z	⊢ 𝑍 = ∪ ( 𝑉 “ ( 𝐻 ∪ { 𝐴 } ) )
5	1 2	mstapst	⊢ 𝑆 ⊆ 𝑃
6	5	sseli	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 → ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 )
7		eqid	⊢ ( mStRed ‘ 𝑇 ) = ( mStRed ‘ 𝑇 )
8	3 1 7 4	msrval	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → ( ( mStRed ‘ 𝑇 ) ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) = ⟨ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
9	6 8	syl	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 → ( ( mStRed ‘ 𝑇 ) ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) = ⟨ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
10	7 2	msrid	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 → ( ( mStRed ‘ 𝑇 ) ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ )
11	9 10	eqtr3d	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 → ⟨ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ )
12	11	fveq2d	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 → ( 1^st ‘ ⟨ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ ) = ( 1^st ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) )
13	12	fveq2d	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 → ( 1^st ‘ ( 1^st ‘ ⟨ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ ) ) = ( 1^st ‘ ( 1^st ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ) )
14		inss1	⊢ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) ⊆ 𝐷
15	1	mpstrcl	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → ( 𝐷 ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V ) )
16	6 15	syl	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 → ( 𝐷 ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V ) )
17	16	simp1d	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 → 𝐷 ∈ V )
18		ssexg	⊢ ( ( ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) ⊆ 𝐷 ∧ 𝐷 ∈ V ) → ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) ∈ V )
19	14 17 18	sylancr	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 → ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) ∈ V )
20	16	simp2d	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 → 𝐻 ∈ V )
21	16	simp3d	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 → 𝐴 ∈ V )
22		ot1stg	⊢ ( ( ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V ) → ( 1^st ‘ ( 1^st ‘ ⟨ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ ) ) = ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) )
23	19 20 21 22	syl3anc	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 → ( 1^st ‘ ( 1^st ‘ ⟨ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ ) ) = ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) )
24		ot1stg	⊢ ( ( 𝐷 ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V ) → ( 1^st ‘ ( 1^st ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ) = 𝐷 )
25	16 24	syl	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 → ( 1^st ‘ ( 1^st ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ) = 𝐷 )
26	13 23 25	3eqtr3d	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 → ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) = 𝐷 )
27		inss2	⊢ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) ⊆ ( 𝑍 × 𝑍 )
28	26 27	eqsstrrdi	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 → 𝐷 ⊆ ( 𝑍 × 𝑍 ) )
29	6 28	jca	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 → ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐷 ⊆ ( 𝑍 × 𝑍 ) ) )
30	8	adantr	⊢ ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐷 ⊆ ( 𝑍 × 𝑍 ) ) → ( ( mStRed ‘ 𝑇 ) ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) = ⟨ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
31		simpr	⊢ ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐷 ⊆ ( 𝑍 × 𝑍 ) ) → 𝐷 ⊆ ( 𝑍 × 𝑍 ) )
32		dfss2	⊢ ( 𝐷 ⊆ ( 𝑍 × 𝑍 ) ↔ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) = 𝐷 )
33	31 32	sylib	⊢ ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐷 ⊆ ( 𝑍 × 𝑍 ) ) → ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) = 𝐷 )
34	33	oteq1d	⊢ ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐷 ⊆ ( 𝑍 × 𝑍 ) ) → ⟨ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ )
35	30 34	eqtrd	⊢ ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐷 ⊆ ( 𝑍 × 𝑍 ) ) → ( ( mStRed ‘ 𝑇 ) ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ )
36	1 7	msrf	⊢ ( mStRed ‘ 𝑇 ) : 𝑃 ⟶ 𝑃
37		ffn	⊢ ( ( mStRed ‘ 𝑇 ) : 𝑃 ⟶ 𝑃 → ( mStRed ‘ 𝑇 ) Fn 𝑃 )
38	36 37	ax-mp	⊢ ( mStRed ‘ 𝑇 ) Fn 𝑃
39		simpl	⊢ ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐷 ⊆ ( 𝑍 × 𝑍 ) ) → ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 )
40		fnfvelrn	⊢ ( ( ( mStRed ‘ 𝑇 ) Fn 𝑃 ∧ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ) → ( ( mStRed ‘ 𝑇 ) ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∈ ran ( mStRed ‘ 𝑇 ) )
41	38 39 40	sylancr	⊢ ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐷 ⊆ ( 𝑍 × 𝑍 ) ) → ( ( mStRed ‘ 𝑇 ) ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∈ ran ( mStRed ‘ 𝑇 ) )
42	35 41	eqeltrrd	⊢ ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐷 ⊆ ( 𝑍 × 𝑍 ) ) → ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ ran ( mStRed ‘ 𝑇 ) )
43	7 2	mstaval	⊢ 𝑆 = ran ( mStRed ‘ 𝑇 )
44	42 43	eleqtrrdi	⊢ ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐷 ⊆ ( 𝑍 × 𝑍 ) ) → ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 )
45	29 44	impbii	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑆 ↔ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝐷 ⊆ ( 𝑍 × 𝑍 ) ) )

Metamath Proof Explorer

Theorem elmsta

Proof