mpstrcl

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

		Ref	Expression
	Hypothesis	mpstssv.p	$⊢ P = mPreSt (T)$
	Assertion	mpstrcl	$⊢ ⟨D, H, A⟩ \in P \to (D \in V \land H \in V \land A \in V)$

Step	Hyp	Ref	Expression
1		mpstssv.p	$⊢ P = mPreSt (T)$
2		df-ot	$⊢ ⟨D, H, A⟩ = ⟨⟨D, H⟩, A⟩$
3	1	mpstssv	$⊢ P \subseteq (V \times V) \times V$
4	3	sseli	$⊢ ⟨D, H, A⟩ \in P \to ⟨D, H, A⟩ \in ((V \times V) \times V)$
5	2 4	eqeltrrid	$⊢ ⟨D, H, A⟩ \in P \to ⟨⟨D, H⟩, A⟩ \in ((V \times V) \times V)$
6		opelxp	$⊢ ⟨D, H⟩ \in (V \times V) \leftrightarrow (D \in V \land H \in V)$
7	6	anbi1i	$⊢ (⟨D, H⟩ \in (V \times V) \land A \in V) \leftrightarrow ((D \in V \land H \in V) \land A \in V)$
8		opelxp	$⊢ ⟨⟨D, H⟩, A⟩ \in ((V \times V) \times V) \leftrightarrow (⟨D, H⟩ \in (V \times V) \land A \in V)$
9		df-3an	$⊢ (D \in V \land H \in V \land A \in V) \leftrightarrow ((D \in V \land H \in V) \land A \in V)$
10	7 8 9	3bitr4i	$⊢ ⟨⟨D, H⟩, A⟩ \in ((V \times V) \times V) \leftrightarrow (D \in V \land H \in V \land A \in V)$
11	5 10	sylib	$⊢ ⟨D, H, A⟩ \in P \to (D \in V \land H \in V \land A \in V)$

Metamath Proof Explorer