msrid

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

	Ref	Expression
Hypotheses	mstaval.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
	mstaval.s	⊢ 𝑆 = ( mStat ‘ 𝑇 )
Assertion	msrid	⊢ ( 𝑋 ∈ 𝑆 → ( 𝑅 ‘ 𝑋 ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		mstaval.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
2		mstaval.s	⊢ 𝑆 = ( mStat ‘ 𝑇 )
3		eqid	⊢ ( mPreSt ‘ 𝑇 ) = ( mPreSt ‘ 𝑇 )
4	3 1	msrf	⊢ 𝑅 : ( mPreSt ‘ 𝑇 ) ⟶ ( mPreSt ‘ 𝑇 )
5		ffn	⊢ ( 𝑅 : ( mPreSt ‘ 𝑇 ) ⟶ ( mPreSt ‘ 𝑇 ) → 𝑅 Fn ( mPreSt ‘ 𝑇 ) )
6		fvelrnb	⊢ ( 𝑅 Fn ( mPreSt ‘ 𝑇 ) → ( 𝑋 ∈ ran 𝑅 ↔ ∃ 𝑠 ∈ ( mPreSt ‘ 𝑇 ) ( 𝑅 ‘ 𝑠 ) = 𝑋 ) )
7	4 5 6	mp2b	⊢ ( 𝑋 ∈ ran 𝑅 ↔ ∃ 𝑠 ∈ ( mPreSt ‘ 𝑇 ) ( 𝑅 ‘ 𝑠 ) = 𝑋 )
8	3	mpst123	⊢ ( 𝑠 ∈ ( mPreSt ‘ 𝑇 ) → 𝑠 = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ )
9	8	fveq2d	⊢ ( 𝑠 ∈ ( mPreSt ‘ 𝑇 ) → ( 𝑅 ‘ 𝑠 ) = ( 𝑅 ‘ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ ) )
10		id	⊢ ( 𝑠 ∈ ( mPreSt ‘ 𝑇 ) → 𝑠 ∈ ( mPreSt ‘ 𝑇 ) )
11	8 10	eqeltrrd	⊢ ( 𝑠 ∈ ( mPreSt ‘ 𝑇 ) → ⟨ ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ ∈ ( mPreSt ‘ 𝑇 ) )
12		eqid	⊢ ( mVars ‘ 𝑇 ) = ( mVars ‘ 𝑇 )
13		eqid	⊢ ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) = ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) )
14	12 3 1 13	msrval	⊢ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ ∈ ( mPreSt ‘ 𝑇 ) → ( 𝑅 ‘ ⟨ ( 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	11 14	syl	⊢ ( 𝑠 ∈ ( mPreSt ‘ 𝑇 ) → ( 𝑅 ‘ ⟨ ( 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	9 15	eqtrd	⊢ ( 𝑠 ∈ ( mPreSt ‘ 𝑇 ) → ( 𝑅 ‘ 𝑠 ) = ⟨ ( ( 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	4	ffvelcdmi	⊢ ( 𝑠 ∈ ( mPreSt ‘ 𝑇 ) → ( 𝑅 ‘ 𝑠 ) ∈ ( mPreSt ‘ 𝑇 ) )
18	16 17	eqeltrrd	⊢ ( 𝑠 ∈ ( mPreSt ‘ 𝑇 ) → ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ ∈ ( mPreSt ‘ 𝑇 ) )
19	12 3 1 13	msrval	⊢ ( ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ ∈ ( mPreSt ‘ 𝑇 ) → ( 𝑅 ‘ ⟨ ( ( 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 ‘ 𝑠 ) } ) ) ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ )
20	18 19	syl	⊢ ( 𝑠 ∈ ( mPreSt ‘ 𝑇 ) → ( 𝑅 ‘ ⟨ ( ( 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 ‘ 𝑠 ) } ) ) ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ )
21		inass	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( 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 ‘ 𝑠 ) } ) ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ( ∪ ( ( 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 ‘ 𝑠 ) } ) ) ) ) )
22		inidm	⊢ ( ( ∪ ( ( 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 ‘ 𝑠 ) } ) ) ) ) = ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) )
23	22	ineq2i	⊢ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ( ∪ ( ( 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 ‘ 𝑠 ) } ) ) ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) )
24	21 23	eqtri	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( 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 ‘ 𝑠 ) } ) ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) )
25	24	a1i	⊢ ( 𝑠 ∈ ( mPreSt ‘ 𝑇 ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( 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 ‘ 𝑠 ) } ) ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) )
26	25	oteq1d	⊢ ( 𝑠 ∈ ( mPreSt ‘ 𝑇 ) → ⟨ ( ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( 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 ‘ 𝑠 ) } ) ) ) ) , ( 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 ‘ 𝑠 ) ⟩ )
27	20 26	eqtrd	⊢ ( 𝑠 ∈ ( mPreSt ‘ 𝑇 ) → ( 𝑅 ‘ ⟨ ( ( 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 ‘ 𝑠 ) } ) ) ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ )
28	16	fveq2d	⊢ ( 𝑠 ∈ ( mPreSt ‘ 𝑇 ) → ( 𝑅 ‘ ( 𝑅 ‘ 𝑠 ) ) = ( 𝑅 ‘ ⟨ ( ( 1^st ‘ ( 1^st ‘ 𝑠 ) ) ∩ ( ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) × ∪ ( ( mVars ‘ 𝑇 ) “ ( ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) ∪ { ( 2^nd ‘ 𝑠 ) } ) ) ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑠 ) ) , ( 2^nd ‘ 𝑠 ) ⟩ ) )
29	27 28 16	3eqtr4d	⊢ ( 𝑠 ∈ ( mPreSt ‘ 𝑇 ) → ( 𝑅 ‘ ( 𝑅 ‘ 𝑠 ) ) = ( 𝑅 ‘ 𝑠 ) )
30		fveq2	⊢ ( ( 𝑅 ‘ 𝑠 ) = 𝑋 → ( 𝑅 ‘ ( 𝑅 ‘ 𝑠 ) ) = ( 𝑅 ‘ 𝑋 ) )
31		id	⊢ ( ( 𝑅 ‘ 𝑠 ) = 𝑋 → ( 𝑅 ‘ 𝑠 ) = 𝑋 )
32	30 31	eqeq12d	⊢ ( ( 𝑅 ‘ 𝑠 ) = 𝑋 → ( ( 𝑅 ‘ ( 𝑅 ‘ 𝑠 ) ) = ( 𝑅 ‘ 𝑠 ) ↔ ( 𝑅 ‘ 𝑋 ) = 𝑋 ) )
33	29 32	syl5ibcom	⊢ ( 𝑠 ∈ ( mPreSt ‘ 𝑇 ) → ( ( 𝑅 ‘ 𝑠 ) = 𝑋 → ( 𝑅 ‘ 𝑋 ) = 𝑋 ) )
34	33	rexlimiv	⊢ ( ∃ 𝑠 ∈ ( mPreSt ‘ 𝑇 ) ( 𝑅 ‘ 𝑠 ) = 𝑋 → ( 𝑅 ‘ 𝑋 ) = 𝑋 )
35	7 34	sylbi	⊢ ( 𝑋 ∈ ran 𝑅 → ( 𝑅 ‘ 𝑋 ) = 𝑋 )
36	1 2	mstaval	⊢ 𝑆 = ran 𝑅
37	35 36	eleq2s	⊢ ( 𝑋 ∈ 𝑆 → ( 𝑅 ‘ 𝑋 ) = 𝑋 )

Metamath Proof Explorer

Theorem msrid

Proof