| Step | Hyp | Ref
| Expression |
| 1 | | n0i 4340 |
. . . . . 6
⊢ (𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅) |
| 2 | | mrsubco.s |
. . . . . . 7
⊢ 𝑆 = (mRSubst‘𝑇) |
| 3 | 2 | rnfvprc 6900 |
. . . . . 6
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ∅) |
| 4 | 1, 3 | nsyl2 141 |
. . . . 5
⊢ (𝐹 ∈ ran 𝑆 → 𝑇 ∈ V) |
| 5 | | eqid 2737 |
. . . . . 6
⊢
(mCN‘𝑇) =
(mCN‘𝑇) |
| 6 | | mrsubvrs.v |
. . . . . 6
⊢ 𝑉 = (mVR‘𝑇) |
| 7 | | mrsubvrs.r |
. . . . . 6
⊢ 𝑅 = (mREx‘𝑇) |
| 8 | 5, 6, 7 | mrexval 35506 |
. . . . 5
⊢ (𝑇 ∈ V → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉)) |
| 9 | 4, 8 | syl 17 |
. . . 4
⊢ (𝐹 ∈ ran 𝑆 → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉)) |
| 10 | 9 | eleq2d 2827 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝑅 ↔ 𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉))) |
| 11 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑣 = ∅ → (𝐹‘𝑣) = (𝐹‘∅)) |
| 12 | 11 | rneqd 5949 |
. . . . . . . 8
⊢ (𝑣 = ∅ → ran (𝐹‘𝑣) = ran (𝐹‘∅)) |
| 13 | 12 | ineq1d 4219 |
. . . . . . 7
⊢ (𝑣 = ∅ → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘∅) ∩ 𝑉)) |
| 14 | | rneq 5947 |
. . . . . . . . . . . 12
⊢ (𝑣 = ∅ → ran 𝑣 = ran ∅) |
| 15 | | rn0 5936 |
. . . . . . . . . . . 12
⊢ ran
∅ = ∅ |
| 16 | 14, 15 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑣 = ∅ → ran 𝑣 = ∅) |
| 17 | 16 | ineq1d 4219 |
. . . . . . . . . 10
⊢ (𝑣 = ∅ → (ran 𝑣 ∩ 𝑉) = (∅ ∩ 𝑉)) |
| 18 | | 0in 4397 |
. . . . . . . . . 10
⊢ (∅
∩ 𝑉) =
∅ |
| 19 | 17, 18 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑣 = ∅ → (ran 𝑣 ∩ 𝑉) = ∅) |
| 20 | 19 | iuneq1d 5019 |
. . . . . . . 8
⊢ (𝑣 = ∅ → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∪
𝑥 ∈ ∅ (ran
(𝐹‘〈“𝑥”〉) ∩ 𝑉)) |
| 21 | | 0iun 5063 |
. . . . . . . 8
⊢ ∪ 𝑥 ∈ ∅ (ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∅ |
| 22 | 20, 21 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝑣 = ∅ → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∅) |
| 23 | 13, 22 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑣 = ∅ → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ↔ (ran (𝐹‘∅) ∩ 𝑉) = ∅)) |
| 24 | 23 | imbi2d 340 |
. . . . 5
⊢ (𝑣 = ∅ → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = ∅))) |
| 25 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑣 = 𝑦 → (𝐹‘𝑣) = (𝐹‘𝑦)) |
| 26 | 25 | rneqd 5949 |
. . . . . . . 8
⊢ (𝑣 = 𝑦 → ran (𝐹‘𝑣) = ran (𝐹‘𝑦)) |
| 27 | 26 | ineq1d 4219 |
. . . . . . 7
⊢ (𝑣 = 𝑦 → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘𝑦) ∩ 𝑉)) |
| 28 | | rneq 5947 |
. . . . . . . . 9
⊢ (𝑣 = 𝑦 → ran 𝑣 = ran 𝑦) |
| 29 | 28 | ineq1d 4219 |
. . . . . . . 8
⊢ (𝑣 = 𝑦 → (ran 𝑣 ∩ 𝑉) = (ran 𝑦 ∩ 𝑉)) |
| 30 | 29 | iuneq1d 5019 |
. . . . . . 7
⊢ (𝑣 = 𝑦 → ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) |
| 31 | 27, 30 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑣 = 𝑦 → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ↔ (ran (𝐹‘𝑦) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉))) |
| 32 | 31 | imbi2d 340 |
. . . . 5
⊢ (𝑣 = 𝑦 → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑦) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)))) |
| 33 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑣 = (𝑦 ++ 〈“𝑧”〉) → (𝐹‘𝑣) = (𝐹‘(𝑦 ++ 〈“𝑧”〉))) |
| 34 | 33 | rneqd 5949 |
. . . . . . . 8
⊢ (𝑣 = (𝑦 ++ 〈“𝑧”〉) → ran (𝐹‘𝑣) = ran (𝐹‘(𝑦 ++ 〈“𝑧”〉))) |
| 35 | 34 | ineq1d 4219 |
. . . . . . 7
⊢ (𝑣 = (𝑦 ++ 〈“𝑧”〉) → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉)) |
| 36 | | rneq 5947 |
. . . . . . . . 9
⊢ (𝑣 = (𝑦 ++ 〈“𝑧”〉) → ran 𝑣 = ran (𝑦 ++ 〈“𝑧”〉)) |
| 37 | 36 | ineq1d 4219 |
. . . . . . . 8
⊢ (𝑣 = (𝑦 ++ 〈“𝑧”〉) → (ran 𝑣 ∩ 𝑉) = (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)) |
| 38 | 37 | iuneq1d 5019 |
. . . . . . 7
⊢ (𝑣 = (𝑦 ++ 〈“𝑧”〉) → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∪
𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) |
| 39 | 35, 38 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑣 = (𝑦 ++ 〈“𝑧”〉) → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ↔ (ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉) = ∪
𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉))) |
| 40 | 39 | imbi2d 340 |
. . . . 5
⊢ (𝑣 = (𝑦 ++ 〈“𝑧”〉) → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉) = ∪
𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)))) |
| 41 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑣 = 𝑋 → (𝐹‘𝑣) = (𝐹‘𝑋)) |
| 42 | 41 | rneqd 5949 |
. . . . . . . 8
⊢ (𝑣 = 𝑋 → ran (𝐹‘𝑣) = ran (𝐹‘𝑋)) |
| 43 | 42 | ineq1d 4219 |
. . . . . . 7
⊢ (𝑣 = 𝑋 → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘𝑋) ∩ 𝑉)) |
| 44 | | rneq 5947 |
. . . . . . . . 9
⊢ (𝑣 = 𝑋 → ran 𝑣 = ran 𝑋) |
| 45 | 44 | ineq1d 4219 |
. . . . . . . 8
⊢ (𝑣 = 𝑋 → (ran 𝑣 ∩ 𝑉) = (ran 𝑋 ∩ 𝑉)) |
| 46 | 45 | iuneq1d 5019 |
. . . . . . 7
⊢ (𝑣 = 𝑋 → ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) |
| 47 | 43, 46 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑣 = 𝑋 → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ↔ (ran (𝐹‘𝑋) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉))) |
| 48 | 47 | imbi2d 340 |
. . . . 5
⊢ (𝑣 = 𝑋 → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)))) |
| 49 | 2 | mrsub0 35521 |
. . . . . . . . 9
⊢ (𝐹 ∈ ran 𝑆 → (𝐹‘∅) = ∅) |
| 50 | 49 | rneqd 5949 |
. . . . . . . 8
⊢ (𝐹 ∈ ran 𝑆 → ran (𝐹‘∅) = ran
∅) |
| 51 | 50, 15 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝐹 ∈ ran 𝑆 → ran (𝐹‘∅) = ∅) |
| 52 | 51 | ineq1d 4219 |
. . . . . 6
⊢ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = (∅ ∩ 𝑉)) |
| 53 | 52, 18 | eqtrdi 2793 |
. . . . 5
⊢ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = ∅) |
| 54 | | uneq1 4161 |
. . . . . . . 8
⊢ ((ran
(𝐹‘𝑦) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) → ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉)) = (∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ∪ (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉))) |
| 55 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝐹 ∈ ran 𝑆) |
| 56 | | simprl 771 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉)) |
| 57 | 9 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉)) |
| 58 | 56, 57 | eleqtrrd 2844 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑦 ∈ 𝑅) |
| 59 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉)) |
| 60 | 59 | s1cld 14641 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 〈“𝑧”〉 ∈ Word ((mCN‘𝑇) ∪ 𝑉)) |
| 61 | 60, 57 | eleqtrrd 2844 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 〈“𝑧”〉 ∈ 𝑅) |
| 62 | 2, 7 | mrsubccat 35523 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑦 ∈ 𝑅 ∧ 〈“𝑧”〉 ∈ 𝑅) → (𝐹‘(𝑦 ++ 〈“𝑧”〉)) = ((𝐹‘𝑦) ++ (𝐹‘〈“𝑧”〉))) |
| 63 | 55, 58, 61, 62 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘(𝑦 ++ 〈“𝑧”〉)) = ((𝐹‘𝑦) ++ (𝐹‘〈“𝑧”〉))) |
| 64 | 63 | rneqd 5949 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) = ran ((𝐹‘𝑦) ++ (𝐹‘〈“𝑧”〉))) |
| 65 | 2, 7 | mrsubf 35522 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅) |
| 66 | 65 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝐹:𝑅⟶𝑅) |
| 67 | 66, 58 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘𝑦) ∈ 𝑅) |
| 68 | 67, 57 | eleqtrd 2843 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘𝑦) ∈ Word ((mCN‘𝑇) ∪ 𝑉)) |
| 69 | 66, 61 | ffvelcdmd 7105 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘〈“𝑧”〉) ∈ 𝑅) |
| 70 | 69, 57 | eleqtrd 2843 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘〈“𝑧”〉) ∈ Word ((mCN‘𝑇) ∪ 𝑉)) |
| 71 | | ccatrn 14627 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑦) ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ (𝐹‘〈“𝑧”〉) ∈ Word ((mCN‘𝑇) ∪ 𝑉)) → ran ((𝐹‘𝑦) ++ (𝐹‘〈“𝑧”〉)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘〈“𝑧”〉))) |
| 72 | 68, 70, 71 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran ((𝐹‘𝑦) ++ (𝐹‘〈“𝑧”〉)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘〈“𝑧”〉))) |
| 73 | 64, 72 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘〈“𝑧”〉))) |
| 74 | 73 | ineq1d 4219 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∪ ran (𝐹‘〈“𝑧”〉)) ∩ 𝑉)) |
| 75 | | indir 4286 |
. . . . . . . . . 10
⊢ ((ran
(𝐹‘𝑦) ∪ ran (𝐹‘〈“𝑧”〉)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉)) |
| 76 | 74, 75 | eqtrdi 2793 |
. . . . . . . . 9
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉))) |
| 77 | | ccatrn 14627 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 〈“𝑧”〉 ∈ Word ((mCN‘𝑇) ∪ 𝑉)) → ran (𝑦 ++ 〈“𝑧”〉) = (ran 𝑦 ∪ ran 〈“𝑧”〉)) |
| 78 | 56, 60, 77 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝑦 ++ 〈“𝑧”〉) = (ran 𝑦 ∪ ran 〈“𝑧”〉)) |
| 79 | | s1rn 14637 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) → ran 〈“𝑧”〉 = {𝑧}) |
| 80 | 79 | ad2antll 729 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran 〈“𝑧”〉 = {𝑧}) |
| 81 | 80 | uneq2d 4168 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran 𝑦 ∪ ran 〈“𝑧”〉) = (ran 𝑦 ∪ {𝑧})) |
| 82 | 78, 81 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝑦 ++ 〈“𝑧”〉) = (ran 𝑦 ∪ {𝑧})) |
| 83 | 82 | ineq1d 4219 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉) = ((ran 𝑦 ∪ {𝑧}) ∩ 𝑉)) |
| 84 | | indir 4286 |
. . . . . . . . . . . . 13
⊢ ((ran
𝑦 ∪ {𝑧}) ∩ 𝑉) = ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉)) |
| 85 | 83, 84 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉) = ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))) |
| 86 | 85 | iuneq1d 5019 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∪
𝑥 ∈ ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) |
| 87 | | iunxun 5094 |
. . . . . . . . . . 11
⊢ ∪ 𝑥 ∈ ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = (∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ∪ ∪
𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) |
| 88 | 86, 87 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = (∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ∪ ∪
𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉))) |
| 89 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → 𝑧 ∈ 𝑉) |
| 90 | 89 | snssd 4809 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → {𝑧} ⊆ 𝑉) |
| 91 | | dfss2 3969 |
. . . . . . . . . . . . . . 15
⊢ ({𝑧} ⊆ 𝑉 ↔ ({𝑧} ∩ 𝑉) = {𝑧}) |
| 92 | 90, 91 | sylib 218 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ({𝑧} ∩ 𝑉) = {𝑧}) |
| 93 | 92 | iuneq1d 5019 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ∪
𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∪
𝑥 ∈ {𝑧} (ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) |
| 94 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
| 95 | | s1eq 14638 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → 〈“𝑥”〉 = 〈“𝑧”〉) |
| 96 | 95 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (𝐹‘〈“𝑥”〉) = (𝐹‘〈“𝑧”〉)) |
| 97 | 96 | rneqd 5949 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → ran (𝐹‘〈“𝑥”〉) = ran (𝐹‘〈“𝑧”〉)) |
| 98 | 97 | ineq1d 4219 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉)) |
| 99 | 94, 98 | iunxsn 5091 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑥 ∈ {𝑧} (ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉) |
| 100 | 93, 99 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ∪
𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉)) |
| 101 | | incom 4209 |
. . . . . . . . . . . . . . 15
⊢ ({𝑧} ∩ 𝑉) = (𝑉 ∩ {𝑧}) |
| 102 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ¬ 𝑧 ∈ 𝑉) |
| 103 | | disjsn 4711 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑉) |
| 104 | 102, 103 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (𝑉 ∩ {𝑧}) = ∅) |
| 105 | 101, 104 | eqtrid 2789 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ({𝑧} ∩ 𝑉) = ∅) |
| 106 | 105 | iuneq1d 5019 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ∪
𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∪
𝑥 ∈ ∅ (ran
(𝐹‘〈“𝑥”〉) ∩ 𝑉)) |
| 107 | 55 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝐹 ∈ ran 𝑆) |
| 108 | | eldif 3961 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉) ↔ (𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) ∧ ¬ 𝑧 ∈ 𝑉)) |
| 109 | 108 | biimpri 228 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉)) |
| 110 | 59, 109 | sylan 580 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉)) |
| 111 | | difun2 4481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((mCN‘𝑇)
∪ 𝑉) ∖ 𝑉) = ((mCN‘𝑇) ∖ 𝑉) |
| 112 | 110, 111 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ ((mCN‘𝑇) ∖ 𝑉)) |
| 113 | 2, 7, 6, 5 | mrsubcn 35524 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑧 ∈ ((mCN‘𝑇) ∖ 𝑉)) → (𝐹‘〈“𝑧”〉) = 〈“𝑧”〉) |
| 114 | 107, 112,
113 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (𝐹‘〈“𝑧”〉) = 〈“𝑧”〉) |
| 115 | 114 | rneqd 5949 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran (𝐹‘〈“𝑧”〉) = ran 〈“𝑧”〉) |
| 116 | 80 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran 〈“𝑧”〉 = {𝑧}) |
| 117 | 115, 116 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran (𝐹‘〈“𝑧”〉) = {𝑧}) |
| 118 | 117 | ineq1d 4219 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉) = ({𝑧} ∩ 𝑉)) |
| 119 | 118, 105 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉) = ∅) |
| 120 | 21, 106, 119 | 3eqtr4a 2803 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ∪
𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉)) |
| 121 | 100, 120 | pm2.61dan 813 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉)) |
| 122 | 121 | uneq2d 4168 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ∪ ∪
𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) = (∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ∪ (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉))) |
| 123 | 88, 122 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = (∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ∪ (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉))) |
| 124 | 76, 123 | eqeq12d 2753 |
. . . . . . . 8
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ((ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉) = ∪
𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ↔ ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉)) = (∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ∪ (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉)))) |
| 125 | 54, 124 | imbitrrid 246 |
. . . . . . 7
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ((ran (𝐹‘𝑦) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) → (ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉) = ∪
𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉))) |
| 126 | 125 | expcom 413 |
. . . . . 6
⊢ ((𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉)) → (𝐹 ∈ ran 𝑆 → ((ran (𝐹‘𝑦) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) → (ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉) = ∪
𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)))) |
| 127 | 126 | a2d 29 |
. . . . 5
⊢ ((𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉)) → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑦) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) → (𝐹 ∈ ran 𝑆 → (ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉) = ∪
𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)))) |
| 128 | 24, 32, 40, 48, 53, 127 | wrdind 14760 |
. . . 4
⊢ (𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉) → (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉))) |
| 129 | 128 | com12 32 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉) → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉))) |
| 130 | 10, 129 | sylbid 240 |
. 2
⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝑅 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉))) |
| 131 | 130 | imp 406 |
1
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅) → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) |