Step | Hyp | Ref
| Expression |
1 | | n0i 3920 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅) |
2 | | mrsubccat.s |
. . . . . 6
⊢ 𝑆 = (mRSubst‘𝑇) |
3 | | fvprc 6185 |
. . . . . 6
⊢ (¬
𝑇 ∈ V →
(mRSubst‘𝑇) =
∅) |
4 | 2, 3 | syl5eq 2668 |
. . . . 5
⊢ (¬
𝑇 ∈ V → 𝑆 = ∅) |
5 | 4 | rneqd 5353 |
. . . 4
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ran ∅) |
6 | | rn0 5377 |
. . . 4
⊢ ran
∅ = ∅ |
7 | 5, 6 | syl6eq 2672 |
. . 3
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ∅) |
8 | 1, 7 | nsyl2 142 |
. 2
⊢ (𝐹 ∈ ran 𝑆 → 𝑇 ∈ V) |
9 | | eqid 2622 |
. . . . 5
⊢
(mVR‘𝑇) =
(mVR‘𝑇) |
10 | | eqid 2622 |
. . . . 5
⊢
(mREx‘𝑇) =
(mREx‘𝑇) |
11 | 9, 10, 2 | mrsubff 31409 |
. . . 4
⊢ (𝑇 ∈ V → 𝑆:((mREx‘𝑇) ↑pm
(mVR‘𝑇))⟶((mREx‘𝑇) ↑𝑚
(mREx‘𝑇))) |
12 | | ffun 6048 |
. . . 4
⊢ (𝑆:((mREx‘𝑇) ↑pm
(mVR‘𝑇))⟶((mREx‘𝑇) ↑𝑚
(mREx‘𝑇)) → Fun
𝑆) |
13 | 8, 11, 12 | 3syl 18 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 → Fun 𝑆) |
14 | 9, 10, 2 | mrsubrn 31410 |
. . . . 5
⊢ ran 𝑆 = (𝑆 “ ((mREx‘𝑇) ↑𝑚
(mVR‘𝑇))) |
15 | 14 | eleq2i 2693 |
. . . 4
⊢ (𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ (𝑆 “ ((mREx‘𝑇) ↑𝑚
(mVR‘𝑇)))) |
16 | 15 | biimpi 206 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 → 𝐹 ∈ (𝑆 “ ((mREx‘𝑇) ↑𝑚
(mVR‘𝑇)))) |
17 | | fvelima 6248 |
. . 3
⊢ ((Fun
𝑆 ∧ 𝐹 ∈ (𝑆 “ ((mREx‘𝑇) ↑𝑚
(mVR‘𝑇)))) →
∃𝑓 ∈
((mREx‘𝑇)
↑𝑚 (mVR‘𝑇))(𝑆‘𝑓) = 𝐹) |
18 | 13, 16, 17 | syl2anc 693 |
. 2
⊢ (𝐹 ∈ ran 𝑆 → ∃𝑓 ∈ ((mREx‘𝑇) ↑𝑚
(mVR‘𝑇))(𝑆‘𝑓) = 𝐹) |
19 | | elmapi 7879 |
. . . . . . 7
⊢ (𝑓 ∈ ((mREx‘𝑇) ↑𝑚
(mVR‘𝑇)) → 𝑓:(mVR‘𝑇)⟶(mREx‘𝑇)) |
20 | 19 | adantl 482 |
. . . . . 6
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ ((mREx‘𝑇) ↑𝑚
(mVR‘𝑇))) →
𝑓:(mVR‘𝑇)⟶(mREx‘𝑇)) |
21 | | ssid 3624 |
. . . . . . 7
⊢
(mVR‘𝑇)
⊆ (mVR‘𝑇) |
22 | 21 | a1i 11 |
. . . . . 6
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ ((mREx‘𝑇) ↑𝑚
(mVR‘𝑇))) →
(mVR‘𝑇) ⊆
(mVR‘𝑇)) |
23 | | wrd0 13330 |
. . . . . . 7
⊢ ∅
∈ Word ((mCN‘𝑇)
∪ (mVR‘𝑇)) |
24 | | eqid 2622 |
. . . . . . . . 9
⊢
(mCN‘𝑇) =
(mCN‘𝑇) |
25 | 24, 9, 10 | mrexval 31398 |
. . . . . . . 8
⊢ (𝑇 ∈ V →
(mREx‘𝑇) = Word
((mCN‘𝑇) ∪
(mVR‘𝑇))) |
26 | 25 | adantr 481 |
. . . . . . 7
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ ((mREx‘𝑇) ↑𝑚
(mVR‘𝑇))) →
(mREx‘𝑇) = Word
((mCN‘𝑇) ∪
(mVR‘𝑇))) |
27 | 23, 26 | syl5eleqr 2708 |
. . . . . 6
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ ((mREx‘𝑇) ↑𝑚
(mVR‘𝑇))) →
∅ ∈ (mREx‘𝑇)) |
28 | | eqid 2622 |
. . . . . . 7
⊢
(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) = (freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) |
29 | 24, 9, 10, 2, 28 | mrsubval 31406 |
. . . . . 6
⊢ ((𝑓:(mVR‘𝑇)⟶(mREx‘𝑇) ∧ (mVR‘𝑇) ⊆ (mVR‘𝑇) ∧ ∅ ∈ (mREx‘𝑇)) → ((𝑆‘𝑓)‘∅) =
((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘
∅))) |
30 | 20, 22, 27, 29 | syl3anc 1326 |
. . . . 5
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ ((mREx‘𝑇) ↑𝑚
(mVR‘𝑇))) →
((𝑆‘𝑓)‘∅) =
((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘
∅))) |
31 | | co02 5649 |
. . . . . . 7
⊢ ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ ∅) =
∅ |
32 | 31 | oveq2i 6661 |
. . . . . 6
⊢
((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ ∅)) =
((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg
∅) |
33 | 28 | frmd0 17397 |
. . . . . . 7
⊢ ∅ =
(0g‘(freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇)))) |
34 | 33 | gsum0 17278 |
. . . . . 6
⊢
((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ∅) =
∅ |
35 | 32, 34 | eqtri 2644 |
. . . . 5
⊢
((freeMnd‘((mCN‘𝑇) ∪ (mVR‘𝑇))) Σg ((𝑣 ∈ ((mCN‘𝑇) ∪ (mVR‘𝑇)) ↦ if(𝑣 ∈ (mVR‘𝑇), (𝑓‘𝑣), 〈“𝑣”〉)) ∘ ∅)) =
∅ |
36 | 30, 35 | syl6eq 2672 |
. . . 4
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ ((mREx‘𝑇) ↑𝑚
(mVR‘𝑇))) →
((𝑆‘𝑓)‘∅) =
∅) |
37 | | fveq1 6190 |
. . . . 5
⊢ ((𝑆‘𝑓) = 𝐹 → ((𝑆‘𝑓)‘∅) = (𝐹‘∅)) |
38 | 37 | eqeq1d 2624 |
. . . 4
⊢ ((𝑆‘𝑓) = 𝐹 → (((𝑆‘𝑓)‘∅) = ∅ ↔ (𝐹‘∅) =
∅)) |
39 | 36, 38 | syl5ibcom 235 |
. . 3
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ ((mREx‘𝑇) ↑𝑚
(mVR‘𝑇))) →
((𝑆‘𝑓) = 𝐹 → (𝐹‘∅) = ∅)) |
40 | 39 | rexlimdva 3031 |
. 2
⊢ (𝑇 ∈ V → (∃𝑓 ∈ ((mREx‘𝑇) ↑𝑚
(mVR‘𝑇))(𝑆‘𝑓) = 𝐹 → (𝐹‘∅) = ∅)) |
41 | 8, 18, 40 | sylc 65 |
1
⊢ (𝐹 ∈ ran 𝑆 → (𝐹‘∅) = ∅) |