Theorem 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	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
	mppsval.j	⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
	mppsval.c	⊢ 𝐶 = ( mCls ‘ 𝑇 )
Assertion	mppsval	⊢ 𝐽 = { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) }

Proof

Step	Hyp	Ref	Expression
1		mppsval.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
2		mppsval.j	⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
3		mppsval.c	⊢ 𝐶 = ( mCls ‘ 𝑇 )
4		fveq2	⊢ ( 𝑡 = 𝑇 → ( mPreSt ‘ 𝑡 ) = ( mPreSt ‘ 𝑇 ) )
5	4 1	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mPreSt ‘ 𝑡 ) = 𝑃 )
6	5	eleq2d	⊢ ( 𝑡 = 𝑇 → ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mPreSt ‘ 𝑡 ) ↔ ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ) )
7		fveq2	⊢ ( 𝑡 = 𝑇 → ( mCls ‘ 𝑡 ) = ( mCls ‘ 𝑇 ) )
8	7 3	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mCls ‘ 𝑡 ) = 𝐶 )
9	8	oveqd	⊢ ( 𝑡 = 𝑇 → ( 𝑑 ( mCls ‘ 𝑡 ) ℎ ) = ( 𝑑 𝐶 ℎ ) )
10	9	eleq2d	⊢ ( 𝑡 = 𝑇 → ( 𝑎 ∈ ( 𝑑 ( mCls ‘ 𝑡 ) ℎ ) ↔ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) )
11	6 10	anbi12d	⊢ ( 𝑡 = 𝑇 → ( ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mPreSt ‘ 𝑡 ) ∧ 𝑎 ∈ ( 𝑑 ( mCls ‘ 𝑡 ) ℎ ) ) ↔ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) ) )
12	11	oprabbidv	⊢ ( 𝑡 = 𝑇 → { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mPreSt ‘ 𝑡 ) ∧ 𝑎 ∈ ( 𝑑 ( mCls ‘ 𝑡 ) ℎ ) ) } = { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } )
13		df-mpps	⊢ mPPSt = ( 𝑡 ∈ V ↦ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mPreSt ‘ 𝑡 ) ∧ 𝑎 ∈ ( 𝑑 ( mCls ‘ 𝑡 ) ℎ ) ) } )
14	1	fvexi	⊢ 𝑃 ∈ V
15	1 2 3	mppspstlem	⊢ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } ⊆ 𝑃
16	14 15	ssexi	⊢ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } ∈ V
17	12 13 16	fvmpt	⊢ ( 𝑇 ∈ V → ( mPPSt ‘ 𝑇 ) = { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } )
18		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mPPSt ‘ 𝑇 ) = ∅ )
19		df-oprab	⊢ { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } = { 𝑥 ∣ ∃ 𝑑 ∃ ℎ ∃ 𝑎 ( 𝑥 = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∧ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) ) }
20		abn0	⊢ ( { 𝑥 ∣ ∃ 𝑑 ∃ ℎ ∃ 𝑎 ( 𝑥 = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∧ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) ) } ≠ ∅ ↔ ∃ 𝑥 ∃ 𝑑 ∃ ℎ ∃ 𝑎 ( 𝑥 = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∧ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) ) )
21		elfvex	⊢ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mPreSt ‘ 𝑇 ) → 𝑇 ∈ V )
22	21 1	eleq2s	⊢ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 → 𝑇 ∈ V )
23	22	ad2antrl	⊢ ( ( 𝑥 = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∧ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) ) → 𝑇 ∈ V )
24	23	exlimivv	⊢ ( ∃ ℎ ∃ 𝑎 ( 𝑥 = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∧ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) ) → 𝑇 ∈ V )
25	24	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑑 ∃ ℎ ∃ 𝑎 ( 𝑥 = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∧ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) ) → 𝑇 ∈ V )
26	20 25	sylbi	⊢ ( { 𝑥 ∣ ∃ 𝑑 ∃ ℎ ∃ 𝑎 ( 𝑥 = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∧ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) ) } ≠ ∅ → 𝑇 ∈ V )
27	26	necon1bi	⊢ ( ¬ 𝑇 ∈ V → { 𝑥 ∣ ∃ 𝑑 ∃ ℎ ∃ 𝑎 ( 𝑥 = ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∧ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) ) } = ∅ )
28	19 27	syl5eq	⊢ ( ¬ 𝑇 ∈ V → { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } = ∅ )
29	18 28	eqtr4d	⊢ ( ¬ 𝑇 ∈ V → ( mPPSt ‘ 𝑇 ) = { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) } )
30	17 29	pm2.61i	⊢ ( mPPSt ‘ 𝑇 ) = { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) }
31	2 30	eqtri	⊢ 𝐽 = { ⟨ ⟨ 𝑑 , ℎ ⟩ , 𝑎 ⟩ ∣ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ 𝑃 ∧ 𝑎 ∈ ( 𝑑 𝐶 ℎ ) ) }