Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . . . . . 8
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
2 | | fviss 6256 |
. . . . . . . 8
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ⊆ Word (𝐼 ×
2𝑜) |
3 | 1, 2 | eqsstri 3635 |
. . . . . . 7
⊢ 𝑊 ⊆ Word (𝐼 ×
2𝑜) |
4 | | efgval.r |
. . . . . . . . . . 11
⊢ ∼ = (
~FG ‘𝐼) |
5 | | efgval2.m |
. . . . . . . . . . 11
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
6 | | efgval2.t |
. . . . . . . . . . 11
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
7 | | efgred.d |
. . . . . . . . . . 11
⊢ 𝐷 = (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) |
8 | | efgred.s |
. . . . . . . . . . 11
⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) |
9 | 1, 4, 5, 6, 7, 8 | efgsf 18142 |
. . . . . . . . . 10
⊢ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊 |
10 | 9 | fdmi 6052 |
. . . . . . . . . . 11
⊢ dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} |
11 | 10 | feq2i 6037 |
. . . . . . . . . 10
⊢ (𝑆:dom 𝑆⟶𝑊 ↔ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊) |
12 | 9, 11 | mpbir 221 |
. . . . . . . . 9
⊢ 𝑆:dom 𝑆⟶𝑊 |
13 | 12 | ffvelrni 6358 |
. . . . . . . 8
⊢ (𝐴 ∈ dom 𝑆 → (𝑆‘𝐴) ∈ 𝑊) |
14 | 13 | adantr 481 |
. . . . . . 7
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → (𝑆‘𝐴) ∈ 𝑊) |
15 | 3, 14 | sseldi 3601 |
. . . . . 6
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → (𝑆‘𝐴) ∈ Word (𝐼 ×
2𝑜)) |
16 | | lencl 13324 |
. . . . . 6
⊢ ((𝑆‘𝐴) ∈ Word (𝐼 × 2𝑜) →
(#‘(𝑆‘𝐴)) ∈
ℕ0) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → (#‘(𝑆‘𝐴)) ∈
ℕ0) |
18 | | peano2nn0 11333 |
. . . . 5
⊢
((#‘(𝑆‘𝐴)) ∈ ℕ0 →
((#‘(𝑆‘𝐴)) + 1) ∈
ℕ0) |
19 | 17, 18 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → ((#‘(𝑆‘𝐴)) + 1) ∈
ℕ0) |
20 | | breq2 4657 |
. . . . . . 7
⊢ (𝑐 = 0 → ((#‘(𝑆‘𝑎)) < 𝑐 ↔ (#‘(𝑆‘𝑎)) < 0)) |
21 | 20 | imbi1d 331 |
. . . . . 6
⊢ (𝑐 = 0 → (((#‘(𝑆‘𝑎)) < 𝑐 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((#‘(𝑆‘𝑎)) < 0 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
22 | 21 | 2ralbidv 2989 |
. . . . 5
⊢ (𝑐 = 0 → (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑐 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 0 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
23 | | breq2 4657 |
. . . . . . 7
⊢ (𝑐 = 𝑖 → ((#‘(𝑆‘𝑎)) < 𝑐 ↔ (#‘(𝑆‘𝑎)) < 𝑖)) |
24 | 23 | imbi1d 331 |
. . . . . 6
⊢ (𝑐 = 𝑖 → (((#‘(𝑆‘𝑎)) < 𝑐 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
25 | 24 | 2ralbidv 2989 |
. . . . 5
⊢ (𝑐 = 𝑖 → (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑐 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
26 | | breq2 4657 |
. . . . . . 7
⊢ (𝑐 = (𝑖 + 1) → ((#‘(𝑆‘𝑎)) < 𝑐 ↔ (#‘(𝑆‘𝑎)) < (𝑖 + 1))) |
27 | 26 | imbi1d 331 |
. . . . . 6
⊢ (𝑐 = (𝑖 + 1) → (((#‘(𝑆‘𝑎)) < 𝑐 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((#‘(𝑆‘𝑎)) < (𝑖 + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
28 | 27 | 2ralbidv 2989 |
. . . . 5
⊢ (𝑐 = (𝑖 + 1) → (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑐 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (𝑖 + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
29 | | breq2 4657 |
. . . . . . 7
⊢ (𝑐 = ((#‘(𝑆‘𝐴)) + 1) → ((#‘(𝑆‘𝑎)) < 𝑐 ↔ (#‘(𝑆‘𝑎)) < ((#‘(𝑆‘𝐴)) + 1))) |
30 | 29 | imbi1d 331 |
. . . . . 6
⊢ (𝑐 = ((#‘(𝑆‘𝐴)) + 1) → (((#‘(𝑆‘𝑎)) < 𝑐 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((#‘(𝑆‘𝑎)) < ((#‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
31 | 30 | 2ralbidv 2989 |
. . . . 5
⊢ (𝑐 = ((#‘(𝑆‘𝐴)) + 1) → (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑐 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < ((#‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
32 | 12 | ffvelrni 6358 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ dom 𝑆 → (𝑆‘𝑎) ∈ 𝑊) |
33 | 3, 32 | sseldi 3601 |
. . . . . . . . . 10
⊢ (𝑎 ∈ dom 𝑆 → (𝑆‘𝑎) ∈ Word (𝐼 ×
2𝑜)) |
34 | | lencl 13324 |
. . . . . . . . . 10
⊢ ((𝑆‘𝑎) ∈ Word (𝐼 × 2𝑜) →
(#‘(𝑆‘𝑎)) ∈
ℕ0) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ (𝑎 ∈ dom 𝑆 → (#‘(𝑆‘𝑎)) ∈
ℕ0) |
36 | | nn0nlt0 11319 |
. . . . . . . . 9
⊢
((#‘(𝑆‘𝑎)) ∈ ℕ0 → ¬
(#‘(𝑆‘𝑎)) < 0) |
37 | 35, 36 | syl 17 |
. . . . . . . 8
⊢ (𝑎 ∈ dom 𝑆 → ¬ (#‘(𝑆‘𝑎)) < 0) |
38 | 37 | pm2.21d 118 |
. . . . . . 7
⊢ (𝑎 ∈ dom 𝑆 → ((#‘(𝑆‘𝑎)) < 0 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
39 | 38 | adantr 481 |
. . . . . 6
⊢ ((𝑎 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆) → ((#‘(𝑆‘𝑎)) < 0 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
40 | 39 | rgen2a 2977 |
. . . . 5
⊢
∀𝑎 ∈ dom
𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 0 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) |
41 | | simpl1 1064 |
. . . . . . . . . . . . . 14
⊢
(((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((#‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0)) → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
42 | | simpl3l 1116 |
. . . . . . . . . . . . . . 15
⊢
(((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((#‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0)) → (#‘(𝑆‘𝑐)) = 𝑖) |
43 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘(𝑆‘𝑐)) = 𝑖 → ((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝑐)) ↔ (#‘(𝑆‘𝑎)) < 𝑖)) |
44 | 43 | imbi1d 331 |
. . . . . . . . . . . . . . . 16
⊢
((#‘(𝑆‘𝑐)) = 𝑖 → (((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝑐)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
45 | 44 | 2ralbidv 2989 |
. . . . . . . . . . . . . . 15
⊢
((#‘(𝑆‘𝑐)) = 𝑖 → (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝑐)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
46 | 42, 45 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((#‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0)) → (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝑐)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
47 | 41, 46 | mpbird 247 |
. . . . . . . . . . . . 13
⊢
(((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((#‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0)) → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (#‘(𝑆‘𝑐)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
48 | | simpl2l 1114 |
. . . . . . . . . . . . 13
⊢
(((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((#‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0)) → 𝑐 ∈ dom 𝑆) |
49 | | simpl2r 1115 |
. . . . . . . . . . . . 13
⊢
(((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((#‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0)) → 𝑑 ∈ dom 𝑆) |
50 | | simpl3r 1117 |
. . . . . . . . . . . . 13
⊢
(((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((#‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0)) → (𝑆‘𝑐) = (𝑆‘𝑑)) |
51 | | simpr 477 |
. . . . . . . . . . . . 13
⊢
(((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((#‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0)) → ¬ (𝑐‘0) = (𝑑‘0)) |
52 | 1, 4, 5, 6, 7, 8, 47, 48, 49, 50, 51 | efgredlem 18160 |
. . . . . . . . . . . 12
⊢ ¬
((∀𝑎 ∈ dom
𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((#‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0)) |
53 | | iman 440 |
. . . . . . . . . . . 12
⊢
(((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((#‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) → (𝑐‘0) = (𝑑‘0)) ↔ ¬ ((∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((#‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0))) |
54 | 52, 53 | mpbir 221 |
. . . . . . . . . . 11
⊢
((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((#‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) → (𝑐‘0) = (𝑑‘0)) |
55 | 54 | 3expia 1267 |
. . . . . . . . . 10
⊢
((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆)) → (((#‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑)) → (𝑐‘0) = (𝑑‘0))) |
56 | 55 | expd 452 |
. . . . . . . . 9
⊢
((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆)) → ((#‘(𝑆‘𝑐)) = 𝑖 → ((𝑆‘𝑐) = (𝑆‘𝑑) → (𝑐‘0) = (𝑑‘0)))) |
57 | 56 | ralrimivva 2971 |
. . . . . . . 8
⊢
(∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) → ∀𝑐 ∈ dom 𝑆∀𝑑 ∈ dom 𝑆((#‘(𝑆‘𝑐)) = 𝑖 → ((𝑆‘𝑐) = (𝑆‘𝑑) → (𝑐‘0) = (𝑑‘0)))) |
58 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑎 → (𝑆‘𝑐) = (𝑆‘𝑎)) |
59 | 58 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑎 → (#‘(𝑆‘𝑐)) = (#‘(𝑆‘𝑎))) |
60 | 59 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑎 → ((#‘(𝑆‘𝑐)) = 𝑖 ↔ (#‘(𝑆‘𝑎)) = 𝑖)) |
61 | 58 | eqeq1d 2624 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑎 → ((𝑆‘𝑐) = (𝑆‘𝑑) ↔ (𝑆‘𝑎) = (𝑆‘𝑑))) |
62 | | fveq1 6190 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑎 → (𝑐‘0) = (𝑎‘0)) |
63 | 62 | eqeq1d 2624 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑎 → ((𝑐‘0) = (𝑑‘0) ↔ (𝑎‘0) = (𝑑‘0))) |
64 | 61, 63 | imbi12d 334 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑎 → (((𝑆‘𝑐) = (𝑆‘𝑑) → (𝑐‘0) = (𝑑‘0)) ↔ ((𝑆‘𝑎) = (𝑆‘𝑑) → (𝑎‘0) = (𝑑‘0)))) |
65 | 60, 64 | imbi12d 334 |
. . . . . . . . 9
⊢ (𝑐 = 𝑎 → (((#‘(𝑆‘𝑐)) = 𝑖 → ((𝑆‘𝑐) = (𝑆‘𝑑) → (𝑐‘0) = (𝑑‘0))) ↔ ((#‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑑) → (𝑎‘0) = (𝑑‘0))))) |
66 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝑏 → (𝑆‘𝑑) = (𝑆‘𝑏)) |
67 | 66 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑏 → ((𝑆‘𝑎) = (𝑆‘𝑑) ↔ (𝑆‘𝑎) = (𝑆‘𝑏))) |
68 | | fveq1 6190 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝑏 → (𝑑‘0) = (𝑏‘0)) |
69 | 68 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑏 → ((𝑎‘0) = (𝑑‘0) ↔ (𝑎‘0) = (𝑏‘0))) |
70 | 67, 69 | imbi12d 334 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑏 → (((𝑆‘𝑎) = (𝑆‘𝑑) → (𝑎‘0) = (𝑑‘0)) ↔ ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
71 | 70 | imbi2d 330 |
. . . . . . . . 9
⊢ (𝑑 = 𝑏 → (((#‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑑) → (𝑎‘0) = (𝑑‘0))) ↔ ((#‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
72 | 65, 71 | cbvral2v 3179 |
. . . . . . . 8
⊢
(∀𝑐 ∈
dom 𝑆∀𝑑 ∈ dom 𝑆((#‘(𝑆‘𝑐)) = 𝑖 → ((𝑆‘𝑐) = (𝑆‘𝑑) → (𝑐‘0) = (𝑑‘0))) ↔ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
73 | 57, 72 | sylib 208 |
. . . . . . 7
⊢
(∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
74 | 73 | ancli 574 |
. . . . . 6
⊢
(∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) → (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
75 | 35 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆) → (#‘(𝑆‘𝑎)) ∈
ℕ0) |
76 | | nn0leltp1 11436 |
. . . . . . . . . . . . 13
⊢
(((#‘(𝑆‘𝑎)) ∈ ℕ0 ∧ 𝑖 ∈ ℕ0)
→ ((#‘(𝑆‘𝑎)) ≤ 𝑖 ↔ (#‘(𝑆‘𝑎)) < (𝑖 + 1))) |
77 | | nn0re 11301 |
. . . . . . . . . . . . . 14
⊢
((#‘(𝑆‘𝑎)) ∈ ℕ0 →
(#‘(𝑆‘𝑎)) ∈
ℝ) |
78 | | nn0re 11301 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℝ) |
79 | | leloe 10124 |
. . . . . . . . . . . . . 14
⊢
(((#‘(𝑆‘𝑎)) ∈ ℝ ∧ 𝑖 ∈ ℝ) → ((#‘(𝑆‘𝑎)) ≤ 𝑖 ↔ ((#‘(𝑆‘𝑎)) < 𝑖 ∨ (#‘(𝑆‘𝑎)) = 𝑖))) |
80 | 77, 78, 79 | syl2an 494 |
. . . . . . . . . . . . 13
⊢
(((#‘(𝑆‘𝑎)) ∈ ℕ0 ∧ 𝑖 ∈ ℕ0)
→ ((#‘(𝑆‘𝑎)) ≤ 𝑖 ↔ ((#‘(𝑆‘𝑎)) < 𝑖 ∨ (#‘(𝑆‘𝑎)) = 𝑖))) |
81 | 76, 80 | bitr3d 270 |
. . . . . . . . . . . 12
⊢
(((#‘(𝑆‘𝑎)) ∈ ℕ0 ∧ 𝑖 ∈ ℕ0)
→ ((#‘(𝑆‘𝑎)) < (𝑖 + 1) ↔ ((#‘(𝑆‘𝑎)) < 𝑖 ∨ (#‘(𝑆‘𝑎)) = 𝑖))) |
82 | 81 | ancoms 469 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ ℕ0
∧ (#‘(𝑆‘𝑎)) ∈ ℕ0) →
((#‘(𝑆‘𝑎)) < (𝑖 + 1) ↔ ((#‘(𝑆‘𝑎)) < 𝑖 ∨ (#‘(𝑆‘𝑎)) = 𝑖))) |
83 | 75, 82 | sylan2 491 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ℕ0
∧ (𝑎 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆)) → ((#‘(𝑆‘𝑎)) < (𝑖 + 1) ↔ ((#‘(𝑆‘𝑎)) < 𝑖 ∨ (#‘(𝑆‘𝑎)) = 𝑖))) |
84 | 83 | imbi1d 331 |
. . . . . . . . 9
⊢ ((𝑖 ∈ ℕ0
∧ (𝑎 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆)) → (((#‘(𝑆‘𝑎)) < (𝑖 + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ (((#‘(𝑆‘𝑎)) < 𝑖 ∨ (#‘(𝑆‘𝑎)) = 𝑖) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
85 | | jaob 822 |
. . . . . . . . 9
⊢
((((#‘(𝑆‘𝑎)) < 𝑖 ∨ (#‘(𝑆‘𝑎)) = 𝑖) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ (((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ ((#‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
86 | 84, 85 | syl6bb 276 |
. . . . . . . 8
⊢ ((𝑖 ∈ ℕ0
∧ (𝑎 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆)) → (((#‘(𝑆‘𝑎)) < (𝑖 + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ (((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ ((#‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))))) |
87 | 86 | 2ralbidva 2988 |
. . . . . . 7
⊢ (𝑖 ∈ ℕ0
→ (∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (𝑖 + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆(((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ ((#‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))))) |
88 | | r19.26-2 3065 |
. . . . . . 7
⊢
(∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆(((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ ((#‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) ↔ (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
89 | 87, 88 | syl6bb 276 |
. . . . . 6
⊢ (𝑖 ∈ ℕ0
→ (∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (𝑖 + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))))) |
90 | 74, 89 | syl5ibr 236 |
. . . . 5
⊢ (𝑖 ∈ ℕ0
→ (∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < (𝑖 + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
91 | 22, 25, 28, 31, 40, 90 | nn0ind 11472 |
. . . 4
⊢
(((#‘(𝑆‘𝐴)) + 1) ∈ ℕ0 →
∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < ((#‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
92 | 19, 91 | syl 17 |
. . 3
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < ((#‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
93 | 17 | nn0red 11352 |
. . . 4
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → (#‘(𝑆‘𝐴)) ∈ ℝ) |
94 | 93 | ltp1d 10954 |
. . 3
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → (#‘(𝑆‘𝐴)) < ((#‘(𝑆‘𝐴)) + 1)) |
95 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (𝑆‘𝑎) = (𝑆‘𝐴)) |
96 | 95 | fveq2d 6195 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (#‘(𝑆‘𝑎)) = (#‘(𝑆‘𝐴))) |
97 | 96 | breq1d 4663 |
. . . . 5
⊢ (𝑎 = 𝐴 → ((#‘(𝑆‘𝑎)) < ((#‘(𝑆‘𝐴)) + 1) ↔ (#‘(𝑆‘𝐴)) < ((#‘(𝑆‘𝐴)) + 1))) |
98 | 95 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑎 = 𝐴 → ((𝑆‘𝑎) = (𝑆‘𝑏) ↔ (𝑆‘𝐴) = (𝑆‘𝑏))) |
99 | | fveq1 6190 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (𝑎‘0) = (𝐴‘0)) |
100 | 99 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑎 = 𝐴 → ((𝑎‘0) = (𝑏‘0) ↔ (𝐴‘0) = (𝑏‘0))) |
101 | 98, 100 | imbi12d 334 |
. . . . 5
⊢ (𝑎 = 𝐴 → (((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)) ↔ ((𝑆‘𝐴) = (𝑆‘𝑏) → (𝐴‘0) = (𝑏‘0)))) |
102 | 97, 101 | imbi12d 334 |
. . . 4
⊢ (𝑎 = 𝐴 → (((#‘(𝑆‘𝑎)) < ((#‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((#‘(𝑆‘𝐴)) < ((#‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝐴) = (𝑆‘𝑏) → (𝐴‘0) = (𝑏‘0))))) |
103 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (𝑆‘𝑏) = (𝑆‘𝐵)) |
104 | 103 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑏 = 𝐵 → ((𝑆‘𝐴) = (𝑆‘𝑏) ↔ (𝑆‘𝐴) = (𝑆‘𝐵))) |
105 | | fveq1 6190 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (𝑏‘0) = (𝐵‘0)) |
106 | 105 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑏 = 𝐵 → ((𝐴‘0) = (𝑏‘0) ↔ (𝐴‘0) = (𝐵‘0))) |
107 | 104, 106 | imbi12d 334 |
. . . . 5
⊢ (𝑏 = 𝐵 → (((𝑆‘𝐴) = (𝑆‘𝑏) → (𝐴‘0) = (𝑏‘0)) ↔ ((𝑆‘𝐴) = (𝑆‘𝐵) → (𝐴‘0) = (𝐵‘0)))) |
108 | 107 | imbi2d 330 |
. . . 4
⊢ (𝑏 = 𝐵 → (((#‘(𝑆‘𝐴)) < ((#‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝐴) = (𝑆‘𝑏) → (𝐴‘0) = (𝑏‘0))) ↔ ((#‘(𝑆‘𝐴)) < ((#‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝐴) = (𝑆‘𝐵) → (𝐴‘0) = (𝐵‘0))))) |
109 | 102, 108 | rspc2v 3322 |
. . 3
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((#‘(𝑆‘𝑎)) < ((#‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) → ((#‘(𝑆‘𝐴)) < ((#‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝐴) = (𝑆‘𝐵) → (𝐴‘0) = (𝐵‘0))))) |
110 | 92, 94, 109 | mp2d 49 |
. 2
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → ((𝑆‘𝐴) = (𝑆‘𝐵) → (𝐴‘0) = (𝐵‘0))) |
111 | 110 | 3impia 1261 |
1
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆 ∧ (𝑆‘𝐴) = (𝑆‘𝐵)) → (𝐴‘0) = (𝐵‘0)) |