Step | Hyp | Ref
| Expression |
1 | | n0i 3879 |
. . . . . 6
⊢ (𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅) |
2 | | mrsubco.s |
. . . . . . . . 9
⊢ 𝑆 = (mRSubst‘𝑇) |
3 | | fvprc 6097 |
. . . . . . . . 9
⊢ (¬
𝑇 ∈ V →
(mRSubst‘𝑇) =
∅) |
4 | 2, 3 | syl5eq 2656 |
. . . . . . . 8
⊢ (¬
𝑇 ∈ V → 𝑆 = ∅) |
5 | 4 | rneqd 5274 |
. . . . . . 7
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ran ∅) |
6 | | rn0 5298 |
. . . . . . 7
⊢ ran
∅ = ∅ |
7 | 5, 6 | syl6eq 2660 |
. . . . . 6
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ∅) |
8 | 1, 7 | nsyl2 141 |
. . . . 5
⊢ (𝐹 ∈ ran 𝑆 → 𝑇 ∈ V) |
9 | | eqid 2610 |
. . . . . 6
⊢
(mCN‘𝑇) =
(mCN‘𝑇) |
10 | | mrsubvrs.v |
. . . . . 6
⊢ 𝑉 = (mVR‘𝑇) |
11 | | mrsubvrs.r |
. . . . . 6
⊢ 𝑅 = (mREx‘𝑇) |
12 | 9, 10, 11 | mrexval 30652 |
. . . . 5
⊢ (𝑇 ∈ V → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉)) |
13 | 8, 12 | syl 17 |
. . . 4
⊢ (𝐹 ∈ ran 𝑆 → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉)) |
14 | 13 | eleq2d 2673 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝑅 ↔ 𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉))) |
15 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑣 = ∅ → (𝐹‘𝑣) = (𝐹‘∅)) |
16 | 15 | rneqd 5274 |
. . . . . . . 8
⊢ (𝑣 = ∅ → ran (𝐹‘𝑣) = ran (𝐹‘∅)) |
17 | 16 | ineq1d 3775 |
. . . . . . 7
⊢ (𝑣 = ∅ → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘∅) ∩ 𝑉)) |
18 | | rneq 5272 |
. . . . . . . . . . . 12
⊢ (𝑣 = ∅ → ran 𝑣 = ran ∅) |
19 | 18, 6 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑣 = ∅ → ran 𝑣 = ∅) |
20 | 19 | ineq1d 3775 |
. . . . . . . . . 10
⊢ (𝑣 = ∅ → (ran 𝑣 ∩ 𝑉) = (∅ ∩ 𝑉)) |
21 | | 0in 3921 |
. . . . . . . . . 10
⊢ (∅
∩ 𝑉) =
∅ |
22 | 20, 21 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑣 = ∅ → (ran 𝑣 ∩ 𝑉) = ∅) |
23 | 22 | iuneq1d 4481 |
. . . . . . . 8
⊢ (𝑣 = ∅ → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∪
𝑥 ∈ ∅ (ran
(𝐹‘〈“𝑥”〉) ∩ 𝑉)) |
24 | | 0iun 4513 |
. . . . . . . 8
⊢ ∪ 𝑥 ∈ ∅ (ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∅ |
25 | 23, 24 | syl6eq 2660 |
. . . . . . 7
⊢ (𝑣 = ∅ → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∅) |
26 | 17, 25 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑣 = ∅ → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ↔ (ran (𝐹‘∅) ∩ 𝑉) = ∅)) |
27 | 26 | imbi2d 329 |
. . . . 5
⊢ (𝑣 = ∅ → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = ∅))) |
28 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑣 = 𝑦 → (𝐹‘𝑣) = (𝐹‘𝑦)) |
29 | 28 | rneqd 5274 |
. . . . . . . 8
⊢ (𝑣 = 𝑦 → ran (𝐹‘𝑣) = ran (𝐹‘𝑦)) |
30 | 29 | ineq1d 3775 |
. . . . . . 7
⊢ (𝑣 = 𝑦 → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘𝑦) ∩ 𝑉)) |
31 | | rneq 5272 |
. . . . . . . . 9
⊢ (𝑣 = 𝑦 → ran 𝑣 = ran 𝑦) |
32 | 31 | ineq1d 3775 |
. . . . . . . 8
⊢ (𝑣 = 𝑦 → (ran 𝑣 ∩ 𝑉) = (ran 𝑦 ∩ 𝑉)) |
33 | 32 | iuneq1d 4481 |
. . . . . . 7
⊢ (𝑣 = 𝑦 → ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) |
34 | 30, 33 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑣 = 𝑦 → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ↔ (ran (𝐹‘𝑦) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉))) |
35 | 34 | imbi2d 329 |
. . . . 5
⊢ (𝑣 = 𝑦 → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑦) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)))) |
36 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑣 = (𝑦 ++ 〈“𝑧”〉) → (𝐹‘𝑣) = (𝐹‘(𝑦 ++ 〈“𝑧”〉))) |
37 | 36 | rneqd 5274 |
. . . . . . . 8
⊢ (𝑣 = (𝑦 ++ 〈“𝑧”〉) → ran (𝐹‘𝑣) = ran (𝐹‘(𝑦 ++ 〈“𝑧”〉))) |
38 | 37 | ineq1d 3775 |
. . . . . . 7
⊢ (𝑣 = (𝑦 ++ 〈“𝑧”〉) → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉)) |
39 | | rneq 5272 |
. . . . . . . . 9
⊢ (𝑣 = (𝑦 ++ 〈“𝑧”〉) → ran 𝑣 = ran (𝑦 ++ 〈“𝑧”〉)) |
40 | 39 | ineq1d 3775 |
. . . . . . . 8
⊢ (𝑣 = (𝑦 ++ 〈“𝑧”〉) → (ran 𝑣 ∩ 𝑉) = (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)) |
41 | 40 | iuneq1d 4481 |
. . . . . . 7
⊢ (𝑣 = (𝑦 ++ 〈“𝑧”〉) → ∪ 𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∪
𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) |
42 | 38, 41 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑣 = (𝑦 ++ 〈“𝑧”〉) → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ↔ (ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉) = ∪
𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉))) |
43 | 42 | imbi2d 329 |
. . . . 5
⊢ (𝑣 = (𝑦 ++ 〈“𝑧”〉) → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉) = ∪
𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)))) |
44 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑣 = 𝑋 → (𝐹‘𝑣) = (𝐹‘𝑋)) |
45 | 44 | rneqd 5274 |
. . . . . . . 8
⊢ (𝑣 = 𝑋 → ran (𝐹‘𝑣) = ran (𝐹‘𝑋)) |
46 | 45 | ineq1d 3775 |
. . . . . . 7
⊢ (𝑣 = 𝑋 → (ran (𝐹‘𝑣) ∩ 𝑉) = (ran (𝐹‘𝑋) ∩ 𝑉)) |
47 | | rneq 5272 |
. . . . . . . . 9
⊢ (𝑣 = 𝑋 → ran 𝑣 = ran 𝑋) |
48 | 47 | ineq1d 3775 |
. . . . . . . 8
⊢ (𝑣 = 𝑋 → (ran 𝑣 ∩ 𝑉) = (ran 𝑋 ∩ 𝑉)) |
49 | 48 | iuneq1d 4481 |
. . . . . . 7
⊢ (𝑣 = 𝑋 → ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) |
50 | 46, 49 | eqeq12d 2625 |
. . . . . 6
⊢ (𝑣 = 𝑋 → ((ran (𝐹‘𝑣) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ↔ (ran (𝐹‘𝑋) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉))) |
51 | 50 | imbi2d 329 |
. . . . 5
⊢ (𝑣 = 𝑋 → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑣) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑣 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) ↔ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)))) |
52 | 2 | mrsub0 30667 |
. . . . . . . . 9
⊢ (𝐹 ∈ ran 𝑆 → (𝐹‘∅) = ∅) |
53 | 52 | rneqd 5274 |
. . . . . . . 8
⊢ (𝐹 ∈ ran 𝑆 → ran (𝐹‘∅) = ran
∅) |
54 | 53, 6 | syl6eq 2660 |
. . . . . . 7
⊢ (𝐹 ∈ ran 𝑆 → ran (𝐹‘∅) = ∅) |
55 | 54 | ineq1d 3775 |
. . . . . 6
⊢ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = (∅ ∩ 𝑉)) |
56 | 55, 21 | syl6eq 2660 |
. . . . 5
⊢ (𝐹 ∈ ran 𝑆 → (ran (𝐹‘∅) ∩ 𝑉) = ∅) |
57 | | uneq1 3722 |
. . . . . . . 8
⊢ ((ran
(𝐹‘𝑦) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) → ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉)) = (∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ∪ (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉))) |
58 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝐹 ∈ ran 𝑆) |
59 | | simprl 790 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉)) |
60 | 13 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑅 = Word ((mCN‘𝑇) ∪ 𝑉)) |
61 | 59, 60 | eleqtrrd 2691 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑦 ∈ 𝑅) |
62 | | simprr 792 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉)) |
63 | 62 | s1cld 13236 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 〈“𝑧”〉 ∈ Word ((mCN‘𝑇) ∪ 𝑉)) |
64 | 63, 60 | eleqtrrd 2691 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 〈“𝑧”〉 ∈ 𝑅) |
65 | 2, 11 | mrsubccat 30669 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑦 ∈ 𝑅 ∧ 〈“𝑧”〉 ∈ 𝑅) → (𝐹‘(𝑦 ++ 〈“𝑧”〉)) = ((𝐹‘𝑦) ++ (𝐹‘〈“𝑧”〉))) |
66 | 58, 61, 64, 65 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘(𝑦 ++ 〈“𝑧”〉)) = ((𝐹‘𝑦) ++ (𝐹‘〈“𝑧”〉))) |
67 | 66 | rneqd 5274 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) = ran ((𝐹‘𝑦) ++ (𝐹‘〈“𝑧”〉))) |
68 | 2, 11 | mrsubf 30668 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ ran 𝑆 → 𝐹:𝑅⟶𝑅) |
69 | 68 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → 𝐹:𝑅⟶𝑅) |
70 | 69, 61 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘𝑦) ∈ 𝑅) |
71 | 70, 60 | eleqtrd 2690 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘𝑦) ∈ Word ((mCN‘𝑇) ∪ 𝑉)) |
72 | 69, 64 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘〈“𝑧”〉) ∈ 𝑅) |
73 | 72, 60 | eleqtrd 2690 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (𝐹‘〈“𝑧”〉) ∈ Word ((mCN‘𝑇) ∪ 𝑉)) |
74 | | ccatrn 13225 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑦) ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ (𝐹‘〈“𝑧”〉) ∈ Word ((mCN‘𝑇) ∪ 𝑉)) → ran ((𝐹‘𝑦) ++ (𝐹‘〈“𝑧”〉)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘〈“𝑧”〉))) |
75 | 71, 73, 74 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran ((𝐹‘𝑦) ++ (𝐹‘〈“𝑧”〉)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘〈“𝑧”〉))) |
76 | 67, 75 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) = (ran (𝐹‘𝑦) ∪ ran (𝐹‘〈“𝑧”〉))) |
77 | 76 | ineq1d 3775 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∪ ran (𝐹‘〈“𝑧”〉)) ∩ 𝑉)) |
78 | | indir 3834 |
. . . . . . . . . 10
⊢ ((ran
(𝐹‘𝑦) ∪ ran (𝐹‘〈“𝑧”〉)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉)) |
79 | 77, 78 | syl6eq 2660 |
. . . . . . . . 9
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉) = ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉))) |
80 | | ccatrn 13225 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 〈“𝑧”〉 ∈ Word ((mCN‘𝑇) ∪ 𝑉)) → ran (𝑦 ++ 〈“𝑧”〉) = (ran 𝑦 ∪ ran 〈“𝑧”〉)) |
81 | 59, 63, 80 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝑦 ++ 〈“𝑧”〉) = (ran 𝑦 ∪ ran 〈“𝑧”〉)) |
82 | | s1rn 13232 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) → ran 〈“𝑧”〉 = {𝑧}) |
83 | 82 | ad2antll 761 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran 〈“𝑧”〉 = {𝑧}) |
84 | 83 | uneq2d 3729 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran 𝑦 ∪ ran 〈“𝑧”〉) = (ran 𝑦 ∪ {𝑧})) |
85 | 81, 84 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ran (𝑦 ++ 〈“𝑧”〉) = (ran 𝑦 ∪ {𝑧})) |
86 | 85 | ineq1d 3775 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉) = ((ran 𝑦 ∪ {𝑧}) ∩ 𝑉)) |
87 | | indir 3834 |
. . . . . . . . . . . . 13
⊢ ((ran
𝑦 ∪ {𝑧}) ∩ 𝑉) = ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉)) |
88 | 86, 87 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉) = ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))) |
89 | 88 | iuneq1d 4481 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∪
𝑥 ∈ ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) |
90 | | iunxun 4541 |
. . . . . . . . . . 11
⊢ ∪ 𝑥 ∈ ((ran 𝑦 ∩ 𝑉) ∪ ({𝑧} ∩ 𝑉))(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = (∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ∪ ∪
𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) |
91 | 89, 90 | syl6eq 2660 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = (∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ∪ ∪
𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉))) |
92 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → 𝑧 ∈ 𝑉) |
93 | 92 | snssd 4281 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → {𝑧} ⊆ 𝑉) |
94 | | df-ss 3554 |
. . . . . . . . . . . . . . 15
⊢ ({𝑧} ⊆ 𝑉 ↔ ({𝑧} ∩ 𝑉) = {𝑧}) |
95 | 93, 94 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ({𝑧} ∩ 𝑉) = {𝑧}) |
96 | 95 | iuneq1d 4481 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ∪
𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∪
𝑥 ∈ {𝑧} (ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) |
97 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
98 | | s1eq 13233 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → 〈“𝑥”〉 = 〈“𝑧”〉) |
99 | 98 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (𝐹‘〈“𝑥”〉) = (𝐹‘〈“𝑧”〉)) |
100 | 99 | rneqd 5274 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → ran (𝐹‘〈“𝑥”〉) = ran (𝐹‘〈“𝑧”〉)) |
101 | 100 | ineq1d 3775 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉)) |
102 | 97, 101 | iunxsn 4539 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑥 ∈ {𝑧} (ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉) |
103 | 96, 102 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ 𝑧 ∈ 𝑉) → ∪
𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉)) |
104 | | incom 3767 |
. . . . . . . . . . . . . . 15
⊢ ({𝑧} ∩ 𝑉) = (𝑉 ∩ {𝑧}) |
105 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ¬ 𝑧 ∈ 𝑉) |
106 | | disjsn 4192 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑉) |
107 | 105, 106 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (𝑉 ∩ {𝑧}) = ∅) |
108 | 104, 107 | syl5eq 2656 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ({𝑧} ∩ 𝑉) = ∅) |
109 | 108 | iuneq1d 4481 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ∪
𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = ∪
𝑥 ∈ ∅ (ran
(𝐹‘〈“𝑥”〉) ∩ 𝑉)) |
110 | 58 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝐹 ∈ ran 𝑆) |
111 | | eldif 3550 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉) ↔ (𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) ∧ ¬ 𝑧 ∈ 𝑉)) |
112 | 111 | biimpri 217 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉)) |
113 | 62, 112 | sylan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ (((mCN‘𝑇) ∪ 𝑉) ∖ 𝑉)) |
114 | | difun2 4000 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((mCN‘𝑇)
∪ 𝑉) ∖ 𝑉) = ((mCN‘𝑇) ∖ 𝑉) |
115 | 113, 114 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → 𝑧 ∈ ((mCN‘𝑇) ∖ 𝑉)) |
116 | 2, 11, 10, 9 | mrsubcn 30670 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑧 ∈ ((mCN‘𝑇) ∖ 𝑉)) → (𝐹‘〈“𝑧”〉) = 〈“𝑧”〉) |
117 | 110, 115,
116 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (𝐹‘〈“𝑧”〉) = 〈“𝑧”〉) |
118 | 117 | rneqd 5274 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran (𝐹‘〈“𝑧”〉) = ran 〈“𝑧”〉) |
119 | 83 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran 〈“𝑧”〉 = {𝑧}) |
120 | 118, 119 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ran (𝐹‘〈“𝑧”〉) = {𝑧}) |
121 | 120 | ineq1d 3775 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉) = ({𝑧} ∩ 𝑉)) |
122 | 121, 108 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉) = ∅) |
123 | 24, 109, 122 | 3eqtr4a 2670 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) ∧ ¬ 𝑧 ∈ 𝑉) → ∪
𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉)) |
124 | 103, 123 | pm2.61dan 828 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉)) |
125 | 124 | uneq2d 3729 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → (∪ 𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ∪ ∪
𝑥 ∈ ({𝑧} ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) = (∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ∪ (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉))) |
126 | 91, 125 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ∪ 𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) = (∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ∪ (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉))) |
127 | 79, 126 | eqeq12d 2625 |
. . . . . . . 8
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ((ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉) = ∪
𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ↔ ((ran (𝐹‘𝑦) ∩ 𝑉) ∪ (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉)) = (∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) ∪ (ran (𝐹‘〈“𝑧”〉) ∩ 𝑉)))) |
128 | 57, 127 | syl5ibr 235 |
. . . . . . 7
⊢ ((𝐹 ∈ ran 𝑆 ∧ (𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉))) → ((ran (𝐹‘𝑦) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) → (ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉) = ∪
𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉))) |
129 | 128 | expcom 450 |
. . . . . 6
⊢ ((𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉)) → (𝐹 ∈ ran 𝑆 → ((ran (𝐹‘𝑦) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉) → (ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉) = ∪
𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)))) |
130 | 129 | a2d 29 |
. . . . 5
⊢ ((𝑦 ∈ Word ((mCN‘𝑇) ∪ 𝑉) ∧ 𝑧 ∈ ((mCN‘𝑇) ∪ 𝑉)) → ((𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑦) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑦 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) → (𝐹 ∈ ran 𝑆 → (ran (𝐹‘(𝑦 ++ 〈“𝑧”〉)) ∩ 𝑉) = ∪
𝑥 ∈ (ran (𝑦 ++ 〈“𝑧”〉) ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)))) |
131 | 27, 35, 43, 51, 56, 130 | wrdind 13328 |
. . . 4
⊢ (𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉) → (𝐹 ∈ ran 𝑆 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉))) |
132 | 131 | com12 32 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ Word ((mCN‘𝑇) ∪ 𝑉) → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉))) |
133 | 14, 132 | sylbid 229 |
. 2
⊢ (𝐹 ∈ ran 𝑆 → (𝑋 ∈ 𝑅 → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉))) |
134 | 133 | imp 444 |
1
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝑋 ∈ 𝑅) → (ran (𝐹‘𝑋) ∩ 𝑉) = ∪
𝑥 ∈ (ran 𝑋 ∩ 𝑉)(ran (𝐹‘〈“𝑥”〉) ∩ 𝑉)) |