Metamath Proof Explorer

Theorem msubrn

Description: Although it is defined for partial mappings of variables, every partial substitution is a substitution on some complete mapping of the variables. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses msubff.v ⊢ 𝑉 = ( mVR ‘ 𝑇 )
msubff.r ⊢ 𝑅 = ( mREx ‘ 𝑇 )
msubff.s ⊢ 𝑆 = ( mSubst ‘ 𝑇 )
Assertion msubrn ran 𝑆 = ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) )

Proof

Step Hyp Ref Expression
1 msubff.v ⊢ 𝑉 = ( mVR ‘ 𝑇 )
2 msubff.r ⊢ 𝑅 = ( mREx ‘ 𝑇 )
3 msubff.s ⊢ 𝑆 = ( mSubst ‘ 𝑇 )
4 eqid ⊢ ( mEx ‘ 𝑇 ) = ( mEx ‘ 𝑇 )
5 eqid ⊢ ( mRSubst ‘ 𝑇 ) = ( mRSubst ‘ 𝑇 )
6 1 2 3 4 5 msubffval ⊢ ( 𝑇 ∈ V → 𝑆 = ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ) )
7 6 rneqd ⊢ ( 𝑇 ∈ V → ran 𝑆 = ran ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ) )
8 1 2 5 mrsubff ⊢ ( 𝑇 ∈ V → ( mRSubst ‘ 𝑇 ) : ( 𝑅 ↑pm 𝑉 ) ⟶ ( 𝑅 ↑m 𝑅 ) )
9 8 adantr ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( mRSubst ‘ 𝑇 ) : ( 𝑅 ↑pm 𝑉 ) ⟶ ( 𝑅 ↑m 𝑅 ) )
10 9 ffund ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → Fun ( mRSubst ‘ 𝑇 ) )
11 8 ffnd ⊢ ( 𝑇 ∈ V → ( mRSubst ‘ 𝑇 ) Fn ( 𝑅 ↑pm 𝑉 ) )
12 fnfvelrn ⊢ ( ( ( mRSubst ‘ 𝑇 ) Fn ( 𝑅 ↑pm 𝑉 ) ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ∈ ran ( mRSubst ‘ 𝑇 ) )
13 11 12 sylan ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ∈ ran ( mRSubst ‘ 𝑇 ) )
14 1 2 5 mrsubrn ⊢ ran ( mRSubst ‘ 𝑇 ) = ( ( mRSubst ‘ 𝑇 ) “ ( 𝑅 ↑m 𝑉 ) )
15 13 14 eleqtrdi ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ∈ ( ( mRSubst ‘ 𝑇 ) “ ( 𝑅 ↑m 𝑉 ) ) )
16 fvelima ⊢ ( ( Fun ( mRSubst ‘ 𝑇 ) ∧ ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ∈ ( ( mRSubst ‘ 𝑇 ) “ ( 𝑅 ↑m 𝑉 ) ) ) → ∃ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) = ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) )
17 10 15 16 syl2anc ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ∃ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) = ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) )
18 elmapi ⊢ ( 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) → 𝑔 : 𝑉 ⟶ 𝑅 )
19 18 adantl ⊢ ( ( 𝑇 ∈ V ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝑔 : 𝑉 ⟶ 𝑅 )
20 ssid ⊢ 𝑉 ⊆ 𝑉
21 1 2 3 4 5 msubfval ⊢ ( ( 𝑔 : 𝑉 ⟶ 𝑅 ∧ 𝑉 ⊆ 𝑉 ) → ( 𝑆 ‘ 𝑔 ) = ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) )
22 19 20 21 sylancl ⊢ ( ( 𝑇 ∈ V ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑆 ‘ 𝑔 ) = ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) )
23 fvex ⊢ ( mEx ‘ 𝑇 ) ∈ V
24 23 mptex ⊢ ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ∈ V
25 eqid ⊢ ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ) = ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) )
26 24 25 fnmpti ⊢ ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ) Fn ( 𝑅 ↑pm 𝑉 )
27 6 fneq1d ⊢ ( 𝑇 ∈ V → ( 𝑆 Fn ( 𝑅 ↑pm 𝑉 ) ↔ ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ) Fn ( 𝑅 ↑pm 𝑉 ) ) )
28 26 27 mpbiri ⊢ ( 𝑇 ∈ V → 𝑆 Fn ( 𝑅 ↑pm 𝑉 ) )
29 28 adantr ⊢ ( ( 𝑇 ∈ V ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝑆 Fn ( 𝑅 ↑pm 𝑉 ) )
30 mapsspm ⊢ ( 𝑅 ↑m 𝑉 ) ⊆ ( 𝑅 ↑pm 𝑉 )
31 30 a1i ⊢ ( ( 𝑇 ∈ V ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑅 ↑m 𝑉 ) ⊆ ( 𝑅 ↑pm 𝑉 ) )
32 simpr ⊢ ( ( 𝑇 ∈ V ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) )
33 fnfvima ⊢ ( ( 𝑆 Fn ( 𝑅 ↑pm 𝑉 ) ∧ ( 𝑅 ↑m 𝑉 ) ⊆ ( 𝑅 ↑pm 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑆 ‘ 𝑔 ) ∈ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) )
34 29 31 32 33 syl3anc ⊢ ( ( 𝑇 ∈ V ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑆 ‘ 𝑔 ) ∈ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) )
35 22 34 eqeltrrd ⊢ ( ( 𝑇 ∈ V ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ∈ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) )
36 35 adantlr ⊢ ( ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ∈ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) )
37 fveq1 ⊢ ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) = ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) → ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ ( 2nd ‘ 𝑒 ) ) = ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) )
38 37 opeq2d ⊢ ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) = ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) → ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ = ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ )
39 38 mpteq2dv ⊢ ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) = ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) → ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) = ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) )
40 39 eleq1d ⊢ ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) = ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) → ( ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ∈ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) ↔ ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ∈ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) ) )
41 36 40 syl5ibcom ⊢ ( ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) = ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) → ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ∈ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) ) )
42 41 rexlimdva ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( ∃ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) = ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) → ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ∈ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) ) )
43 17 42 mpd ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ∈ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) )
44 43 fmpttd ⊢ ( 𝑇 ∈ V → ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ) : ( 𝑅 ↑pm 𝑉 ) ⟶ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) )
45 44 frnd ⊢ ( 𝑇 ∈ V → ran ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ↦ ( 𝑒 ∈ ( mEx ‘ 𝑇 ) ↦ ⟨ ( 1st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ 𝑒 ) ) ⟩ ) ) ⊆ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) )
46 7 45 eqsstrd ⊢ ( 𝑇 ∈ V → ran 𝑆 ⊆ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) )
47 3 rnfvprc ⊢ ( ¬ 𝑇 ∈ V → ran 𝑆 = ∅ )
48 0ss ⊢ ∅ ⊆ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) )
49 47 48 eqsstrdi ⊢ ( ¬ 𝑇 ∈ V → ran 𝑆 ⊆ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) )
50 46 49 pm2.61i ⊢ ran 𝑆 ⊆ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) )
51 imassrn ⊢ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) ⊆ ran 𝑆
52 50 51 eqssi ⊢ ran 𝑆 = ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) )