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 ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
efgval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
efgval2.m ⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
efgval2.t ⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
efgred.d ⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
efgred.s ⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
Assertion efgred ( ( 𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )

Proof

Step Hyp Ref Expression
1 efgval.w ⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2 efgval.r ⊢ ∼ = ( ~FG ‘ 𝐼 )
3 efgval2.m ⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
4 efgval2.t ⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
5 efgred.d ⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
6 efgred.s ⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
7 fviss ⊢ ( I ‘ Word ( 𝐼 × 2o ) ) ⊆ Word ( 𝐼 × 2o )
8 1 7 eqsstri ⊢ 𝑊 ⊆ Word ( 𝐼 × 2o )
9 1 2 3 4 5 6 efgsf ⊢ 𝑆 : { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ⟶ 𝑊
10 9 fdmi ⊢ dom 𝑆 = { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) }
11 10 feq2i ⊢ ( 𝑆 : dom 𝑆 ⟶ 𝑊 ↔ 𝑆 : { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ⟶ 𝑊 )
12 9 11 mpbir ⊢ 𝑆 : dom 𝑆 ⟶ 𝑊
13 12 ffvelrni ⊢ ( 𝐴 ∈ dom 𝑆 → ( 𝑆 ‘ 𝐴 ) ∈ 𝑊 )
14 13 adantr ⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆 ) → ( 𝑆 ‘ 𝐴 ) ∈ 𝑊 )
15 8 14 sseldi ⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆 ) → ( 𝑆 ‘ 𝐴 ) ∈ Word ( 𝐼 × 2o ) )
16 lencl ⊢ ( ( 𝑆 ‘ 𝐴 ) ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) ∈ ℕ0 )
17 15 16 syl ⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆 ) → ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) ∈ ℕ0 )
18 peano2nn0 ⊢ ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) ∈ ℕ0 → ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) ∈ ℕ0 )
19 17 18 syl ⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆 ) → ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) ∈ ℕ0 )
20 breq2 ⊢ ( 𝑐 = 0 → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑐 ↔ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 0 ) )
21 20 imbi1d ⊢ ( 𝑐 = 0 → ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑐 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 0 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
22 21 2ralbidv ⊢ ( 𝑐 = 0 → ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑐 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 0 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
23 breq2 ⊢ ( 𝑐 = 𝑖 → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑐 ↔ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 ) )
24 23 imbi1d ⊢ ( 𝑐 = 𝑖 → ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑐 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
25 24 2ralbidv ⊢ ( 𝑐 = 𝑖 → ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑐 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
26 breq2 ⊢ ( 𝑐 = ( 𝑖 + 1 ) → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑐 ↔ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( 𝑖 + 1 ) ) )
27 26 imbi1d ⊢ ( 𝑐 = ( 𝑖 + 1 ) → ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑐 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( 𝑖 + 1 ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
28 27 2ralbidv ⊢ ( 𝑐 = ( 𝑖 + 1 ) → ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑐 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( 𝑖 + 1 ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
29 breq2 ⊢ ( 𝑐 = ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑐 ↔ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) ) )
30 29 imbi1d ⊢ ( 𝑐 = ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) → ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑐 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
31 30 2ralbidv ⊢ ( 𝑐 = ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) → ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑐 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
32 12 ffvelrni ⊢ ( 𝑎 ∈ dom 𝑆 → ( 𝑆 ‘ 𝑎 ) ∈ 𝑊 )
33 8 32 sseldi ⊢ ( 𝑎 ∈ dom 𝑆 → ( 𝑆 ‘ 𝑎 ) ∈ Word ( 𝐼 × 2o ) )
34 lencl ⊢ ( ( 𝑆 ‘ 𝑎 ) ∈ Word ( 𝐼 × 2o ) → ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) ∈ ℕ0 )
35 33 34 syl ⊢ ( 𝑎 ∈ dom 𝑆 → ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) ∈ ℕ0 )
36 nn0nlt0 ⊢ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) ∈ ℕ0 → ¬ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 0 )
37 35 36 syl ⊢ ( 𝑎 ∈ dom 𝑆 → ¬ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 0 )
38 37 pm2.21d ⊢ ( 𝑎 ∈ dom 𝑆 → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 0 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
39 38 adantr ⊢ ( ( 𝑎 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ) → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 0 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
40 39 rgen2 ⊢ ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 0 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) )
41 simpl1 ⊢ ( ( ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆 ) ∧ ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 ∧ ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) ) ) ∧ ¬ ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) → ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
42 simpl3l ⊢ ( ( ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆 ) ∧ ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 ∧ ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) ) ) ∧ ¬ ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) → ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 )
43 breq2 ⊢ ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) ↔ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 ) )
44 43 imbi1d ⊢ ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 → ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
45 44 2ralbidv ⊢ ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 → ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
46 42 45 syl ⊢ ( ( ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆 ) ∧ ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 ∧ ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) ) ) ∧ ¬ ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) → ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
47 41 46 mpbird ⊢ ( ( ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆 ) ∧ ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 ∧ ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) ) ) ∧ ¬ ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) → ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
48 simpl2l ⊢ ( ( ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆 ) ∧ ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 ∧ ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) ) ) ∧ ¬ ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) → 𝑐 ∈ dom 𝑆 )
49 simpl2r ⊢ ( ( ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆 ) ∧ ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 ∧ ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) ) ) ∧ ¬ ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) → 𝑑 ∈ dom 𝑆 )
50 simpl3r ⊢ ( ( ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆 ) ∧ ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 ∧ ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) ) ) ∧ ¬ ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) → ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) )
51 simpr ⊢ ( ( ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆 ) ∧ ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 ∧ ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) ) ) ∧ ¬ ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) → ¬ ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) )
52 1 2 3 4 5 6 47 48 49 50 51 efgredlem ⊢ ¬ ( ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆 ) ∧ ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 ∧ ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) ) ) ∧ ¬ ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) )
53 iman ⊢ ( ( ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆 ) ∧ ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 ∧ ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) ) ) → ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) ↔ ¬ ( ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆 ) ∧ ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 ∧ ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) ) ) ∧ ¬ ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) )
54 52 53 mpbir ⊢ ( ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆 ) ∧ ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 ∧ ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) ) ) → ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) )
55 54 3expia ⊢ ( ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆 ) ) → ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 ∧ ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) ) → ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) )
56 55 expd ⊢ ( ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( 𝑐 ∈ dom 𝑆 ∧ 𝑑 ∈ dom 𝑆 ) ) → ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 → ( ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) → ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) ) )
57 56 ralrimivva ⊢ ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) → ∀ 𝑐 ∈ dom 𝑆 ∀ 𝑑 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 → ( ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) → ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) ) )
58 2fveq3 ⊢ ( 𝑐 = 𝑎 → ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) )
59 58 eqeq1d ⊢ ( 𝑐 = 𝑎 → ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 ↔ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 ) )
60 fveqeq2 ⊢ ( 𝑐 = 𝑎 → ( ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) ↔ ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑑 ) ) )
61 fveq1 ⊢ ( 𝑐 = 𝑎 → ( 𝑐 ‘ 0 ) = ( 𝑎 ‘ 0 ) )
62 61 eqeq1d ⊢ ( 𝑐 = 𝑎 → ( ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ↔ ( 𝑎 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) )
63 60 62 imbi12d ⊢ ( 𝑐 = 𝑎 → ( ( ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) → ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) ↔ ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑑 ) → ( 𝑎 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) ) )
64 59 63 imbi12d ⊢ ( 𝑐 = 𝑎 → ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 → ( ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) → ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑑 ) → ( 𝑎 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) ) ) )
65 fveq2 ⊢ ( 𝑑 = 𝑏 → ( 𝑆 ‘ 𝑑 ) = ( 𝑆 ‘ 𝑏 ) )
66 65 eqeq2d ⊢ ( 𝑑 = 𝑏 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑑 ) ↔ ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) ) )
67 fveq1 ⊢ ( 𝑑 = 𝑏 → ( 𝑑 ‘ 0 ) = ( 𝑏 ‘ 0 ) )
68 67 eqeq2d ⊢ ( 𝑑 = 𝑏 → ( ( 𝑎 ‘ 0 ) = ( 𝑑 ‘ 0 ) ↔ ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) )
69 66 68 imbi12d ⊢ ( 𝑑 = 𝑏 → ( ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑑 ) → ( 𝑎 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) ↔ ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
70 69 imbi2d ⊢ ( 𝑑 = 𝑏 → ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑑 ) → ( 𝑎 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
71 64 70 cbvral2vw ⊢ ( ∀ 𝑐 ∈ dom 𝑆 ∀ 𝑑 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑐 ) ) = 𝑖 → ( ( 𝑆 ‘ 𝑐 ) = ( 𝑆 ‘ 𝑑 ) → ( 𝑐 ‘ 0 ) = ( 𝑑 ‘ 0 ) ) ) ↔ ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
72 57 71 sylib ⊢ ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) → ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
73 72 ancli ⊢ ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) → ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
74 35 adantr ⊢ ( ( 𝑎 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ) → ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) ∈ ℕ0 )
75 nn0leltp1 ⊢ ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) ∈ ℕ0 ∧ 𝑖 ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) ≤ 𝑖 ↔ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( 𝑖 + 1 ) ) )
76 nn0re ⊢ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) ∈ ℕ0 → ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) ∈ ℝ )
77 nn0re ⊢ ( 𝑖 ∈ ℕ0 → 𝑖 ∈ ℝ )
78 leloe ⊢ ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) ∈ ℝ ∧ 𝑖 ∈ ℝ ) → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) ≤ 𝑖 ↔ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 ∨ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 ) ) )
79 76 77 78 syl2an ⊢ ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) ∈ ℕ0 ∧ 𝑖 ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) ≤ 𝑖 ↔ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 ∨ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 ) ) )
80 75 79 bitr3d ⊢ ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) ∈ ℕ0 ∧ 𝑖 ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( 𝑖 + 1 ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 ∨ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 ) ) )
81 80 ancoms ⊢ ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( 𝑖 + 1 ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 ∨ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 ) ) )
82 74 81 sylan2 ⊢ ( ( 𝑖 ∈ ℕ0 ∧ ( 𝑎 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ) ) → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( 𝑖 + 1 ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 ∨ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 ) ) )
83 82 imbi1d ⊢ ( ( 𝑖 ∈ ℕ0 ∧ ( 𝑎 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ) ) → ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( 𝑖 + 1 ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 ∨ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
84 jaob ⊢ ( ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 ∨ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
85 83 84 bitrdi ⊢ ( ( 𝑖 ∈ ℕ0 ∧ ( 𝑎 ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ) ) → ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( 𝑖 + 1 ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) ) )
86 85 2ralbidva ⊢ ( 𝑖 ∈ ℕ0 → ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( 𝑖 + 1 ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) ) )
87 r19.26-2 ⊢ ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) ↔ ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
88 86 87 bitrdi ⊢ ( 𝑖 ∈ ℕ0 → ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( 𝑖 + 1 ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ∧ ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) ) )
89 73 88 syl5ibr ⊢ ( 𝑖 ∈ ℕ0 → ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < 𝑖 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) → ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( 𝑖 + 1 ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
90 22 25 28 31 40 89 nn0ind ⊢ ( ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) ∈ ℕ0 → ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
91 19 90 syl ⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆 ) → ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
92 17 nn0red ⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆 ) → ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) ∈ ℝ )
93 92 ltp1d ⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆 ) → ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) < ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) )
94 2fveq3 ⊢ ( 𝑎 = 𝐴 → ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) = ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) )
95 94 breq1d ⊢ ( 𝑎 = 𝐴 → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) ↔ ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) < ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) ) )
96 fveqeq2 ⊢ ( 𝑎 = 𝐴 → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) ↔ ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝑏 ) ) )
97 fveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ‘ 0 ) = ( 𝐴 ‘ 0 ) )
98 97 eqeq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ↔ ( 𝐴 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) )
99 96 98 imbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ↔ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝐴 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
100 95 99 imbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) < ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) → ( ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝐴 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
101 fveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝑆 ‘ 𝑏 ) = ( 𝑆 ‘ 𝐵 ) )
102 101 eqeq2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝑏 ) ↔ ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) ) )
103 fveq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ‘ 0 ) = ( 𝐵 ‘ 0 ) )
104 103 eqeq2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ‘ 0 ) = ( 𝑏 ‘ 0 ) ↔ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) )
105 102 104 imbi12d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝐴 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ↔ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ) )
106 105 imbi2d ⊢ ( 𝑏 = 𝐵 → ( ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) < ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) → ( ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝐴 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) < ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) → ( ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ) ) )
107 100 106 rspc2v ⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆 ) → ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) → ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) < ( ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) + 1 ) → ( ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) ) ) )
108 91 93 107 mp2d ⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆 ) → ( ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) )
109 108 3impia ⊢ ( ( 𝐴 ∈ dom 𝑆 ∧ 𝐵 ∈ dom 𝑆 ∧ ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )