Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . . . . . 8
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) |
2 | | fviss 6747 |
. . . . . . . 8
⊢ ( I
‘Word (𝐼 ×
2o)) ⊆ Word (𝐼 × 2o) |
3 | 1, 2 | eqsstri 3911 |
. . . . . . 7
⊢ 𝑊 ⊆ Word (𝐼 × 2o) |
4 | | efgval.r |
. . . . . . . . . . 11
⊢ ∼ = (
~FG ‘𝐼) |
5 | | efgval2.m |
. . . . . . . . . . 11
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) |
6 | | efgval2.t |
. . . . . . . . . . 11
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
7 | | efgred.d |
. . . . . . . . . . 11
⊢ 𝐷 = (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) |
8 | | efgred.s |
. . . . . . . . . . 11
⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈
(1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1))) |
9 | 1, 4, 5, 6, 7, 8 | efgsf 18975 |
. . . . . . . . . 10
⊢ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈
(1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊 |
10 | 9 | fdmi 6516 |
. . . . . . . . . . 11
⊢ dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈
(1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} |
11 | 10 | feq2i 6496 |
. . . . . . . . . 10
⊢ (𝑆:dom 𝑆⟶𝑊 ↔ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈
(1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊) |
12 | 9, 11 | mpbir 234 |
. . . . . . . . 9
⊢ 𝑆:dom 𝑆⟶𝑊 |
13 | 12 | ffvelrni 6862 |
. . . . . . . 8
⊢ (𝐴 ∈ dom 𝑆 → (𝑆‘𝐴) ∈ 𝑊) |
14 | 13 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → (𝑆‘𝐴) ∈ 𝑊) |
15 | 3, 14 | sseldi 3875 |
. . . . . 6
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → (𝑆‘𝐴) ∈ Word (𝐼 × 2o)) |
16 | | lencl 13976 |
. . . . . 6
⊢ ((𝑆‘𝐴) ∈ Word (𝐼 × 2o) →
(♯‘(𝑆‘𝐴)) ∈
ℕ0) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → (♯‘(𝑆‘𝐴)) ∈
ℕ0) |
18 | | peano2nn0 12018 |
. . . . 5
⊢
((♯‘(𝑆‘𝐴)) ∈ ℕ0 →
((♯‘(𝑆‘𝐴)) + 1) ∈
ℕ0) |
19 | 17, 18 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → ((♯‘(𝑆‘𝐴)) + 1) ∈
ℕ0) |
20 | | breq2 5034 |
. . . . . . 7
⊢ (𝑐 = 0 →
((♯‘(𝑆‘𝑎)) < 𝑐 ↔ (♯‘(𝑆‘𝑎)) < 0)) |
21 | 20 | imbi1d 345 |
. . . . . 6
⊢ (𝑐 = 0 →
(((♯‘(𝑆‘𝑎)) < 𝑐 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((♯‘(𝑆‘𝑎)) < 0 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
22 | 21 | 2ralbidv 3111 |
. . . . 5
⊢ (𝑐 = 0 → (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑐 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 0 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
23 | | breq2 5034 |
. . . . . . 7
⊢ (𝑐 = 𝑖 → ((♯‘(𝑆‘𝑎)) < 𝑐 ↔ (♯‘(𝑆‘𝑎)) < 𝑖)) |
24 | 23 | imbi1d 345 |
. . . . . 6
⊢ (𝑐 = 𝑖 → (((♯‘(𝑆‘𝑎)) < 𝑐 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
25 | 24 | 2ralbidv 3111 |
. . . . 5
⊢ (𝑐 = 𝑖 → (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑐 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
26 | | breq2 5034 |
. . . . . . 7
⊢ (𝑐 = (𝑖 + 1) → ((♯‘(𝑆‘𝑎)) < 𝑐 ↔ (♯‘(𝑆‘𝑎)) < (𝑖 + 1))) |
27 | 26 | imbi1d 345 |
. . . . . 6
⊢ (𝑐 = (𝑖 + 1) → (((♯‘(𝑆‘𝑎)) < 𝑐 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((♯‘(𝑆‘𝑎)) < (𝑖 + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
28 | 27 | 2ralbidv 3111 |
. . . . 5
⊢ (𝑐 = (𝑖 + 1) → (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑐 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (𝑖 + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
29 | | breq2 5034 |
. . . . . . 7
⊢ (𝑐 = ((♯‘(𝑆‘𝐴)) + 1) → ((♯‘(𝑆‘𝑎)) < 𝑐 ↔ (♯‘(𝑆‘𝑎)) < ((♯‘(𝑆‘𝐴)) + 1))) |
30 | 29 | imbi1d 345 |
. . . . . 6
⊢ (𝑐 = ((♯‘(𝑆‘𝐴)) + 1) → (((♯‘(𝑆‘𝑎)) < 𝑐 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((♯‘(𝑆‘𝑎)) < ((♯‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
31 | 30 | 2ralbidv 3111 |
. . . . 5
⊢ (𝑐 = ((♯‘(𝑆‘𝐴)) + 1) → (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑐 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < ((♯‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
32 | 12 | ffvelrni 6862 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ dom 𝑆 → (𝑆‘𝑎) ∈ 𝑊) |
33 | 3, 32 | sseldi 3875 |
. . . . . . . . . 10
⊢ (𝑎 ∈ dom 𝑆 → (𝑆‘𝑎) ∈ Word (𝐼 × 2o)) |
34 | | lencl 13976 |
. . . . . . . . . 10
⊢ ((𝑆‘𝑎) ∈ Word (𝐼 × 2o) →
(♯‘(𝑆‘𝑎)) ∈
ℕ0) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ (𝑎 ∈ dom 𝑆 → (♯‘(𝑆‘𝑎)) ∈
ℕ0) |
36 | | nn0nlt0 12004 |
. . . . . . . . 9
⊢
((♯‘(𝑆‘𝑎)) ∈ ℕ0 → ¬
(♯‘(𝑆‘𝑎)) < 0) |
37 | 35, 36 | syl 17 |
. . . . . . . 8
⊢ (𝑎 ∈ dom 𝑆 → ¬ (♯‘(𝑆‘𝑎)) < 0) |
38 | 37 | pm2.21d 121 |
. . . . . . 7
⊢ (𝑎 ∈ dom 𝑆 → ((♯‘(𝑆‘𝑎)) < 0 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
39 | 38 | adantr 484 |
. . . . . 6
⊢ ((𝑎 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆) → ((♯‘(𝑆‘𝑎)) < 0 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
40 | 39 | rgen2 3115 |
. . . . 5
⊢
∀𝑎 ∈ dom
𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 0 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) |
41 | | simpl1 1192 |
. . . . . . . . . . . . . 14
⊢
(((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((♯‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0)) → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
42 | | simpl3l 1229 |
. . . . . . . . . . . . . . 15
⊢
(((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((♯‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0)) → (♯‘(𝑆‘𝑐)) = 𝑖) |
43 | | breq2 5034 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘(𝑆‘𝑐)) = 𝑖 → ((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝑐)) ↔ (♯‘(𝑆‘𝑎)) < 𝑖)) |
44 | 43 | imbi1d 345 |
. . . . . . . . . . . . . . . 16
⊢
((♯‘(𝑆‘𝑐)) = 𝑖 → (((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝑐)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
45 | 44 | 2ralbidv 3111 |
. . . . . . . . . . . . . . 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 260 |
. . . . . . . . . . . . 13
⊢
(((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((♯‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0)) → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (♯‘(𝑆‘𝑐)) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
48 | | simpl2l 1227 |
. . . . . . . . . . . . 13
⊢
(((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((♯‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0)) → 𝑐 ∈ dom 𝑆) |
49 | | simpl2r 1228 |
. . . . . . . . . . . . 13
⊢
(((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((♯‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0)) → 𝑑 ∈ dom 𝑆) |
50 | | simpl3r 1230 |
. . . . . . . . . . . . 13
⊢
(((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((♯‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0)) → (𝑆‘𝑐) = (𝑆‘𝑑)) |
51 | | simpr 488 |
. . . . . . . . . . . . 13
⊢
(((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((♯‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0)) → ¬ (𝑐‘0) = (𝑑‘0)) |
52 | 1, 4, 5, 6, 7, 8, 47, 48, 49, 50, 51 | efgredlem 18993 |
. . . . . . . . . . . 12
⊢ ¬
((∀𝑎 ∈ dom
𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((♯‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0)) |
53 | | iman 405 |
. . . . . . . . . . . 12
⊢
(((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((♯‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) → (𝑐‘0) = (𝑑‘0)) ↔ ¬ ((∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((♯‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) ∧ ¬ (𝑐‘0) = (𝑑‘0))) |
54 | 52, 53 | mpbir 234 |
. . . . . . . . . . 11
⊢
((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆) ∧ ((♯‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑))) → (𝑐‘0) = (𝑑‘0)) |
55 | 54 | 3expia 1122 |
. . . . . . . . . 10
⊢
((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆)) → (((♯‘(𝑆‘𝑐)) = 𝑖 ∧ (𝑆‘𝑐) = (𝑆‘𝑑)) → (𝑐‘0) = (𝑑‘0))) |
56 | 55 | expd 419 |
. . . . . . . . 9
⊢
((∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ (𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆)) → ((♯‘(𝑆‘𝑐)) = 𝑖 → ((𝑆‘𝑐) = (𝑆‘𝑑) → (𝑐‘0) = (𝑑‘0)))) |
57 | 56 | ralrimivva 3103 |
. . . . . . . 8
⊢
(∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) → ∀𝑐 ∈ dom 𝑆∀𝑑 ∈ dom 𝑆((♯‘(𝑆‘𝑐)) = 𝑖 → ((𝑆‘𝑐) = (𝑆‘𝑑) → (𝑐‘0) = (𝑑‘0)))) |
58 | | 2fveq3 6681 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑎 → (♯‘(𝑆‘𝑐)) = (♯‘(𝑆‘𝑎))) |
59 | 58 | eqeq1d 2740 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑎 → ((♯‘(𝑆‘𝑐)) = 𝑖 ↔ (♯‘(𝑆‘𝑎)) = 𝑖)) |
60 | | fveqeq2 6685 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑎 → ((𝑆‘𝑐) = (𝑆‘𝑑) ↔ (𝑆‘𝑎) = (𝑆‘𝑑))) |
61 | | fveq1 6675 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑎 → (𝑐‘0) = (𝑎‘0)) |
62 | 61 | eqeq1d 2740 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑎 → ((𝑐‘0) = (𝑑‘0) ↔ (𝑎‘0) = (𝑑‘0))) |
63 | 60, 62 | imbi12d 348 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑎 → (((𝑆‘𝑐) = (𝑆‘𝑑) → (𝑐‘0) = (𝑑‘0)) ↔ ((𝑆‘𝑎) = (𝑆‘𝑑) → (𝑎‘0) = (𝑑‘0)))) |
64 | 59, 63 | imbi12d 348 |
. . . . . . . . 9
⊢ (𝑐 = 𝑎 → (((♯‘(𝑆‘𝑐)) = 𝑖 → ((𝑆‘𝑐) = (𝑆‘𝑑) → (𝑐‘0) = (𝑑‘0))) ↔ ((♯‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑑) → (𝑎‘0) = (𝑑‘0))))) |
65 | | fveq2 6676 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝑏 → (𝑆‘𝑑) = (𝑆‘𝑏)) |
66 | 65 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑏 → ((𝑆‘𝑎) = (𝑆‘𝑑) ↔ (𝑆‘𝑎) = (𝑆‘𝑏))) |
67 | | fveq1 6675 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝑏 → (𝑑‘0) = (𝑏‘0)) |
68 | 67 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑏 → ((𝑎‘0) = (𝑑‘0) ↔ (𝑎‘0) = (𝑏‘0))) |
69 | 66, 68 | imbi12d 348 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑏 → (((𝑆‘𝑎) = (𝑆‘𝑑) → (𝑎‘0) = (𝑑‘0)) ↔ ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
70 | 69 | imbi2d 344 |
. . . . . . . . 9
⊢ (𝑑 = 𝑏 → (((♯‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑑) → (𝑎‘0) = (𝑑‘0))) ↔ ((♯‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
71 | 64, 70 | cbvral2vw 3362 |
. . . . . . . 8
⊢
(∀𝑐 ∈
dom 𝑆∀𝑑 ∈ dom 𝑆((♯‘(𝑆‘𝑐)) = 𝑖 → ((𝑆‘𝑐) = (𝑆‘𝑑) → (𝑐‘0) = (𝑑‘0))) ↔ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
72 | 57, 71 | sylib 221 |
. . . . . . 7
⊢
(∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
73 | 72 | ancli 552 |
. . . . . 6
⊢
(∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) → (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
74 | 35 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆) → (♯‘(𝑆‘𝑎)) ∈
ℕ0) |
75 | | nn0leltp1 12124 |
. . . . . . . . . . . . 13
⊢
(((♯‘(𝑆‘𝑎)) ∈ ℕ0 ∧ 𝑖 ∈ ℕ0)
→ ((♯‘(𝑆‘𝑎)) ≤ 𝑖 ↔ (♯‘(𝑆‘𝑎)) < (𝑖 + 1))) |
76 | | nn0re 11987 |
. . . . . . . . . . . . . 14
⊢
((♯‘(𝑆‘𝑎)) ∈ ℕ0 →
(♯‘(𝑆‘𝑎)) ∈ ℝ) |
77 | | nn0re 11987 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℝ) |
78 | | leloe 10807 |
. . . . . . . . . . . . . 14
⊢
(((♯‘(𝑆‘𝑎)) ∈ ℝ ∧ 𝑖 ∈ ℝ) →
((♯‘(𝑆‘𝑎)) ≤ 𝑖 ↔ ((♯‘(𝑆‘𝑎)) < 𝑖 ∨ (♯‘(𝑆‘𝑎)) = 𝑖))) |
79 | 76, 77, 78 | syl2an 599 |
. . . . . . . . . . . . 13
⊢
(((♯‘(𝑆‘𝑎)) ∈ ℕ0 ∧ 𝑖 ∈ ℕ0)
→ ((♯‘(𝑆‘𝑎)) ≤ 𝑖 ↔ ((♯‘(𝑆‘𝑎)) < 𝑖 ∨ (♯‘(𝑆‘𝑎)) = 𝑖))) |
80 | 75, 79 | bitr3d 284 |
. . . . . . . . . . . 12
⊢
(((♯‘(𝑆‘𝑎)) ∈ ℕ0 ∧ 𝑖 ∈ ℕ0)
→ ((♯‘(𝑆‘𝑎)) < (𝑖 + 1) ↔ ((♯‘(𝑆‘𝑎)) < 𝑖 ∨ (♯‘(𝑆‘𝑎)) = 𝑖))) |
81 | 80 | ancoms 462 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ ℕ0
∧ (♯‘(𝑆‘𝑎)) ∈ ℕ0) →
((♯‘(𝑆‘𝑎)) < (𝑖 + 1) ↔ ((♯‘(𝑆‘𝑎)) < 𝑖 ∨ (♯‘(𝑆‘𝑎)) = 𝑖))) |
82 | 74, 81 | sylan2 596 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ℕ0
∧ (𝑎 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆)) → ((♯‘(𝑆‘𝑎)) < (𝑖 + 1) ↔ ((♯‘(𝑆‘𝑎)) < 𝑖 ∨ (♯‘(𝑆‘𝑎)) = 𝑖))) |
83 | 82 | imbi1d 345 |
. . . . . . . . 9
⊢ ((𝑖 ∈ ℕ0
∧ (𝑎 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆)) → (((♯‘(𝑆‘𝑎)) < (𝑖 + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ (((♯‘(𝑆‘𝑎)) < 𝑖 ∨ (♯‘(𝑆‘𝑎)) = 𝑖) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
84 | | jaob 961 |
. . . . . . . . 9
⊢
((((♯‘(𝑆‘𝑎)) < 𝑖 ∨ (♯‘(𝑆‘𝑎)) = 𝑖) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ (((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ ((♯‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
85 | 83, 84 | bitrdi 290 |
. . . . . . . 8
⊢ ((𝑖 ∈ ℕ0
∧ (𝑎 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆)) → (((♯‘(𝑆‘𝑎)) < (𝑖 + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ (((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ ((♯‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))))) |
86 | 85 | 2ralbidva 3110 |
. . . . . . 7
⊢ (𝑖 ∈ ℕ0
→ (∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (𝑖 + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆(((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ ((♯‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))))) |
87 | | r19.26-2 3085 |
. . . . . . 7
⊢
(∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆(((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ ((♯‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) ↔ (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
88 | 86, 87 | bitrdi 290 |
. . . . . 6
⊢ (𝑖 ∈ ℕ0
→ (∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (𝑖 + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ∧ ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) = 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))))) |
89 | 73, 88 | syl5ibr 249 |
. . . . 5
⊢ (𝑖 ∈ ℕ0
→ (∀𝑎 ∈
dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < 𝑖 → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < (𝑖 + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))))) |
90 | 22, 25, 28, 31, 40, 89 | nn0ind 12160 |
. . . 4
⊢
(((♯‘(𝑆‘𝐴)) + 1) ∈ ℕ0 →
∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < ((♯‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
91 | 19, 90 | syl 17 |
. . 3
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → ∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < ((♯‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)))) |
92 | 17 | nn0red 12039 |
. . . 4
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → (♯‘(𝑆‘𝐴)) ∈ ℝ) |
93 | 92 | ltp1d 11650 |
. . 3
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → (♯‘(𝑆‘𝐴)) < ((♯‘(𝑆‘𝐴)) + 1)) |
94 | | 2fveq3 6681 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (♯‘(𝑆‘𝑎)) = (♯‘(𝑆‘𝐴))) |
95 | 94 | breq1d 5040 |
. . . . 5
⊢ (𝑎 = 𝐴 → ((♯‘(𝑆‘𝑎)) < ((♯‘(𝑆‘𝐴)) + 1) ↔ (♯‘(𝑆‘𝐴)) < ((♯‘(𝑆‘𝐴)) + 1))) |
96 | | fveqeq2 6685 |
. . . . . 6
⊢ (𝑎 = 𝐴 → ((𝑆‘𝑎) = (𝑆‘𝑏) ↔ (𝑆‘𝐴) = (𝑆‘𝑏))) |
97 | | fveq1 6675 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (𝑎‘0) = (𝐴‘0)) |
98 | 97 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑎 = 𝐴 → ((𝑎‘0) = (𝑏‘0) ↔ (𝐴‘0) = (𝑏‘0))) |
99 | 96, 98 | imbi12d 348 |
. . . . 5
⊢ (𝑎 = 𝐴 → (((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0)) ↔ ((𝑆‘𝐴) = (𝑆‘𝑏) → (𝐴‘0) = (𝑏‘0)))) |
100 | 95, 99 | imbi12d 348 |
. . . 4
⊢ (𝑎 = 𝐴 → (((♯‘(𝑆‘𝑎)) < ((♯‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) ↔ ((♯‘(𝑆‘𝐴)) < ((♯‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝐴) = (𝑆‘𝑏) → (𝐴‘0) = (𝑏‘0))))) |
101 | | fveq2 6676 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (𝑆‘𝑏) = (𝑆‘𝐵)) |
102 | 101 | eqeq2d 2749 |
. . . . . 6
⊢ (𝑏 = 𝐵 → ((𝑆‘𝐴) = (𝑆‘𝑏) ↔ (𝑆‘𝐴) = (𝑆‘𝐵))) |
103 | | fveq1 6675 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (𝑏‘0) = (𝐵‘0)) |
104 | 103 | eqeq2d 2749 |
. . . . . 6
⊢ (𝑏 = 𝐵 → ((𝐴‘0) = (𝑏‘0) ↔ (𝐴‘0) = (𝐵‘0))) |
105 | 102, 104 | imbi12d 348 |
. . . . 5
⊢ (𝑏 = 𝐵 → (((𝑆‘𝐴) = (𝑆‘𝑏) → (𝐴‘0) = (𝑏‘0)) ↔ ((𝑆‘𝐴) = (𝑆‘𝐵) → (𝐴‘0) = (𝐵‘0)))) |
106 | 105 | imbi2d 344 |
. . . 4
⊢ (𝑏 = 𝐵 → (((♯‘(𝑆‘𝐴)) < ((♯‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝐴) = (𝑆‘𝑏) → (𝐴‘0) = (𝑏‘0))) ↔ ((♯‘(𝑆‘𝐴)) < ((♯‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝐴) = (𝑆‘𝐵) → (𝐴‘0) = (𝐵‘0))))) |
107 | 100, 106 | rspc2v 3536 |
. . 3
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → (∀𝑎 ∈ dom 𝑆∀𝑏 ∈ dom 𝑆((♯‘(𝑆‘𝑎)) < ((♯‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝑎) = (𝑆‘𝑏) → (𝑎‘0) = (𝑏‘0))) → ((♯‘(𝑆‘𝐴)) < ((♯‘(𝑆‘𝐴)) + 1) → ((𝑆‘𝐴) = (𝑆‘𝐵) → (𝐴‘0) = (𝐵‘0))))) |
108 | 91, 93, 107 | mp2d 49 |
. 2
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆) → ((𝑆‘𝐴) = (𝑆‘𝐵) → (𝐴‘0) = (𝐵‘0))) |
109 | 108 | 3impia 1118 |
1
⊢ ((𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆 ∧ (𝑆‘𝐴) = (𝑆‘𝐵)) → (𝐴‘0) = (𝐵‘0)) |