elmsubrn

Description: Characterization of substitution in terms of raw substitution, without reference to the generating functions. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	elmsubrn.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
	elmsubrn.o	⊢ 𝑂 = ( mRSubst ‘ 𝑇 )
	elmsubrn.s	⊢ 𝑆 = ( mSubst ‘ 𝑇 )
Assertion	elmsubrn	⊢ ran 𝑆 = ran ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		elmsubrn.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
2		elmsubrn.o	⊢ 𝑂 = ( mRSubst ‘ 𝑇 )
3		elmsubrn.s	⊢ 𝑆 = ( mSubst ‘ 𝑇 )
4		eqid	⊢ ( mVR ‘ 𝑇 ) = ( mVR ‘ 𝑇 )
5		eqid	⊢ ( mREx ‘ 𝑇 ) = ( mREx ‘ 𝑇 )
6	4 5 3 1 2	msubffval	⊢ ( 𝑇 ∈ V → 𝑆 = ( 𝑔 ∈ ( ( mREx ‘ 𝑇 ) ↑_pm ( mVR ‘ 𝑇 ) ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝑔 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )
7	4 5 2	mrsubff	⊢ ( 𝑇 ∈ V → 𝑂 : ( ( mREx ‘ 𝑇 ) ↑_pm ( mVR ‘ 𝑇 ) ) ⟶ ( ( mREx ‘ 𝑇 ) ↑_m ( mREx ‘ 𝑇 ) ) )
8	7	ffnd	⊢ ( 𝑇 ∈ V → 𝑂 Fn ( ( mREx ‘ 𝑇 ) ↑_pm ( mVR ‘ 𝑇 ) ) )
9		fnfvelrn	⊢ ( ( 𝑂 Fn ( ( mREx ‘ 𝑇 ) ↑_pm ( mVR ‘ 𝑇 ) ) ∧ 𝑔 ∈ ( ( mREx ‘ 𝑇 ) ↑_pm ( mVR ‘ 𝑇 ) ) ) → ( 𝑂 ‘ 𝑔 ) ∈ ran 𝑂 )
10	8 9	sylan	⊢ ( ( 𝑇 ∈ V ∧ 𝑔 ∈ ( ( mREx ‘ 𝑇 ) ↑_pm ( mVR ‘ 𝑇 ) ) ) → ( 𝑂 ‘ 𝑔 ) ∈ ran 𝑂 )
11	7	feqmptd	⊢ ( 𝑇 ∈ V → 𝑂 = ( 𝑔 ∈ ( ( mREx ‘ 𝑇 ) ↑_pm ( mVR ‘ 𝑇 ) ) ↦ ( 𝑂 ‘ 𝑔 ) ) )
12		eqidd	⊢ ( 𝑇 ∈ V → ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) = ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )
13		fveq1	⊢ ( 𝑓 = ( 𝑂 ‘ 𝑔 ) → ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) = ( ( 𝑂 ‘ 𝑔 ) ‘ ( 2^nd ‘ 𝑒 ) ) )
14	13	opeq2d	⊢ ( 𝑓 = ( 𝑂 ‘ 𝑔 ) → ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ = ⟨ ( 1^st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝑔 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ )
15	14	mpteq2dv	⊢ ( 𝑓 = ( 𝑂 ‘ 𝑔 ) → ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) = ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝑔 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) )
16	10 11 12 15	fmptco	⊢ ( 𝑇 ∈ V → ( ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) ∘ 𝑂 ) = ( 𝑔 ∈ ( ( mREx ‘ 𝑇 ) ↑_pm ( mVR ‘ 𝑇 ) ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( 𝑂 ‘ 𝑔 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )
17	6 16	eqtr4d	⊢ ( 𝑇 ∈ V → 𝑆 = ( ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) ∘ 𝑂 ) )
18	17	rneqd	⊢ ( 𝑇 ∈ V → ran 𝑆 = ran ( ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) ∘ 𝑂 ) )
19		rnco	⊢ ran ( ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) ∘ 𝑂 ) = ran ( ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) ↾ ran 𝑂 )
20		ssid	⊢ ran 𝑂 ⊆ ran 𝑂
21		resmpt	⊢ ( ran 𝑂 ⊆ ran 𝑂 → ( ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) ↾ ran 𝑂 ) = ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )
22	20 21	ax-mp	⊢ ( ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) ↾ ran 𝑂 ) = ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) )
23	22	rneqi	⊢ ran ( ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) ↾ ran 𝑂 ) = ran ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) )
24	19 23	eqtri	⊢ ran ( ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) ∘ 𝑂 ) = ran ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) )
25	18 24	eqtrdi	⊢ ( 𝑇 ∈ V → ran 𝑆 = ran ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )
26		mpt0	⊢ ( 𝑓 ∈ ∅ ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) = ∅
27	26	eqcomi	⊢ ∅ = ( 𝑓 ∈ ∅ ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) )
28		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mSubst ‘ 𝑇 ) = ∅ )
29	3 28	eqtrid	⊢ ( ¬ 𝑇 ∈ V → 𝑆 = ∅ )
30	2	rnfvprc	⊢ ( ¬ 𝑇 ∈ V → ran 𝑂 = ∅ )
31	30	mpteq1d	⊢ ( ¬ 𝑇 ∈ V → ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) = ( 𝑓 ∈ ∅ ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )
32	27 29 31	3eqtr4a	⊢ ( ¬ 𝑇 ∈ V → 𝑆 = ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )
33	32	rneqd	⊢ ( ¬ 𝑇 ∈ V → ran 𝑆 = ran ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )
34	25 33	pm2.61i	⊢ ran 𝑆 = ran ( 𝑓 ∈ ran 𝑂 ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( 𝑓 ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) )

Metamath Proof Explorer

Theorem elmsubrn

Proof