Theorem mpstrcl

Description: The elements of a pre-statement are sets. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypothesis	mpstssv.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
Assertion	mpstrcl	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → ( 𝐷 ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		mpstssv.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
2		df-ot	⊢ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ = ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩
3	1	mpstssv	⊢ 𝑃 ⊆ ( ( V × V ) × V )
4	3	sseli	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ ( ( V × V ) × V ) )
5	2 4	eqeltrrid	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ ( ( V × V ) × V ) )
6		opelxp	⊢ ( ⟨ 𝐷 , 𝐻 ⟩ ∈ ( V × V ) ↔ ( 𝐷 ∈ V ∧ 𝐻 ∈ V ) )
7	6	anbi1i	⊢ ( ( ⟨ 𝐷 , 𝐻 ⟩ ∈ ( V × V ) ∧ 𝐴 ∈ V ) ↔ ( ( 𝐷 ∈ V ∧ 𝐻 ∈ V ) ∧ 𝐴 ∈ V ) )
8		opelxp	⊢ ( ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ ( ( V × V ) × V ) ↔ ( ⟨ 𝐷 , 𝐻 ⟩ ∈ ( V × V ) ∧ 𝐴 ∈ V ) )
9		df-3an	⊢ ( ( 𝐷 ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V ) ↔ ( ( 𝐷 ∈ V ∧ 𝐻 ∈ V ) ∧ 𝐴 ∈ V ) )
10	7 8 9	3bitr4i	⊢ ( ⟨ ⟨ 𝐷 , 𝐻 ⟩ , 𝐴 ⟩ ∈ ( ( V × V ) × V ) ↔ ( 𝐷 ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V ) )
11	5 10	sylib	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → ( 𝐷 ∈ V ∧ 𝐻 ∈ V ∧ 𝐴 ∈ V ) )