msrval

Description: Value of the reduct of a pre-statement. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	msrfval.v	⊢ 𝑉 = ( mVars ‘ 𝑇 )
	msrfval.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
	msrfval.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
	msrval.z	⊢ 𝑍 = ∪ ( 𝑉 “ ( 𝐻 ∪ { 𝐴 } ) )
Assertion	msrval	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → ( 𝑅 ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) = ⟨ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		msrfval.v	⊢ 𝑉 = ( mVars ‘ 𝑇 )
2		msrfval.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
3		msrfval.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
4		msrval.z	⊢ 𝑍 = ∪ ( 𝑉 “ ( 𝐻 ∪ { 𝐴 } ) )
5	1 2 3	msrfval	⊢ 𝑅 = ( 𝑠 ∈ 𝑃 ↦ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ )
6	5	a1i	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → 𝑅 = ( 𝑠 ∈ 𝑃 ↦ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ ) )
7		fvexd	⊢ ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) → ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∈ V )
8		fvexd	⊢ ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) → ( 2^nd ‘ 𝑠 ) ∈ V )
9		simpllr	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ )
10	9	fveq2d	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ( 1^st ‘ 𝑠 ) = ( 1^st ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) )
11	10	fveq2d	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) = ( 1^st ‘ ( 1^st ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ) )
12		eqid	⊢ ( mDV ‘ 𝑇 ) = ( mDV ‘ 𝑇 )
13		eqid	⊢ ( mEx ‘ 𝑇 ) = ( mEx ‘ 𝑇 )
14	12 13 2	elmpst	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ↔ ( ( 𝐷 ⊆ ( mDV ‘ 𝑇 ) ∧ ^◡ 𝐷 = 𝐷 ) ∧ ( 𝐻 ⊆ ( mEx ‘ 𝑇 ) ∧ 𝐻 ∈ Fin ) ∧ 𝐴 ∈ ( mEx ‘ 𝑇 ) ) )
15	14	simp1bi	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → ( 𝐷 ⊆ ( mDV ‘ 𝑇 ) ∧ ^◡ 𝐷 = 𝐷 ) )
16	15	simpld	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → 𝐷 ⊆ ( mDV ‘ 𝑇 ) )
17	16	ad3antrrr	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → 𝐷 ⊆ ( mDV ‘ 𝑇 ) )
18		fvex	⊢ ( mDV ‘ 𝑇 ) ∈ V
19	18	ssex	⊢ ( 𝐷 ⊆ ( mDV ‘ 𝑇 ) → 𝐷 ∈ V )
20	17 19	syl	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → 𝐷 ∈ V )
21	14	simp2bi	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → ( 𝐻 ⊆ ( mEx ‘ 𝑇 ) ∧ 𝐻 ∈ Fin ) )
22	21	simprd	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → 𝐻 ∈ Fin )
23	22	ad3antrrr	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → 𝐻 ∈ Fin )
24	14	simp3bi	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → 𝐴 ∈ ( mEx ‘ 𝑇 ) )
25	24	ad3antrrr	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → 𝐴 ∈ ( mEx ‘ 𝑇 ) )
26		ot1stg	⊢ ( ( 𝐷 ∈ V ∧ 𝐻 ∈ Fin ∧ 𝐴 ∈ ( mEx ‘ 𝑇 ) ) → ( 1^st ‘ ( 1^st ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ) = 𝐷 )
27	20 23 25 26	syl3anc	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ( 1^st ‘ ( 1^st ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ) = 𝐷 )
28	11 27	eqtrd	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) = 𝐷 )
29	1	fvexi	⊢ 𝑉 ∈ V
30		imaexg	⊢ ( 𝑉 ∈ V → ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) ∈ V )
31	29 30	ax-mp	⊢ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) ∈ V
32	31	uniex	⊢ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) ∈ V
33	32	a1i	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) ∈ V )
34		id	⊢ ( 𝑧 = ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) → 𝑧 = ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) )
35		simplr	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) )
36	10	fveq2d	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ) )
37		ot2ndg	⊢ ( ( 𝐷 ∈ V ∧ 𝐻 ∈ Fin ∧ 𝐴 ∈ ( mEx ‘ 𝑇 ) ) → ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ) = 𝐻 )
38	20 23 25 37	syl3anc	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ( 2^nd ‘ ( 1^st ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ) = 𝐻 )
39	35 36 38	3eqtrd	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ℎ = 𝐻 )
40		simpr	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → 𝑎 = ( 2^nd ‘ 𝑠 ) )
41	9	fveq2d	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ( 2^nd ‘ 𝑠 ) = ( 2^nd ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) )
42		ot3rdg	⊢ ( 𝐴 ∈ ( mEx ‘ 𝑇 ) → ( 2^nd ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) = 𝐴 )
43	25 42	syl	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ( 2^nd ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) = 𝐴 )
44	40 41 43	3eqtrd	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → 𝑎 = 𝐴 )
45	44	sneqd	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → { 𝑎 } = { 𝐴 } )
46	39 45	uneq12d	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ( ℎ ∪ { 𝑎 } ) = ( 𝐻 ∪ { 𝐴 } ) )
47	46	imaeq2d	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) = ( 𝑉 “ ( 𝐻 ∪ { 𝐴 } ) ) )
48	47	unieqd	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) = ∪ ( 𝑉 “ ( 𝐻 ∪ { 𝐴 } ) ) )
49	48 4	eqtr4di	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) = 𝑍 )
50	34 49	sylan9eqr	⊢ ( ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) ∧ 𝑧 = ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) ) → 𝑧 = 𝑍 )
51	50	sqxpeqd	⊢ ( ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) ∧ 𝑧 = ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) ) → ( 𝑧 × 𝑧 ) = ( 𝑍 × 𝑍 ) )
52	33 51	csbied	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) = ( 𝑍 × 𝑍 ) )
53	28 52	ineq12d	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) = ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) )
54	53 39 44	oteq123d	⊢ ( ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ 𝑎 = ( 2^nd ‘ 𝑠 ) ) → ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ = ⟨ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
55	8 54	csbied	⊢ ( ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) ∧ ℎ = ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ) → ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ = ⟨ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
56	7 55	csbied	⊢ ( ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 ∧ 𝑠 = ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) → ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( 𝑉 “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ = ⟨ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
57		id	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 )
58		otex	⊢ ⟨ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ ∈ V
59	58	a1i	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → ⟨ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ ∈ V )
60	6 56 57 59	fvmptd	⊢ ( ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ∈ 𝑃 → ( 𝑅 ‘ ⟨ 𝐷 , 𝐻 , 𝐴 ⟩ ) = ⟨ ( 𝐷 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )

Metamath Proof Explorer

Theorem msrval

Proof