msrf

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

	Ref	Expression
Hypotheses	mpstssv.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
	msrf.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
Assertion	msrf	⊢ 𝑅 : 𝑃 ⟶ 𝑃

Proof

Step	Hyp	Ref	Expression
1		mpstssv.p	⊢ 𝑃 = ( mPreSt ‘ 𝑇 )
2		msrf.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
3		otex	⊢ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑇 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ ∈ V
4	3	csbex	⊢ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑇 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ ∈ V
5	4	csbex	⊢ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑇 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ ∈ V
6		eqid	⊢ ( mVars ‘ 𝑇 ) = ( mVars ‘ 𝑇 )
7	6 1 2	msrfval	⊢ 𝑅 = ( 𝑠 ∈ 𝑃 ↦ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) / ℎ ⦌ ⦋ ( 2^nd ‘ 𝑠 ) / 𝑎 ⦌ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ⦋ ∪ ( ( mVars ‘ 𝑇 ) “ ( ℎ ∪ { 𝑎 } ) ) / 𝑧 ⦌ ( 𝑧 × 𝑧 ) ) , ℎ , 𝑎 ⟩ )
8	5 7	fnmpti	⊢ 𝑅 Fn 𝑃
9	1	mpst123	⊢ ( 𝑠 ∈ 𝑃 → 𝑠 = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ )
10	9	fveq2d	⊢ ( 𝑠 ∈ 𝑃 → ( 𝑅 ‘ 𝑠 ) = ( 𝑅 ‘ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ ) )
11		id	⊢ ( 𝑠 ∈ 𝑃 → 𝑠 ∈ 𝑃 )
12	9 11	eqeltrrd	⊢ ( 𝑠 ∈ 𝑃 → ⟨ ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ ∈ 𝑃 )
13		eqid	⊢ ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) = ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) )
14	6 1 2 13	msrval	⊢ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ ∈ 𝑃 → ( 𝑅 ‘ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ ) = ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ )
15	12 14	syl	⊢ ( 𝑠 ∈ 𝑃 → ( 𝑅 ‘ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ ) = ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ )
16	10 15	eqtrd	⊢ ( 𝑠 ∈ 𝑃 → ( 𝑅 ‘ 𝑠 ) = ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ )
17		inss1	⊢ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) ⊆ ( 1^st ‘ ( 1^st ‘ 𝑠 ) )
18		eqid	⊢ ( mDV ‘ 𝑇 ) = ( mDV ‘ 𝑇 )
19		eqid	⊢ ( mEx ‘ 𝑇 ) = ( mEx ‘ 𝑇 )
20	18 19 1	elmpst	⊢ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ ∈ 𝑃 ↔ ( ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ⊆ ( mDV ‘ 𝑇 ) ∧ ^◡ ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ⊆ ( mEx ‘ 𝑇 ) ∧ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∈ Fin ) ∧ ( 2^nd ‘ 𝑠 ) ∈ ( mEx ‘ 𝑇 ) ) )
21	12 20	sylib	⊢ ( 𝑠 ∈ 𝑃 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ⊆ ( mDV ‘ 𝑇 ) ∧ ^◡ ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ⊆ ( mEx ‘ 𝑇 ) ∧ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∈ Fin ) ∧ ( 2^nd ‘ 𝑠 ) ∈ ( mEx ‘ 𝑇 ) ) )
22	21	simp1d	⊢ ( 𝑠 ∈ 𝑃 → ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ⊆ ( mDV ‘ 𝑇 ) ∧ ^◡ ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ) )
23	22	simpld	⊢ ( 𝑠 ∈ 𝑃 → ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ⊆ ( mDV ‘ 𝑇 ) )
24	17 23	sstrid	⊢ ( 𝑠 ∈ 𝑃 → ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) ⊆ ( mDV ‘ 𝑇 ) )
25		cnvin	⊢ ^◡ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) = ( ^◡ ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ^◡ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) )
26	22	simprd	⊢ ( 𝑠 ∈ 𝑃 → ^◡ ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) )
27		cnvxp	⊢ ^◡ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) = ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) )
28	27	a1i	⊢ ( 𝑠 ∈ 𝑃 → ^◡ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) = ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) )
29	26 28	ineq12d	⊢ ( 𝑠 ∈ 𝑃 → ( ^◡ ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ^◡ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) )
30	25 29	syl5eq	⊢ ( 𝑠 ∈ 𝑃 → ^◡ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) )
31	24 30	jca	⊢ ( 𝑠 ∈ 𝑃 → ( ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) ⊆ ( mDV ‘ 𝑇 ) ∧ ^◡ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) ) )
32	21	simp2d	⊢ ( 𝑠 ∈ 𝑃 → ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ⊆ ( mEx ‘ 𝑇 ) ∧ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∈ Fin ) )
33	21	simp3d	⊢ ( 𝑠 ∈ 𝑃 → ( 2^nd ‘ 𝑠 ) ∈ ( mEx ‘ 𝑇 ) )
34	18 19 1	elmpst	⊢ ( ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ ∈ 𝑃 ↔ ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) ⊆ ( mDV ‘ 𝑇 ) ∧ ^◡ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ⊆ ( mEx ‘ 𝑇 ) ∧ ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∈ Fin ) ∧ ( 2^nd ‘ 𝑠 ) ∈ ( mEx ‘ 𝑇 ) ) )
35	31 32 33 34	syl3anbrc	⊢ ( 𝑠 ∈ 𝑃 → ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ ∈ 𝑃 )
36	16 35	eqeltrd	⊢ ( 𝑠 ∈ 𝑃 → ( 𝑅 ‘ 𝑠 ) ∈ 𝑃 )
37	36	rgen	⊢ ∀ 𝑠 ∈ 𝑃 ( 𝑅 ‘ 𝑠 ) ∈ 𝑃
38		ffnfv	⊢ ( 𝑅 : 𝑃 ⟶ 𝑃 ↔ ( 𝑅 Fn 𝑃 ∧ ∀ 𝑠 ∈ 𝑃 ( 𝑅 ‘ 𝑠 ) ∈ 𝑃 ) )
39	8 37 38	mpbir2an	⊢ 𝑅 : 𝑃 ⟶ 𝑃

Metamath Proof Explorer

Theorem msrf

Proof