Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . 4
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
2 | | efgval.r |
. . . 4
⊢ ∼ = (
~FG ‘𝐼) |
3 | | efgval2.m |
. . . 4
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
4 | | efgval2.t |
. . . 4
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
5 | | efgred.d |
. . . 4
⊢ 𝐷 = (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) |
6 | | efgred.s |
. . . 4
⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) |
7 | 1, 2, 3, 4, 5, 6 | efgsf 18142 |
. . 3
⊢ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊 |
8 | 7 | fdmi 6052 |
. . . 4
⊢ dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} |
9 | 8 | feq2i 6037 |
. . 3
⊢ (𝑆:dom 𝑆⟶𝑊 ↔ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊) |
10 | 7, 9 | mpbir 221 |
. 2
⊢ 𝑆:dom 𝑆⟶𝑊 |
11 | | frn 6053 |
. . . 4
⊢ (𝑆:dom 𝑆⟶𝑊 → ran 𝑆 ⊆ 𝑊) |
12 | 10, 11 | ax-mp 5 |
. . 3
⊢ ran 𝑆 ⊆ 𝑊 |
13 | | fviss 6256 |
. . . . . . . . 9
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ⊆ Word (𝐼 ×
2𝑜) |
14 | 1, 13 | eqsstri 3635 |
. . . . . . . 8
⊢ 𝑊 ⊆ Word (𝐼 ×
2𝑜) |
15 | 14 | sseli 3599 |
. . . . . . 7
⊢ (𝑐 ∈ 𝑊 → 𝑐 ∈ Word (𝐼 ×
2𝑜)) |
16 | | lencl 13324 |
. . . . . . 7
⊢ (𝑐 ∈ Word (𝐼 × 2𝑜) →
(#‘𝑐) ∈
ℕ0) |
17 | 15, 16 | syl 17 |
. . . . . 6
⊢ (𝑐 ∈ 𝑊 → (#‘𝑐) ∈
ℕ0) |
18 | | peano2nn0 11333 |
. . . . . 6
⊢
((#‘𝑐) ∈
ℕ0 → ((#‘𝑐) + 1) ∈
ℕ0) |
19 | 14 | sseli 3599 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝑊 → 𝑎 ∈ Word (𝐼 ×
2𝑜)) |
20 | | lencl 13324 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ Word (𝐼 × 2𝑜) →
(#‘𝑎) ∈
ℕ0) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ 𝑊 → (#‘𝑎) ∈
ℕ0) |
22 | | nn0nlt0 11319 |
. . . . . . . . . . . 12
⊢
((#‘𝑎) ∈
ℕ0 → ¬ (#‘𝑎) < 0) |
23 | | breq2 4657 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 0 → ((#‘𝑎) < 𝑏 ↔ (#‘𝑎) < 0)) |
24 | 23 | notbid 308 |
. . . . . . . . . . . 12
⊢ (𝑏 = 0 → (¬
(#‘𝑎) < 𝑏 ↔ ¬ (#‘𝑎) < 0)) |
25 | 22, 24 | syl5ibr 236 |
. . . . . . . . . . 11
⊢ (𝑏 = 0 → ((#‘𝑎) ∈ ℕ0
→ ¬ (#‘𝑎)
< 𝑏)) |
26 | 21, 25 | syl5 34 |
. . . . . . . . . 10
⊢ (𝑏 = 0 → (𝑎 ∈ 𝑊 → ¬ (#‘𝑎) < 𝑏)) |
27 | 26 | ralrimiv 2965 |
. . . . . . . . 9
⊢ (𝑏 = 0 → ∀𝑎 ∈ 𝑊 ¬ (#‘𝑎) < 𝑏) |
28 | | rabeq0 3957 |
. . . . . . . . 9
⊢ ({𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑏} = ∅ ↔ ∀𝑎 ∈ 𝑊 ¬ (#‘𝑎) < 𝑏) |
29 | 27, 28 | sylibr 224 |
. . . . . . . 8
⊢ (𝑏 = 0 → {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑏} = ∅) |
30 | 29 | sseq1d 3632 |
. . . . . . 7
⊢ (𝑏 = 0 → ({𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑏} ⊆ ran 𝑆 ↔ ∅ ⊆ ran 𝑆)) |
31 | | breq2 4657 |
. . . . . . . . 9
⊢ (𝑏 = 𝑑 → ((#‘𝑎) < 𝑏 ↔ (#‘𝑎) < 𝑑)) |
32 | 31 | rabbidv 3189 |
. . . . . . . 8
⊢ (𝑏 = 𝑑 → {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑏} = {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑}) |
33 | 32 | sseq1d 3632 |
. . . . . . 7
⊢ (𝑏 = 𝑑 → ({𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑏} ⊆ ran 𝑆 ↔ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆)) |
34 | | breq2 4657 |
. . . . . . . . 9
⊢ (𝑏 = (𝑑 + 1) → ((#‘𝑎) < 𝑏 ↔ (#‘𝑎) < (𝑑 + 1))) |
35 | 34 | rabbidv 3189 |
. . . . . . . 8
⊢ (𝑏 = (𝑑 + 1) → {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑏} = {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < (𝑑 + 1)}) |
36 | 35 | sseq1d 3632 |
. . . . . . 7
⊢ (𝑏 = (𝑑 + 1) → ({𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑏} ⊆ ran 𝑆 ↔ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < (𝑑 + 1)} ⊆ ran 𝑆)) |
37 | | breq2 4657 |
. . . . . . . . 9
⊢ (𝑏 = ((#‘𝑐) + 1) → ((#‘𝑎) < 𝑏 ↔ (#‘𝑎) < ((#‘𝑐) + 1))) |
38 | 37 | rabbidv 3189 |
. . . . . . . 8
⊢ (𝑏 = ((#‘𝑐) + 1) → {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑏} = {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < ((#‘𝑐) + 1)}) |
39 | 38 | sseq1d 3632 |
. . . . . . 7
⊢ (𝑏 = ((#‘𝑐) + 1) → ({𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑏} ⊆ ran 𝑆 ↔ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < ((#‘𝑐) + 1)} ⊆ ran 𝑆)) |
40 | | 0ss 3972 |
. . . . . . 7
⊢ ∅
⊆ ran 𝑆 |
41 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) → {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) |
42 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑐 → (#‘𝑎) = (#‘𝑐)) |
43 | 42 | eqeq1d 2624 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑐 → ((#‘𝑎) = 𝑑 ↔ (#‘𝑐) = 𝑑)) |
44 | 43 | cbvrabv 3199 |
. . . . . . . . . . 11
⊢ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) = 𝑑} = {𝑐 ∈ 𝑊 ∣ (#‘𝑐) = 𝑑} |
45 | | eliun 4524 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥) ↔ ∃𝑥 ∈ 𝑊 𝑐 ∈ ran (𝑇‘𝑥)) |
46 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑏 → (𝑇‘𝑥) = (𝑇‘𝑏)) |
47 | 46 | rneqd 5353 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑏 → ran (𝑇‘𝑥) = ran (𝑇‘𝑏)) |
48 | 47 | eleq2d 2687 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑏 → (𝑐 ∈ ran (𝑇‘𝑥) ↔ 𝑐 ∈ ran (𝑇‘𝑏))) |
49 | 48 | cbvrexv 3172 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥 ∈
𝑊 𝑐 ∈ ran (𝑇‘𝑥) ↔ ∃𝑏 ∈ 𝑊 𝑐 ∈ ran (𝑇‘𝑏)) |
50 | 45, 49 | bitri 264 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥) ↔ ∃𝑏 ∈ 𝑊 𝑐 ∈ ran (𝑇‘𝑏)) |
51 | | simpl1r 1113 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏))) → {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) |
52 | | simprl 794 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏))) → 𝑏 ∈ 𝑊) |
53 | 14, 52 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏))) → 𝑏 ∈ Word (𝐼 ×
2𝑜)) |
54 | | lencl 13324 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 ∈ Word (𝐼 × 2𝑜) →
(#‘𝑏) ∈
ℕ0) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏))) → (#‘𝑏) ∈
ℕ0) |
56 | 55 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏))) → (#‘𝑏) ∈ ℝ) |
57 | | 2rp 11837 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℝ+ |
58 | | ltaddrp 11867 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#‘𝑏) ∈
ℝ ∧ 2 ∈ ℝ+) → (#‘𝑏) < ((#‘𝑏) + 2)) |
59 | 56, 57, 58 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏))) → (#‘𝑏) < ((#‘𝑏) + 2)) |
60 | 1, 2, 3, 4 | efgtlen 18139 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏)) → (#‘𝑐) = ((#‘𝑏) + 2)) |
61 | 60 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏))) → (#‘𝑐) = ((#‘𝑏) + 2)) |
62 | | simpl3 1066 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏))) → (#‘𝑐) = 𝑑) |
63 | 61, 62 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏))) → ((#‘𝑏) + 2) = 𝑑) |
64 | 59, 63 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏))) → (#‘𝑏) < 𝑑) |
65 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = 𝑏 → (#‘𝑎) = (#‘𝑏)) |
66 | 65 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝑏 → ((#‘𝑎) < 𝑑 ↔ (#‘𝑏) < 𝑑)) |
67 | 66 | elrab 3363 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ↔ (𝑏 ∈ 𝑊 ∧ (#‘𝑏) < 𝑑)) |
68 | 52, 64, 67 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏))) → 𝑏 ∈ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑}) |
69 | 51, 68 | sseldd 3604 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏))) → 𝑏 ∈ ran 𝑆) |
70 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆:dom 𝑆⟶𝑊 → 𝑆 Fn dom 𝑆) |
71 | 10, 70 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑆 Fn dom 𝑆 |
72 | | fvelrnb 6243 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 Fn dom 𝑆 → (𝑏 ∈ ran 𝑆 ↔ ∃𝑜 ∈ dom 𝑆(𝑆‘𝑜) = 𝑏)) |
73 | 71, 72 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ ran 𝑆 ↔ ∃𝑜 ∈ dom 𝑆(𝑆‘𝑜) = 𝑏) |
74 | 69, 73 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏))) → ∃𝑜 ∈ dom 𝑆(𝑆‘𝑜) = 𝑏) |
75 | | simprrl 804 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆‘𝑜) = 𝑏))) → 𝑜 ∈ dom 𝑆) |
76 | 1, 2, 3, 4, 5, 6 | efgsdm 18143 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑜 ∈ dom 𝑆 ↔ (𝑜 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝑜‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝑜))(𝑜‘𝑖) ∈ ran (𝑇‘(𝑜‘(𝑖 − 1))))) |
77 | 76 | simp1bi 1076 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑜 ∈ dom 𝑆 → 𝑜 ∈ (Word 𝑊 ∖ {∅})) |
78 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑜 ∈ (Word 𝑊 ∖ {∅}) → 𝑜 ∈ Word 𝑊) |
79 | 75, 77, 78 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆‘𝑜) = 𝑏))) → 𝑜 ∈ Word 𝑊) |
80 | | simpl2 1065 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆‘𝑜) = 𝑏))) → 𝑐 ∈ 𝑊) |
81 | | simprlr 803 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆‘𝑜) = 𝑏))) → 𝑐 ∈ ran (𝑇‘𝑏)) |
82 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆‘𝑜) = 𝑏))) → (𝑆‘𝑜) = 𝑏) |
83 | 82 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆‘𝑜) = 𝑏))) → (𝑇‘(𝑆‘𝑜)) = (𝑇‘𝑏)) |
84 | 83 | rneqd 5353 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆‘𝑜) = 𝑏))) → ran (𝑇‘(𝑆‘𝑜)) = ran (𝑇‘𝑏)) |
85 | 81, 84 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆‘𝑜) = 𝑏))) → 𝑐 ∈ ran (𝑇‘(𝑆‘𝑜))) |
86 | 1, 2, 3, 4, 5, 6 | efgsp1 18150 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑜 ∈ dom 𝑆 ∧ 𝑐 ∈ ran (𝑇‘(𝑆‘𝑜))) → (𝑜 ++ 〈“𝑐”〉) ∈ dom 𝑆) |
87 | 75, 85, 86 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆‘𝑜) = 𝑏))) → (𝑜 ++ 〈“𝑐”〉) ∈ dom 𝑆) |
88 | 1, 2, 3, 4, 5, 6 | efgsval2 18146 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑜 ∈ Word 𝑊 ∧ 𝑐 ∈ 𝑊 ∧ (𝑜 ++ 〈“𝑐”〉) ∈ dom 𝑆) → (𝑆‘(𝑜 ++ 〈“𝑐”〉)) = 𝑐) |
89 | 79, 80, 87, 88 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆‘𝑜) = 𝑏))) → (𝑆‘(𝑜 ++ 〈“𝑐”〉)) = 𝑐) |
90 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 Fn dom 𝑆 ∧ (𝑜 ++ 〈“𝑐”〉) ∈ dom 𝑆) → (𝑆‘(𝑜 ++ 〈“𝑐”〉)) ∈ ran 𝑆) |
91 | 71, 87, 90 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆‘𝑜) = 𝑏))) → (𝑆‘(𝑜 ++ 〈“𝑐”〉)) ∈ ran 𝑆) |
92 | 89, 91 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ ((𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏)) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆‘𝑜) = 𝑏))) → 𝑐 ∈ ran 𝑆) |
93 | 92 | anassrs 680 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑑 ∈
ℕ0 ∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏))) ∧ (𝑜 ∈ dom 𝑆 ∧ (𝑆‘𝑜) = 𝑏)) → 𝑐 ∈ ran 𝑆) |
94 | 74, 93 | rexlimddv 3035 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) ∧ (𝑏 ∈ 𝑊 ∧ 𝑐 ∈ ran (𝑇‘𝑏))) → 𝑐 ∈ ran 𝑆) |
95 | 94 | rexlimdvaa 3032 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) → (∃𝑏 ∈ 𝑊 𝑐 ∈ ran (𝑇‘𝑏) → 𝑐 ∈ ran 𝑆)) |
96 | 50, 95 | syl5bi 232 |
. . . . . . . . . . . . 13
⊢ (((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) → (𝑐 ∈ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥) → 𝑐 ∈ ran 𝑆)) |
97 | | eldif 3584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 ∈ (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) ↔ (𝑐 ∈ 𝑊 ∧ ¬ 𝑐 ∈ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥))) |
98 | 5 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 ∈ 𝐷 ↔ 𝑐 ∈ (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥))) |
99 | 1, 2, 3, 4, 5, 6 | efgs1 18148 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 ∈ 𝐷 → 〈“𝑐”〉 ∈ dom 𝑆) |
100 | 98, 99 | sylbir 225 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 ∈ (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) → 〈“𝑐”〉 ∈ dom 𝑆) |
101 | 97, 100 | sylbir 225 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 ∈ 𝑊 ∧ ¬ 𝑐 ∈ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) → 〈“𝑐”〉 ∈ dom 𝑆) |
102 | 1, 2, 3, 4, 5, 6 | efgsval 18144 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈“𝑐”〉 ∈ dom 𝑆 → (𝑆‘〈“𝑐”〉) = (〈“𝑐”〉‘((#‘〈“𝑐”〉) −
1))) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 ∈ 𝑊 ∧ ¬ 𝑐 ∈ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) → (𝑆‘〈“𝑐”〉) = (〈“𝑐”〉‘((#‘〈“𝑐”〉) −
1))) |
104 | | s1len 13385 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(#‘〈“𝑐”〉) = 1 |
105 | 104 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘〈“𝑐”〉) − 1) = (1 −
1) |
106 | | 1m1e0 11089 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1
− 1) = 0 |
107 | 105, 106 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘〈“𝑐”〉) − 1) =
0 |
108 | 107 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈“𝑐”〉‘((#‘〈“𝑐”〉) − 1)) =
(〈“𝑐”〉‘0) |
109 | 108 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 ∈ 𝑊 ∧ ¬ 𝑐 ∈ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) → (〈“𝑐”〉‘((#‘〈“𝑐”〉) − 1)) =
(〈“𝑐”〉‘0)) |
110 | | s1fv 13390 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 ∈ 𝑊 → (〈“𝑐”〉‘0) = 𝑐) |
111 | 110 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 ∈ 𝑊 ∧ ¬ 𝑐 ∈ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) → (〈“𝑐”〉‘0) = 𝑐) |
112 | 103, 109,
111 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ∈ 𝑊 ∧ ¬ 𝑐 ∈ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) → (𝑆‘〈“𝑐”〉) = 𝑐) |
113 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 Fn dom 𝑆 ∧ 〈“𝑐”〉 ∈ dom 𝑆) → (𝑆‘〈“𝑐”〉) ∈ ran 𝑆) |
114 | 71, 101, 113 | sylancr 695 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ∈ 𝑊 ∧ ¬ 𝑐 ∈ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) → (𝑆‘〈“𝑐”〉) ∈ ran 𝑆) |
115 | 112, 114 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 ∈ 𝑊 ∧ ¬ 𝑐 ∈ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) → 𝑐 ∈ ran 𝑆) |
116 | 115 | ex 450 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ 𝑊 → (¬ 𝑐 ∈ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥) → 𝑐 ∈ ran 𝑆)) |
117 | 116 | 3ad2ant2 1083 |
. . . . . . . . . . . . 13
⊢ (((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) → (¬ 𝑐 ∈ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥) → 𝑐 ∈ ran 𝑆)) |
118 | 96, 117 | pm2.61d 170 |
. . . . . . . . . . . 12
⊢ (((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) ∧ 𝑐 ∈ 𝑊 ∧ (#‘𝑐) = 𝑑) → 𝑐 ∈ ran 𝑆) |
119 | 118 | rabssdv 3682 |
. . . . . . . . . . 11
⊢ ((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) → {𝑐 ∈ 𝑊 ∣ (#‘𝑐) = 𝑑} ⊆ ran 𝑆) |
120 | 44, 119 | syl5eqss 3649 |
. . . . . . . . . 10
⊢ ((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) → {𝑎 ∈ 𝑊 ∣ (#‘𝑎) = 𝑑} ⊆ ran 𝑆) |
121 | 41, 120 | unssd 3789 |
. . . . . . . . 9
⊢ ((𝑑 ∈ ℕ0
∧ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆) → ({𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ∪ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) = 𝑑}) ⊆ ran 𝑆) |
122 | 121 | ex 450 |
. . . . . . . 8
⊢ (𝑑 ∈ ℕ0
→ ({𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆 → ({𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ∪ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) = 𝑑}) ⊆ ran 𝑆)) |
123 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈ ℕ0
→ 𝑑 ∈
ℕ0) |
124 | | nn0leltp1 11436 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑎) ∈
ℕ0 ∧ 𝑑
∈ ℕ0) → ((#‘𝑎) ≤ 𝑑 ↔ (#‘𝑎) < (𝑑 + 1))) |
125 | 21, 123, 124 | syl2anr 495 |
. . . . . . . . . . . 12
⊢ ((𝑑 ∈ ℕ0
∧ 𝑎 ∈ 𝑊) → ((#‘𝑎) ≤ 𝑑 ↔ (#‘𝑎) < (𝑑 + 1))) |
126 | 21 | nn0red 11352 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝑊 → (#‘𝑎) ∈ ℝ) |
127 | | nn0re 11301 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈ ℕ0
→ 𝑑 ∈
ℝ) |
128 | | leloe 10124 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑎) ∈
ℝ ∧ 𝑑 ∈
ℝ) → ((#‘𝑎) ≤ 𝑑 ↔ ((#‘𝑎) < 𝑑 ∨ (#‘𝑎) = 𝑑))) |
129 | 126, 127,
128 | syl2anr 495 |
. . . . . . . . . . . 12
⊢ ((𝑑 ∈ ℕ0
∧ 𝑎 ∈ 𝑊) → ((#‘𝑎) ≤ 𝑑 ↔ ((#‘𝑎) < 𝑑 ∨ (#‘𝑎) = 𝑑))) |
130 | 125, 129 | bitr3d 270 |
. . . . . . . . . . 11
⊢ ((𝑑 ∈ ℕ0
∧ 𝑎 ∈ 𝑊) → ((#‘𝑎) < (𝑑 + 1) ↔ ((#‘𝑎) < 𝑑 ∨ (#‘𝑎) = 𝑑))) |
131 | 130 | rabbidva 3188 |
. . . . . . . . . 10
⊢ (𝑑 ∈ ℕ0
→ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < (𝑑 + 1)} = {𝑎 ∈ 𝑊 ∣ ((#‘𝑎) < 𝑑 ∨ (#‘𝑎) = 𝑑)}) |
132 | | unrab 3898 |
. . . . . . . . . 10
⊢ ({𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ∪ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) = 𝑑}) = {𝑎 ∈ 𝑊 ∣ ((#‘𝑎) < 𝑑 ∨ (#‘𝑎) = 𝑑)} |
133 | 131, 132 | syl6eqr 2674 |
. . . . . . . . 9
⊢ (𝑑 ∈ ℕ0
→ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < (𝑑 + 1)} = ({𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ∪ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) = 𝑑})) |
134 | 133 | sseq1d 3632 |
. . . . . . . 8
⊢ (𝑑 ∈ ℕ0
→ ({𝑎 ∈ 𝑊 ∣ (#‘𝑎) < (𝑑 + 1)} ⊆ ran 𝑆 ↔ ({𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ∪ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) = 𝑑}) ⊆ ran 𝑆)) |
135 | 122, 134 | sylibrd 249 |
. . . . . . 7
⊢ (𝑑 ∈ ℕ0
→ ({𝑎 ∈ 𝑊 ∣ (#‘𝑎) < 𝑑} ⊆ ran 𝑆 → {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < (𝑑 + 1)} ⊆ ran 𝑆)) |
136 | 30, 33, 36, 39, 40, 135 | nn0ind 11472 |
. . . . . 6
⊢
(((#‘𝑐) + 1)
∈ ℕ0 → {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < ((#‘𝑐) + 1)} ⊆ ran 𝑆) |
137 | 17, 18, 136 | 3syl 18 |
. . . . 5
⊢ (𝑐 ∈ 𝑊 → {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < ((#‘𝑐) + 1)} ⊆ ran 𝑆) |
138 | | id 22 |
. . . . . 6
⊢ (𝑐 ∈ 𝑊 → 𝑐 ∈ 𝑊) |
139 | 17 | nn0red 11352 |
. . . . . . 7
⊢ (𝑐 ∈ 𝑊 → (#‘𝑐) ∈ ℝ) |
140 | 139 | ltp1d 10954 |
. . . . . 6
⊢ (𝑐 ∈ 𝑊 → (#‘𝑐) < ((#‘𝑐) + 1)) |
141 | 42 | breq1d 4663 |
. . . . . . 7
⊢ (𝑎 = 𝑐 → ((#‘𝑎) < ((#‘𝑐) + 1) ↔ (#‘𝑐) < ((#‘𝑐) + 1))) |
142 | 141 | elrab 3363 |
. . . . . 6
⊢ (𝑐 ∈ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < ((#‘𝑐) + 1)} ↔ (𝑐 ∈ 𝑊 ∧ (#‘𝑐) < ((#‘𝑐) + 1))) |
143 | 138, 140,
142 | sylanbrc 698 |
. . . . 5
⊢ (𝑐 ∈ 𝑊 → 𝑐 ∈ {𝑎 ∈ 𝑊 ∣ (#‘𝑎) < ((#‘𝑐) + 1)}) |
144 | 137, 143 | sseldd 3604 |
. . . 4
⊢ (𝑐 ∈ 𝑊 → 𝑐 ∈ ran 𝑆) |
145 | 144 | ssriv 3607 |
. . 3
⊢ 𝑊 ⊆ ran 𝑆 |
146 | 12, 145 | eqssi 3619 |
. 2
⊢ ran 𝑆 = 𝑊 |
147 | | dffo2 6119 |
. 2
⊢ (𝑆:dom 𝑆–onto→𝑊 ↔ (𝑆:dom 𝑆⟶𝑊 ∧ ran 𝑆 = 𝑊)) |
148 | 10, 146, 147 | mpbir2an 955 |
1
⊢ 𝑆:dom 𝑆–onto→𝑊 |