mppsval

Description: Definition of a provable pre-statement, essentially just a reorganization of the arguments of df-mcls . (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mppsval.p	$⊢ P = mPreSt (T)$
	mppsval.j	$⊢ J = mPPSt (T)$
	mppsval.c	$⊢ C = mCls (T)$
Assertion	mppsval	$⊢ J = \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\}$

Proof

Step	Hyp	Ref	Expression
1		mppsval.p	$⊢ P = mPreSt (T)$
2		mppsval.j	$⊢ J = mPPSt (T)$
3		mppsval.c	$⊢ C = mCls (T)$
4		fveq2	$⊢ t = T \to mPreSt (t) = mPreSt (T)$
5	4 1	eqtr4di	$⊢ t = T \to mPreSt (t) = P$
6	5	eleq2d	$⊢ t = T \to (⟨d, h, a⟩ \in mPreSt (t) \leftrightarrow ⟨d, h, a⟩ \in P)$
7		fveq2	$⊢ t = T \to mCls (t) = mCls (T)$
8	7 3	eqtr4di	$⊢ t = T \to mCls (t) = C$
9	8	oveqd	$⊢ t = T \to d mCls (t) h = d C h$
10	9	eleq2d	$⊢ t = T \to (a \in (d mCls (t) h) \leftrightarrow a \in (d C h))$
11	6 10	anbi12d	$⊢ t = T \to ((⟨d, h, a⟩ \in mPreSt (t) \land a \in (d mCls (t) h)) \leftrightarrow (⟨d, h, a⟩ \in P \land a \in (d C h)))$
12	11	oprabbidv	$⊢ t = T \to \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in mPreSt (t) \land a \in (d mCls (t) h))\} = \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\}$
13		df-mpps	$⊢ mPPSt = (t \in V ⟼ \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in mPreSt (t) \land a \in (d mCls (t) h))\})$
14	1	fvexi	$⊢ P \in V$
15	1 2 3	mppspstlem	$⊢ \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\} \subseteq P$
16	14 15	ssexi	$⊢ \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\} \in V$
17	12 13 16	fvmpt	$⊢ T \in V \to mPPSt (T) = \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\}$
18		fvprc	$⊢ \neg T \in V \to mPPSt (T) = \emptyset$
19		df-oprab	$⊢ \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\} = \{x \| \exists d \exists h \exists a (x = ⟨⟨d, h⟩, a⟩ \land (⟨d, h, a⟩ \in P \land a \in (d C h)))\}$
20		abn0	$⊢ \{x \| \exists d \exists h \exists a (x = ⟨⟨d, h⟩, a⟩ \land (⟨d, h, a⟩ \in P \land a \in (d C h)))\} \neq \emptyset \leftrightarrow \exists x \exists d \exists h \exists a (x = ⟨⟨d, h⟩, a⟩ \land (⟨d, h, a⟩ \in P \land a \in (d C h)))$
21		elfvex	$⊢ ⟨d, h, a⟩ \in mPreSt (T) \to T \in V$
22	21 1	eleq2s	$⊢ ⟨d, h, a⟩ \in P \to T \in V$
23	22	ad2antrl	$⊢ (x = ⟨⟨d, h⟩, a⟩ \land (⟨d, h, a⟩ \in P \land a \in (d C h))) \to T \in V$
24	23	exlimivv	$⊢ \exists h \exists a (x = ⟨⟨d, h⟩, a⟩ \land (⟨d, h, a⟩ \in P \land a \in (d C h))) \to T \in V$
25	24	exlimivv	$⊢ \exists x \exists d \exists h \exists a (x = ⟨⟨d, h⟩, a⟩ \land (⟨d, h, a⟩ \in P \land a \in (d C h))) \to T \in V$
26	20 25	sylbi	$⊢ \{x \| \exists d \exists h \exists a (x = ⟨⟨d, h⟩, a⟩ \land (⟨d, h, a⟩ \in P \land a \in (d C h)))\} \neq \emptyset \to T \in V$
27	26	necon1bi	$⊢ \neg T \in V \to \{x \| \exists d \exists h \exists a (x = ⟨⟨d, h⟩, a⟩ \land (⟨d, h, a⟩ \in P \land a \in (d C h)))\} = \emptyset$
28	19 27	syl5eq	$⊢ \neg T \in V \to \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\} = \emptyset$
29	18 28	eqtr4d	$⊢ \neg T \in V \to mPPSt (T) = \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\}$
30	17 29	pm2.61i	$⊢ mPPSt (T) = \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\}$
31	2 30	eqtri	$⊢ J = \{⟨⟨d, h⟩, a⟩ \| (⟨d, h, a⟩ \in P \land a \in (d C h))\}$

Metamath Proof Explorer

Theorem mppsval

Proof