# Metamath Proof Explorer

## Theorem efgred

Description: The reduced word that forms the base of the sequence in efgsval is uniquely determined, given the terminal point. (Contributed by Mario Carneiro, 28-Sep-2015)

Ref Expression
Hypotheses efgval.w ${⊢}{W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
efgval.r
efgval2.m ${⊢}{M}=\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)$
efgval2.t ${⊢}{T}=\left({v}\in {W}⟼\left({n}\in \left(0\dots \left|{v}\right|\right),{w}\in \left({I}×{2}_{𝑜}\right)⟼{v}\mathrm{splice}⟨{n},{n},⟨“{w}{M}\left({w}\right)”⟩⟩\right)\right)$
efgred.d ${⊢}{D}={W}\setminus \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)$
efgred.s ${⊢}{S}=\left({m}\in \left\{{t}\in \left(\mathrm{Word}{W}\setminus \left\{\varnothing \right\}\right)|\left({t}\left(0\right)\in {D}\wedge \forall {k}\in \left(1..^\left|{t}\right|\right)\phantom{\rule{.4em}{0ex}}{t}\left({k}\right)\in \mathrm{ran}{T}\left({t}\left({k}-1\right)\right)\right)\right\}⟼{m}\left(\left|{m}\right|-1\right)\right)$
Assertion efgred ${⊢}\left({A}\in \mathrm{dom}{S}\wedge {B}\in \mathrm{dom}{S}\wedge {S}\left({A}\right)={S}\left({B}\right)\right)\to {A}\left(0\right)={B}\left(0\right)$

### Proof

Step Hyp Ref Expression
1 efgval.w ${⊢}{W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
2 efgval.r
3 efgval2.m ${⊢}{M}=\left({y}\in {I},{z}\in {2}_{𝑜}⟼⟨{y},{1}_{𝑜}\setminus {z}⟩\right)$
4 efgval2.t ${⊢}{T}=\left({v}\in {W}⟼\left({n}\in \left(0\dots \left|{v}\right|\right),{w}\in \left({I}×{2}_{𝑜}\right)⟼{v}\mathrm{splice}⟨{n},{n},⟨“{w}{M}\left({w}\right)”⟩⟩\right)\right)$
5 efgred.d ${⊢}{D}={W}\setminus \bigcup _{{x}\in {W}}\mathrm{ran}{T}\left({x}\right)$
6 efgred.s ${⊢}{S}=\left({m}\in \left\{{t}\in \left(\mathrm{Word}{W}\setminus \left\{\varnothing \right\}\right)|\left({t}\left(0\right)\in {D}\wedge \forall {k}\in \left(1..^\left|{t}\right|\right)\phantom{\rule{.4em}{0ex}}{t}\left({k}\right)\in \mathrm{ran}{T}\left({t}\left({k}-1\right)\right)\right)\right\}⟼{m}\left(\left|{m}\right|-1\right)\right)$
7 fviss ${⊢}\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\subseteq \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
8 1 7 eqsstri ${⊢}{W}\subseteq \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
9 1 2 3 4 5 6 efgsf ${⊢}{S}:\left\{{t}\in \left(\mathrm{Word}{W}\setminus \left\{\varnothing \right\}\right)|\left({t}\left(0\right)\in {D}\wedge \forall {k}\in \left(1..^\left|{t}\right|\right)\phantom{\rule{.4em}{0ex}}{t}\left({k}\right)\in \mathrm{ran}{T}\left({t}\left({k}-1\right)\right)\right)\right\}⟶{W}$
10 9 fdmi ${⊢}\mathrm{dom}{S}=\left\{{t}\in \left(\mathrm{Word}{W}\setminus \left\{\varnothing \right\}\right)|\left({t}\left(0\right)\in {D}\wedge \forall {k}\in \left(1..^\left|{t}\right|\right)\phantom{\rule{.4em}{0ex}}{t}\left({k}\right)\in \mathrm{ran}{T}\left({t}\left({k}-1\right)\right)\right)\right\}$
11 10 feq2i ${⊢}{S}:\mathrm{dom}{S}⟶{W}↔{S}:\left\{{t}\in \left(\mathrm{Word}{W}\setminus \left\{\varnothing \right\}\right)|\left({t}\left(0\right)\in {D}\wedge \forall {k}\in \left(1..^\left|{t}\right|\right)\phantom{\rule{.4em}{0ex}}{t}\left({k}\right)\in \mathrm{ran}{T}\left({t}\left({k}-1\right)\right)\right)\right\}⟶{W}$
12 9 11 mpbir ${⊢}{S}:\mathrm{dom}{S}⟶{W}$
13 12 ffvelrni ${⊢}{A}\in \mathrm{dom}{S}\to {S}\left({A}\right)\in {W}$
14 13 adantr ${⊢}\left({A}\in \mathrm{dom}{S}\wedge {B}\in \mathrm{dom}{S}\right)\to {S}\left({A}\right)\in {W}$
15 8 14 sseldi ${⊢}\left({A}\in \mathrm{dom}{S}\wedge {B}\in \mathrm{dom}{S}\right)\to {S}\left({A}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
16 lencl ${⊢}{S}\left({A}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to \left|{S}\left({A}\right)\right|\in {ℕ}_{0}$
17 15 16 syl ${⊢}\left({A}\in \mathrm{dom}{S}\wedge {B}\in \mathrm{dom}{S}\right)\to \left|{S}\left({A}\right)\right|\in {ℕ}_{0}$
18 peano2nn0 ${⊢}\left|{S}\left({A}\right)\right|\in {ℕ}_{0}\to \left|{S}\left({A}\right)\right|+1\in {ℕ}_{0}$
19 17 18 syl ${⊢}\left({A}\in \mathrm{dom}{S}\wedge {B}\in \mathrm{dom}{S}\right)\to \left|{S}\left({A}\right)\right|+1\in {ℕ}_{0}$
20 breq2 ${⊢}{c}=0\to \left(\left|{S}\left({a}\right)\right|<{c}↔\left|{S}\left({a}\right)\right|<0\right)$
21 20 imbi1d ${⊢}{c}=0\to \left(\left(\left|{S}\left({a}\right)\right|<{c}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)↔\left(\left|{S}\left({a}\right)\right|<0\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)$
22 21 2ralbidv ${⊢}{c}=0\to \left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{c}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)↔\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<0\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)$
23 breq2 ${⊢}{c}={i}\to \left(\left|{S}\left({a}\right)\right|<{c}↔\left|{S}\left({a}\right)\right|<{i}\right)$
24 23 imbi1d ${⊢}{c}={i}\to \left(\left(\left|{S}\left({a}\right)\right|<{c}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)↔\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)$
25 24 2ralbidv ${⊢}{c}={i}\to \left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{c}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)↔\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)$
26 breq2 ${⊢}{c}={i}+1\to \left(\left|{S}\left({a}\right)\right|<{c}↔\left|{S}\left({a}\right)\right|<{i}+1\right)$
27 26 imbi1d ${⊢}{c}={i}+1\to \left(\left(\left|{S}\left({a}\right)\right|<{c}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)↔\left(\left|{S}\left({a}\right)\right|<{i}+1\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)$
28 27 2ralbidv ${⊢}{c}={i}+1\to \left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{c}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)↔\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}+1\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)$
29 breq2 ${⊢}{c}=\left|{S}\left({A}\right)\right|+1\to \left(\left|{S}\left({a}\right)\right|<{c}↔\left|{S}\left({a}\right)\right|<\left|{S}\left({A}\right)\right|+1\right)$
30 29 imbi1d ${⊢}{c}=\left|{S}\left({A}\right)\right|+1\to \left(\left(\left|{S}\left({a}\right)\right|<{c}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)↔\left(\left|{S}\left({a}\right)\right|<\left|{S}\left({A}\right)\right|+1\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)$
31 30 2ralbidv ${⊢}{c}=\left|{S}\left({A}\right)\right|+1\to \left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{c}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)↔\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<\left|{S}\left({A}\right)\right|+1\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)$
32 12 ffvelrni ${⊢}{a}\in \mathrm{dom}{S}\to {S}\left({a}\right)\in {W}$
33 8 32 sseldi ${⊢}{a}\in \mathrm{dom}{S}\to {S}\left({a}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
34 lencl ${⊢}{S}\left({a}\right)\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\to \left|{S}\left({a}\right)\right|\in {ℕ}_{0}$
35 33 34 syl ${⊢}{a}\in \mathrm{dom}{S}\to \left|{S}\left({a}\right)\right|\in {ℕ}_{0}$
36 nn0nlt0 ${⊢}\left|{S}\left({a}\right)\right|\in {ℕ}_{0}\to ¬\left|{S}\left({a}\right)\right|<0$
37 35 36 syl ${⊢}{a}\in \mathrm{dom}{S}\to ¬\left|{S}\left({a}\right)\right|<0$
38 37 pm2.21d ${⊢}{a}\in \mathrm{dom}{S}\to \left(\left|{S}\left({a}\right)\right|<0\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)$
39 38 adantr ${⊢}\left({a}\in \mathrm{dom}{S}\wedge {b}\in \mathrm{dom}{S}\right)\to \left(\left|{S}\left({a}\right)\right|<0\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)$
40 39 rgen2 ${⊢}\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<0\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)$
41 simpl1 ${⊢}\left(\left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left({c}\in \mathrm{dom}{S}\wedge {d}\in \mathrm{dom}{S}\right)\wedge \left(\left|{S}\left({c}\right)\right|={i}\wedge {S}\left({c}\right)={S}\left({d}\right)\right)\right)\wedge ¬{c}\left(0\right)={d}\left(0\right)\right)\to \forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)$
42 simpl3l ${⊢}\left(\left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left({c}\in \mathrm{dom}{S}\wedge {d}\in \mathrm{dom}{S}\right)\wedge \left(\left|{S}\left({c}\right)\right|={i}\wedge {S}\left({c}\right)={S}\left({d}\right)\right)\right)\wedge ¬{c}\left(0\right)={d}\left(0\right)\right)\to \left|{S}\left({c}\right)\right|={i}$
43 breq2 ${⊢}\left|{S}\left({c}\right)\right|={i}\to \left(\left|{S}\left({a}\right)\right|<\left|{S}\left({c}\right)\right|↔\left|{S}\left({a}\right)\right|<{i}\right)$
44 43 imbi1d ${⊢}\left|{S}\left({c}\right)\right|={i}\to \left(\left(\left|{S}\left({a}\right)\right|<\left|{S}\left({c}\right)\right|\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)↔\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)$
45 44 2ralbidv ${⊢}\left|{S}\left({c}\right)\right|={i}\to \left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<\left|{S}\left({c}\right)\right|\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)↔\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)$
46 42 45 syl ${⊢}\left(\left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left({c}\in \mathrm{dom}{S}\wedge {d}\in \mathrm{dom}{S}\right)\wedge \left(\left|{S}\left({c}\right)\right|={i}\wedge {S}\left({c}\right)={S}\left({d}\right)\right)\right)\wedge ¬{c}\left(0\right)={d}\left(0\right)\right)\to \left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<\left|{S}\left({c}\right)\right|\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)↔\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)$
47 41 46 mpbird ${⊢}\left(\left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left({c}\in \mathrm{dom}{S}\wedge {d}\in \mathrm{dom}{S}\right)\wedge \left(\left|{S}\left({c}\right)\right|={i}\wedge {S}\left({c}\right)={S}\left({d}\right)\right)\right)\wedge ¬{c}\left(0\right)={d}\left(0\right)\right)\to \forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<\left|{S}\left({c}\right)\right|\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)$
48 simpl2l ${⊢}\left(\left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left({c}\in \mathrm{dom}{S}\wedge {d}\in \mathrm{dom}{S}\right)\wedge \left(\left|{S}\left({c}\right)\right|={i}\wedge {S}\left({c}\right)={S}\left({d}\right)\right)\right)\wedge ¬{c}\left(0\right)={d}\left(0\right)\right)\to {c}\in \mathrm{dom}{S}$
49 simpl2r ${⊢}\left(\left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left({c}\in \mathrm{dom}{S}\wedge {d}\in \mathrm{dom}{S}\right)\wedge \left(\left|{S}\left({c}\right)\right|={i}\wedge {S}\left({c}\right)={S}\left({d}\right)\right)\right)\wedge ¬{c}\left(0\right)={d}\left(0\right)\right)\to {d}\in \mathrm{dom}{S}$
50 simpl3r ${⊢}\left(\left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left({c}\in \mathrm{dom}{S}\wedge {d}\in \mathrm{dom}{S}\right)\wedge \left(\left|{S}\left({c}\right)\right|={i}\wedge {S}\left({c}\right)={S}\left({d}\right)\right)\right)\wedge ¬{c}\left(0\right)={d}\left(0\right)\right)\to {S}\left({c}\right)={S}\left({d}\right)$
51 simpr ${⊢}\left(\left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left({c}\in \mathrm{dom}{S}\wedge {d}\in \mathrm{dom}{S}\right)\wedge \left(\left|{S}\left({c}\right)\right|={i}\wedge {S}\left({c}\right)={S}\left({d}\right)\right)\right)\wedge ¬{c}\left(0\right)={d}\left(0\right)\right)\to ¬{c}\left(0\right)={d}\left(0\right)$
52 1 2 3 4 5 6 47 48 49 50 51 efgredlem ${⊢}¬\left(\left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left({c}\in \mathrm{dom}{S}\wedge {d}\in \mathrm{dom}{S}\right)\wedge \left(\left|{S}\left({c}\right)\right|={i}\wedge {S}\left({c}\right)={S}\left({d}\right)\right)\right)\wedge ¬{c}\left(0\right)={d}\left(0\right)\right)$
53 iman ${⊢}\left(\left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left({c}\in \mathrm{dom}{S}\wedge {d}\in \mathrm{dom}{S}\right)\wedge \left(\left|{S}\left({c}\right)\right|={i}\wedge {S}\left({c}\right)={S}\left({d}\right)\right)\right)\to {c}\left(0\right)={d}\left(0\right)\right)↔¬\left(\left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left({c}\in \mathrm{dom}{S}\wedge {d}\in \mathrm{dom}{S}\right)\wedge \left(\left|{S}\left({c}\right)\right|={i}\wedge {S}\left({c}\right)={S}\left({d}\right)\right)\right)\wedge ¬{c}\left(0\right)={d}\left(0\right)\right)$
54 52 53 mpbir ${⊢}\left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left({c}\in \mathrm{dom}{S}\wedge {d}\in \mathrm{dom}{S}\right)\wedge \left(\left|{S}\left({c}\right)\right|={i}\wedge {S}\left({c}\right)={S}\left({d}\right)\right)\right)\to {c}\left(0\right)={d}\left(0\right)$
55 54 3expia ${⊢}\left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left({c}\in \mathrm{dom}{S}\wedge {d}\in \mathrm{dom}{S}\right)\right)\to \left(\left(\left|{S}\left({c}\right)\right|={i}\wedge {S}\left({c}\right)={S}\left({d}\right)\right)\to {c}\left(0\right)={d}\left(0\right)\right)$
56 55 expd ${⊢}\left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left({c}\in \mathrm{dom}{S}\wedge {d}\in \mathrm{dom}{S}\right)\right)\to \left(\left|{S}\left({c}\right)\right|={i}\to \left({S}\left({c}\right)={S}\left({d}\right)\to {c}\left(0\right)={d}\left(0\right)\right)\right)$
57 56 ralrimivva ${⊢}\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\to \forall {c}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {d}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({c}\right)\right|={i}\to \left({S}\left({c}\right)={S}\left({d}\right)\to {c}\left(0\right)={d}\left(0\right)\right)\right)$
58 2fveq3 ${⊢}{c}={a}\to \left|{S}\left({c}\right)\right|=\left|{S}\left({a}\right)\right|$
59 58 eqeq1d ${⊢}{c}={a}\to \left(\left|{S}\left({c}\right)\right|={i}↔\left|{S}\left({a}\right)\right|={i}\right)$
60 fveqeq2 ${⊢}{c}={a}\to \left({S}\left({c}\right)={S}\left({d}\right)↔{S}\left({a}\right)={S}\left({d}\right)\right)$
61 fveq1 ${⊢}{c}={a}\to {c}\left(0\right)={a}\left(0\right)$
62 61 eqeq1d ${⊢}{c}={a}\to \left({c}\left(0\right)={d}\left(0\right)↔{a}\left(0\right)={d}\left(0\right)\right)$
63 60 62 imbi12d ${⊢}{c}={a}\to \left(\left({S}\left({c}\right)={S}\left({d}\right)\to {c}\left(0\right)={d}\left(0\right)\right)↔\left({S}\left({a}\right)={S}\left({d}\right)\to {a}\left(0\right)={d}\left(0\right)\right)\right)$
64 59 63 imbi12d ${⊢}{c}={a}\to \left(\left(\left|{S}\left({c}\right)\right|={i}\to \left({S}\left({c}\right)={S}\left({d}\right)\to {c}\left(0\right)={d}\left(0\right)\right)\right)↔\left(\left|{S}\left({a}\right)\right|={i}\to \left({S}\left({a}\right)={S}\left({d}\right)\to {a}\left(0\right)={d}\left(0\right)\right)\right)\right)$
65 fveq2 ${⊢}{d}={b}\to {S}\left({d}\right)={S}\left({b}\right)$
66 65 eqeq2d ${⊢}{d}={b}\to \left({S}\left({a}\right)={S}\left({d}\right)↔{S}\left({a}\right)={S}\left({b}\right)\right)$
67 fveq1 ${⊢}{d}={b}\to {d}\left(0\right)={b}\left(0\right)$
68 67 eqeq2d ${⊢}{d}={b}\to \left({a}\left(0\right)={d}\left(0\right)↔{a}\left(0\right)={b}\left(0\right)\right)$
69 66 68 imbi12d ${⊢}{d}={b}\to \left(\left({S}\left({a}\right)={S}\left({d}\right)\to {a}\left(0\right)={d}\left(0\right)\right)↔\left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)$
70 69 imbi2d ${⊢}{d}={b}\to \left(\left(\left|{S}\left({a}\right)\right|={i}\to \left({S}\left({a}\right)={S}\left({d}\right)\to {a}\left(0\right)={d}\left(0\right)\right)\right)↔\left(\left|{S}\left({a}\right)\right|={i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)$
71 64 70 cbvral2vw ${⊢}\forall {c}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {d}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({c}\right)\right|={i}\to \left({S}\left({c}\right)={S}\left({d}\right)\to {c}\left(0\right)={d}\left(0\right)\right)\right)↔\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|={i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)$
72 57 71 sylib ${⊢}\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\to \forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|={i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)$
73 72 ancli ${⊢}\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\to \left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|={i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)$
74 35 adantr ${⊢}\left({a}\in \mathrm{dom}{S}\wedge {b}\in \mathrm{dom}{S}\right)\to \left|{S}\left({a}\right)\right|\in {ℕ}_{0}$
75 nn0leltp1 ${⊢}\left(\left|{S}\left({a}\right)\right|\in {ℕ}_{0}\wedge {i}\in {ℕ}_{0}\right)\to \left(\left|{S}\left({a}\right)\right|\le {i}↔\left|{S}\left({a}\right)\right|<{i}+1\right)$
76 nn0re ${⊢}\left|{S}\left({a}\right)\right|\in {ℕ}_{0}\to \left|{S}\left({a}\right)\right|\in ℝ$
77 nn0re ${⊢}{i}\in {ℕ}_{0}\to {i}\in ℝ$
78 leloe ${⊢}\left(\left|{S}\left({a}\right)\right|\in ℝ\wedge {i}\in ℝ\right)\to \left(\left|{S}\left({a}\right)\right|\le {i}↔\left(\left|{S}\left({a}\right)\right|<{i}\vee \left|{S}\left({a}\right)\right|={i}\right)\right)$
79 76 77 78 syl2an ${⊢}\left(\left|{S}\left({a}\right)\right|\in {ℕ}_{0}\wedge {i}\in {ℕ}_{0}\right)\to \left(\left|{S}\left({a}\right)\right|\le {i}↔\left(\left|{S}\left({a}\right)\right|<{i}\vee \left|{S}\left({a}\right)\right|={i}\right)\right)$
80 75 79 bitr3d ${⊢}\left(\left|{S}\left({a}\right)\right|\in {ℕ}_{0}\wedge {i}\in {ℕ}_{0}\right)\to \left(\left|{S}\left({a}\right)\right|<{i}+1↔\left(\left|{S}\left({a}\right)\right|<{i}\vee \left|{S}\left({a}\right)\right|={i}\right)\right)$
81 80 ancoms ${⊢}\left({i}\in {ℕ}_{0}\wedge \left|{S}\left({a}\right)\right|\in {ℕ}_{0}\right)\to \left(\left|{S}\left({a}\right)\right|<{i}+1↔\left(\left|{S}\left({a}\right)\right|<{i}\vee \left|{S}\left({a}\right)\right|={i}\right)\right)$
82 74 81 sylan2 ${⊢}\left({i}\in {ℕ}_{0}\wedge \left({a}\in \mathrm{dom}{S}\wedge {b}\in \mathrm{dom}{S}\right)\right)\to \left(\left|{S}\left({a}\right)\right|<{i}+1↔\left(\left|{S}\left({a}\right)\right|<{i}\vee \left|{S}\left({a}\right)\right|={i}\right)\right)$
83 82 imbi1d ${⊢}\left({i}\in {ℕ}_{0}\wedge \left({a}\in \mathrm{dom}{S}\wedge {b}\in \mathrm{dom}{S}\right)\right)\to \left(\left(\left|{S}\left({a}\right)\right|<{i}+1\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)↔\left(\left(\left|{S}\left({a}\right)\right|<{i}\vee \left|{S}\left({a}\right)\right|={i}\right)\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)$
84 jaob ${⊢}\left(\left(\left|{S}\left({a}\right)\right|<{i}\vee \left|{S}\left({a}\right)\right|={i}\right)\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)↔\left(\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left(\left|{S}\left({a}\right)\right|={i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)$
85 83 84 syl6bb ${⊢}\left({i}\in {ℕ}_{0}\wedge \left({a}\in \mathrm{dom}{S}\wedge {b}\in \mathrm{dom}{S}\right)\right)\to \left(\left(\left|{S}\left({a}\right)\right|<{i}+1\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)↔\left(\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left(\left|{S}\left({a}\right)\right|={i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)\right)$
86 85 2ralbidva ${⊢}{i}\in {ℕ}_{0}\to \left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}+1\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)↔\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left(\left|{S}\left({a}\right)\right|={i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)\right)$
87 r19.26-2 ${⊢}\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \left(\left|{S}\left({a}\right)\right|={i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)↔\left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|={i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)$
88 86 87 syl6bb ${⊢}{i}\in {ℕ}_{0}\to \left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}+1\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)↔\left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\wedge \forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|={i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)\right)$
89 73 88 syl5ibr ${⊢}{i}\in {ℕ}_{0}\to \left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\to \forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<{i}+1\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\right)$
90 22 25 28 31 40 89 nn0ind ${⊢}\left|{S}\left({A}\right)\right|+1\in {ℕ}_{0}\to \forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<\left|{S}\left({A}\right)\right|+1\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)$
91 19 90 syl ${⊢}\left({A}\in \mathrm{dom}{S}\wedge {B}\in \mathrm{dom}{S}\right)\to \forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<\left|{S}\left({A}\right)\right|+1\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)$
92 17 nn0red ${⊢}\left({A}\in \mathrm{dom}{S}\wedge {B}\in \mathrm{dom}{S}\right)\to \left|{S}\left({A}\right)\right|\in ℝ$
93 92 ltp1d ${⊢}\left({A}\in \mathrm{dom}{S}\wedge {B}\in \mathrm{dom}{S}\right)\to \left|{S}\left({A}\right)\right|<\left|{S}\left({A}\right)\right|+1$
94 2fveq3 ${⊢}{a}={A}\to \left|{S}\left({a}\right)\right|=\left|{S}\left({A}\right)\right|$
95 94 breq1d ${⊢}{a}={A}\to \left(\left|{S}\left({a}\right)\right|<\left|{S}\left({A}\right)\right|+1↔\left|{S}\left({A}\right)\right|<\left|{S}\left({A}\right)\right|+1\right)$
96 fveqeq2 ${⊢}{a}={A}\to \left({S}\left({a}\right)={S}\left({b}\right)↔{S}\left({A}\right)={S}\left({b}\right)\right)$
97 fveq1 ${⊢}{a}={A}\to {a}\left(0\right)={A}\left(0\right)$
98 97 eqeq1d ${⊢}{a}={A}\to \left({a}\left(0\right)={b}\left(0\right)↔{A}\left(0\right)={b}\left(0\right)\right)$
99 96 98 imbi12d ${⊢}{a}={A}\to \left(\left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)↔\left({S}\left({A}\right)={S}\left({b}\right)\to {A}\left(0\right)={b}\left(0\right)\right)\right)$
100 95 99 imbi12d ${⊢}{a}={A}\to \left(\left(\left|{S}\left({a}\right)\right|<\left|{S}\left({A}\right)\right|+1\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)↔\left(\left|{S}\left({A}\right)\right|<\left|{S}\left({A}\right)\right|+1\to \left({S}\left({A}\right)={S}\left({b}\right)\to {A}\left(0\right)={b}\left(0\right)\right)\right)\right)$
101 fveq2 ${⊢}{b}={B}\to {S}\left({b}\right)={S}\left({B}\right)$
102 101 eqeq2d ${⊢}{b}={B}\to \left({S}\left({A}\right)={S}\left({b}\right)↔{S}\left({A}\right)={S}\left({B}\right)\right)$
103 fveq1 ${⊢}{b}={B}\to {b}\left(0\right)={B}\left(0\right)$
104 103 eqeq2d ${⊢}{b}={B}\to \left({A}\left(0\right)={b}\left(0\right)↔{A}\left(0\right)={B}\left(0\right)\right)$
105 102 104 imbi12d ${⊢}{b}={B}\to \left(\left({S}\left({A}\right)={S}\left({b}\right)\to {A}\left(0\right)={b}\left(0\right)\right)↔\left({S}\left({A}\right)={S}\left({B}\right)\to {A}\left(0\right)={B}\left(0\right)\right)\right)$
106 105 imbi2d ${⊢}{b}={B}\to \left(\left(\left|{S}\left({A}\right)\right|<\left|{S}\left({A}\right)\right|+1\to \left({S}\left({A}\right)={S}\left({b}\right)\to {A}\left(0\right)={b}\left(0\right)\right)\right)↔\left(\left|{S}\left({A}\right)\right|<\left|{S}\left({A}\right)\right|+1\to \left({S}\left({A}\right)={S}\left({B}\right)\to {A}\left(0\right)={B}\left(0\right)\right)\right)\right)$
107 100 106 rspc2v ${⊢}\left({A}\in \mathrm{dom}{S}\wedge {B}\in \mathrm{dom}{S}\right)\to \left(\forall {a}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\forall {b}\in \mathrm{dom}{S}\phantom{\rule{.4em}{0ex}}\left(\left|{S}\left({a}\right)\right|<\left|{S}\left({A}\right)\right|+1\to \left({S}\left({a}\right)={S}\left({b}\right)\to {a}\left(0\right)={b}\left(0\right)\right)\right)\to \left(\left|{S}\left({A}\right)\right|<\left|{S}\left({A}\right)\right|+1\to \left({S}\left({A}\right)={S}\left({B}\right)\to {A}\left(0\right)={B}\left(0\right)\right)\right)\right)$
108 91 93 107 mp2d ${⊢}\left({A}\in \mathrm{dom}{S}\wedge {B}\in \mathrm{dom}{S}\right)\to \left({S}\left({A}\right)={S}\left({B}\right)\to {A}\left(0\right)={B}\left(0\right)\right)$
109 108 3impia ${⊢}\left({A}\in \mathrm{dom}{S}\wedge {B}\in \mathrm{dom}{S}\wedge {S}\left({A}\right)={S}\left({B}\right)\right)\to {A}\left(0\right)={B}\left(0\right)$