This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psgnunilem3

Description: Lemma for psgnuni . Any nonempty representation of the identity can be incrementally transformed into a representation two shorter. (Contributed by Stefan O'Rear, 25-Aug-2015)

Ref Expression
Hypotheses psgnunilem3.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
psgnunilem3.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
psgnunilem3.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
psgnunilem3.w1 ⊢ ( 𝜑 → 𝑊 ∈ Word 𝑇 )
psgnunilem3.l ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) = 𝐿 )
psgnunilem3.w2 ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ )
psgnunilem3.w3 ⊢ ( 𝜑 → ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) )
psgnunilem3.in ⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
Assertion psgnunilem3 ¬ 𝜑

Proof

Step Hyp Ref Expression
1 psgnunilem3.g ⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2 psgnunilem3.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
3 psgnunilem3.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
4 psgnunilem3.w1 ⊢ ( 𝜑 → 𝑊 ∈ Word 𝑇 )
5 psgnunilem3.l ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) = 𝐿 )
6 psgnunilem3.w2 ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ )
7 psgnunilem3.w3 ⊢ ( 𝜑 → ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) )
8 psgnunilem3.in ⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
9 5 6 eqeltrrd ⊢ ( 𝜑 → 𝐿 ∈ ℕ )
10 9 nnnn0d ⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
11 wrdf ⊢ ( 𝑊 ∈ Word 𝑇 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑇 )
12 4 11 syl ⊢ ( 𝜑 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑇 )
13 0nn0 ⊢ 0 ∈ ℕ0
14 13 a1i ⊢ ( 𝜑 → 0 ∈ ℕ0 )
15 9 nngt0d ⊢ ( 𝜑 → 0 < 𝐿 )
16 elfzo0 ⊢ ( 0 ∈ ( 0 ..^ 𝐿 ) ↔ ( 0 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ 0 < 𝐿 ) )
17 14 9 15 16 syl3anbrc ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ 𝐿 ) )
18 5 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 𝐿 ) )
19 17 18 eleqtrrd ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
20 12 19 ffvelcdmd ⊢ ( 𝜑 → ( 𝑊 ‘ 0 ) ∈ 𝑇 )
21 eqid ⊢ ( pmTrsp ‘ 𝐷 ) = ( pmTrsp ‘ 𝐷 )
22 21 2 pmtrfmvdn0 ⊢ ( ( 𝑊 ‘ 0 ) ∈ 𝑇 → dom ( ( 𝑊 ‘ 0 ) ∖ I ) ≠ ∅ )
23 20 22 syl ⊢ ( 𝜑 → dom ( ( 𝑊 ‘ 0 ) ∖ I ) ≠ ∅ )
24 n0 ⊢ ( dom ( ( 𝑊 ‘ 0 ) ∖ I ) ≠ ∅ ↔ ∃ 𝑒 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) )
25 23 24 sylib ⊢ ( 𝜑 → ∃ 𝑒 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) )
26 fzonel ⊢ ¬ 𝐿 ∈ ( 0 ..^ 𝐿 )
27 simpr1 ⊢ ( ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝐿 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝐿 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝐿 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) → 𝐿 ∈ ( 0 ..^ 𝐿 ) )
28 26 27 mto ⊢ ¬ ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝐿 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝐿 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝐿 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) )
29 28 a1i ⊢ ( 𝑤 ∈ Word 𝑇 → ¬ ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝐿 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝐿 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝐿 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) )
30 29 nrex ⊢ ¬ ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝐿 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝐿 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝐿 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) )
31 eleq1 ⊢ ( 𝑎 = 0 → ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ↔ 0 ∈ ( 0 ..^ 𝐿 ) ) )
32 fveq2 ⊢ ( 𝑎 = 0 → ( 𝑤 ‘ 𝑎 ) = ( 𝑤 ‘ 0 ) )
33 32 difeq1d ⊢ ( 𝑎 = 0 → ( ( 𝑤 ‘ 𝑎 ) ∖ I ) = ( ( 𝑤 ‘ 0 ) ∖ I ) )
34 33 dmeqd ⊢ ( 𝑎 = 0 → dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) = dom ( ( 𝑤 ‘ 0 ) ∖ I ) )
35 34 eleq2d ⊢ ( 𝑎 = 0 → ( 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ↔ 𝑒 ∈ dom ( ( 𝑤 ‘ 0 ) ∖ I ) ) )
36 oveq2 ⊢ ( 𝑎 = 0 → ( 0 ..^ 𝑎 ) = ( 0 ..^ 0 ) )
37 36 raleqdv ⊢ ( 𝑎 = 0 → ( ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ↔ ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) )
38 31 35 37 3anbi123d ⊢ ( 𝑎 = 0 → ( ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ↔ ( 0 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 0 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) )
39 38 anbi2d ⊢ ( 𝑎 = 0 → ( ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ↔ ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 0 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 0 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) )
40 39 rexbidv ⊢ ( 𝑎 = 0 → ( ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 0 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 0 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) )
41 40 imbi2d ⊢ ( 𝑎 = 0 → ( ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) ↔ ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 0 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 0 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) ) )
42 eleq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ↔ 𝑏 ∈ ( 0 ..^ 𝐿 ) ) )
43 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑤 ‘ 𝑎 ) = ( 𝑤 ‘ 𝑏 ) )
44 43 difeq1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑤 ‘ 𝑎 ) ∖ I ) = ( ( 𝑤 ‘ 𝑏 ) ∖ I ) )
45 44 dmeqd ⊢ ( 𝑎 = 𝑏 → dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) = dom ( ( 𝑤 ‘ 𝑏 ) ∖ I ) )
46 45 eleq2d ⊢ ( 𝑎 = 𝑏 → ( 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ↔ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑏 ) ∖ I ) ) )
47 oveq2 ⊢ ( 𝑎 = 𝑏 → ( 0 ..^ 𝑎 ) = ( 0 ..^ 𝑏 ) )
48 47 raleqdv ⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ↔ ∀ 𝑐 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) )
49 42 46 48 3anbi123d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ↔ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) )
50 49 anbi2d ⊢ ( 𝑎 = 𝑏 → ( ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ↔ ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) )
51 50 rexbidv ⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) )
52 oveq2 ⊢ ( 𝑤 = 𝑥 → ( 𝐺 Σg 𝑤 ) = ( 𝐺 Σg 𝑥 ) )
53 52 eqeq1d ⊢ ( 𝑤 = 𝑥 → ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ↔ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) )
54 fveqeq2 ⊢ ( 𝑤 = 𝑥 → ( ( ♯ ‘ 𝑤 ) = 𝐿 ↔ ( ♯ ‘ 𝑥 ) = 𝐿 ) )
55 53 54 anbi12d ⊢ ( 𝑤 = 𝑥 → ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ↔ ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ) )
56 fveq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ‘ 𝑏 ) = ( 𝑥 ‘ 𝑏 ) )
57 56 difeq1d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ‘ 𝑏 ) ∖ I ) = ( ( 𝑥 ‘ 𝑏 ) ∖ I ) )
58 57 dmeqd ⊢ ( 𝑤 = 𝑥 → dom ( ( 𝑤 ‘ 𝑏 ) ∖ I ) = dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) )
59 58 eleq2d ⊢ ( 𝑤 = 𝑥 → ( 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑏 ) ∖ I ) ↔ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ) )
60 fveq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ‘ 𝑐 ) = ( 𝑥 ‘ 𝑐 ) )
61 60 difeq1d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ‘ 𝑐 ) ∖ I ) = ( ( 𝑥 ‘ 𝑐 ) ∖ I ) )
62 61 dmeqd ⊢ ( 𝑤 = 𝑥 → dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) = dom ( ( 𝑥 ‘ 𝑐 ) ∖ I ) )
63 62 eleq2d ⊢ ( 𝑤 = 𝑥 → ( 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ↔ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑐 ) ∖ I ) ) )
64 63 notbid ⊢ ( 𝑤 = 𝑥 → ( ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ↔ ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑐 ) ∖ I ) ) )
65 64 ralbidv ⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑐 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ↔ ∀ 𝑐 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑐 ) ∖ I ) ) )
66 fveq2 ⊢ ( 𝑐 = 𝑑 → ( 𝑥 ‘ 𝑐 ) = ( 𝑥 ‘ 𝑑 ) )
67 66 difeq1d ⊢ ( 𝑐 = 𝑑 → ( ( 𝑥 ‘ 𝑐 ) ∖ I ) = ( ( 𝑥 ‘ 𝑑 ) ∖ I ) )
68 67 dmeqd ⊢ ( 𝑐 = 𝑑 → dom ( ( 𝑥 ‘ 𝑐 ) ∖ I ) = dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) )
69 68 eleq2d ⊢ ( 𝑐 = 𝑑 → ( 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑐 ) ∖ I ) ↔ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) )
70 69 notbid ⊢ ( 𝑐 = 𝑑 → ( ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑐 ) ∖ I ) ↔ ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) )
71 70 cbvralvw ⊢ ( ∀ 𝑐 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑐 ) ∖ I ) ↔ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) )
72 65 71 bitrdi ⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑐 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ↔ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) )
73 59 72 3anbi23d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ↔ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) )
74 55 73 anbi12d ⊢ ( 𝑤 = 𝑥 → ( ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ↔ ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) ) )
75 74 cbvrexvw ⊢ ( ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ↔ ∃ 𝑥 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) )
76 51 75 bitrdi ⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ↔ ∃ 𝑥 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) ) )
77 76 imbi2d ⊢ ( 𝑎 = 𝑏 → ( ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) ↔ ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ∃ 𝑥 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) ) ) )
78 eleq1 ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ↔ ( 𝑏 + 1 ) ∈ ( 0 ..^ 𝐿 ) ) )
79 fveq2 ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝑤 ‘ 𝑎 ) = ( 𝑤 ‘ ( 𝑏 + 1 ) ) )
80 79 difeq1d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝑤 ‘ 𝑎 ) ∖ I ) = ( ( 𝑤 ‘ ( 𝑏 + 1 ) ) ∖ I ) )
81 80 dmeqd ⊢ ( 𝑎 = ( 𝑏 + 1 ) → dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) = dom ( ( 𝑤 ‘ ( 𝑏 + 1 ) ) ∖ I ) )
82 81 eleq2d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ↔ 𝑒 ∈ dom ( ( 𝑤 ‘ ( 𝑏 + 1 ) ) ∖ I ) ) )
83 oveq2 ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 0 ..^ 𝑎 ) = ( 0 ..^ ( 𝑏 + 1 ) ) )
84 83 raleqdv ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ↔ ∀ 𝑐 ∈ ( 0 ..^ ( 𝑏 + 1 ) ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) )
85 78 82 84 3anbi123d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ↔ ( ( 𝑏 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ ( 𝑏 + 1 ) ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ ( 𝑏 + 1 ) ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) )
86 85 anbi2d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ↔ ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝑏 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ ( 𝑏 + 1 ) ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ ( 𝑏 + 1 ) ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) )
87 86 rexbidv ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝑏 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ ( 𝑏 + 1 ) ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ ( 𝑏 + 1 ) ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) )
88 87 imbi2d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) ↔ ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝑏 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ ( 𝑏 + 1 ) ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ ( 𝑏 + 1 ) ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) ) )
89 eleq1 ⊢ ( 𝑎 = 𝐿 → ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ↔ 𝐿 ∈ ( 0 ..^ 𝐿 ) ) )
90 fveq2 ⊢ ( 𝑎 = 𝐿 → ( 𝑤 ‘ 𝑎 ) = ( 𝑤 ‘ 𝐿 ) )
91 90 difeq1d ⊢ ( 𝑎 = 𝐿 → ( ( 𝑤 ‘ 𝑎 ) ∖ I ) = ( ( 𝑤 ‘ 𝐿 ) ∖ I ) )
92 91 dmeqd ⊢ ( 𝑎 = 𝐿 → dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) = dom ( ( 𝑤 ‘ 𝐿 ) ∖ I ) )
93 92 eleq2d ⊢ ( 𝑎 = 𝐿 → ( 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ↔ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝐿 ) ∖ I ) ) )
94 oveq2 ⊢ ( 𝑎 = 𝐿 → ( 0 ..^ 𝑎 ) = ( 0 ..^ 𝐿 ) )
95 94 raleqdv ⊢ ( 𝑎 = 𝐿 → ( ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ↔ ∀ 𝑐 ∈ ( 0 ..^ 𝐿 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) )
96 89 93 95 3anbi123d ⊢ ( 𝑎 = 𝐿 → ( ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ↔ ( 𝐿 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝐿 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝐿 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) )
97 96 anbi2d ⊢ ( 𝑎 = 𝐿 → ( ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ↔ ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝐿 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝐿 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝐿 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) )
98 97 rexbidv ⊢ ( 𝑎 = 𝐿 → ( ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ↔ ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝐿 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝐿 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝐿 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) )
99 98 imbi2d ⊢ ( 𝑎 = 𝐿 → ( ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝑎 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑎 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝑎 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) ↔ ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝐿 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝐿 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝐿 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) ) )
100 4 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → 𝑊 ∈ Word 𝑇 )
101 7 5 jca ⊢ ( 𝜑 → ( ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑊 ) = 𝐿 ) )
102 101 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ( ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑊 ) = 𝐿 ) )
103 17 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → 0 ∈ ( 0 ..^ 𝐿 ) )
104 simpr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) )
105 ral0 ⊢ ∀ 𝑐 ∈ ∅ ¬ 𝑒 ∈ dom ( ( 𝑊 ‘ 𝑐 ) ∖ I )
106 fzo0 ⊢ ( 0 ..^ 0 ) = ∅
107 106 raleqi ⊢ ( ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑊 ‘ 𝑐 ) ∖ I ) ↔ ∀ 𝑐 ∈ ∅ ¬ 𝑒 ∈ dom ( ( 𝑊 ‘ 𝑐 ) ∖ I ) )
108 105 107 mpbir ⊢ ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑊 ‘ 𝑐 ) ∖ I )
109 108 a1i ⊢ ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑊 ‘ 𝑐 ) ∖ I ) )
110 103 104 109 3jca ⊢ ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ( 0 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑊 ‘ 𝑐 ) ∖ I ) ) )
111 oveq2 ⊢ ( 𝑤 = 𝑊 → ( 𝐺 Σg 𝑤 ) = ( 𝐺 Σg 𝑊 ) )
112 111 eqeq1d ⊢ ( 𝑤 = 𝑊 → ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ↔ ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) ) )
113 fveqeq2 ⊢ ( 𝑤 = 𝑊 → ( ( ♯ ‘ 𝑤 ) = 𝐿 ↔ ( ♯ ‘ 𝑊 ) = 𝐿 ) )
114 112 113 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ↔ ( ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑊 ) = 𝐿 ) ) )
115 fveq1 ⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ 0 ) = ( 𝑊 ‘ 0 ) )
116 115 difeq1d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 ‘ 0 ) ∖ I ) = ( ( 𝑊 ‘ 0 ) ∖ I ) )
117 116 dmeqd ⊢ ( 𝑤 = 𝑊 → dom ( ( 𝑤 ‘ 0 ) ∖ I ) = dom ( ( 𝑊 ‘ 0 ) ∖ I ) )
118 117 eleq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑒 ∈ dom ( ( 𝑤 ‘ 0 ) ∖ I ) ↔ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) )
119 fveq1 ⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ 𝑐 ) = ( 𝑊 ‘ 𝑐 ) )
120 119 difeq1d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑤 ‘ 𝑐 ) ∖ I ) = ( ( 𝑊 ‘ 𝑐 ) ∖ I ) )
121 120 dmeqd ⊢ ( 𝑤 = 𝑊 → dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) = dom ( ( 𝑊 ‘ 𝑐 ) ∖ I ) )
122 121 eleq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ↔ 𝑒 ∈ dom ( ( 𝑊 ‘ 𝑐 ) ∖ I ) ) )
123 122 notbid ⊢ ( 𝑤 = 𝑊 → ( ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ↔ ¬ 𝑒 ∈ dom ( ( 𝑊 ‘ 𝑐 ) ∖ I ) ) )
124 123 ralbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ↔ ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑊 ‘ 𝑐 ) ∖ I ) ) )
125 118 124 3anbi23d ⊢ ( 𝑤 = 𝑊 → ( ( 0 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 0 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ↔ ( 0 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑊 ‘ 𝑐 ) ∖ I ) ) ) )
126 114 125 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 0 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 0 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ↔ ( ( ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑊 ) = 𝐿 ) ∧ ( 0 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑊 ‘ 𝑐 ) ∖ I ) ) ) ) )
127 126 rspcev ⊢ ( ( 𝑊 ∈ Word 𝑇 ∧ ( ( ( 𝐺 Σg 𝑊 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑊 ) = 𝐿 ) ∧ ( 0 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑊 ‘ 𝑐 ) ∖ I ) ) ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 0 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 0 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) )
128 100 102 110 127 syl12anc ⊢ ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 0 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 0 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 0 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) )
129 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) ) ) → 𝐷 ∈ 𝑉 )
130 simprl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) ) ) → 𝑥 ∈ Word 𝑇 )
131 simpll ⊢ ( ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) → ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) )
132 131 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) ) ) → ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) )
133 simplr ⊢ ( ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) → ( ♯ ‘ 𝑥 ) = 𝐿 )
134 133 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) ) ) → ( ♯ ‘ 𝑥 ) = 𝐿 )
135 simpr1 ⊢ ( ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) → 𝑏 ∈ ( 0 ..^ 𝐿 ) )
136 135 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) ) ) → 𝑏 ∈ ( 0 ..^ 𝐿 ) )
137 simpr2 ⊢ ( ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) → 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) )
138 137 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) ) ) → 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) )
139 simpr3 ⊢ ( ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) → ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) )
140 139 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) ) ) → ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) )
141 fveqeq2 ⊢ ( 𝑥 = 𝑦 → ( ( ♯ ‘ 𝑥 ) = ( 𝐿 − 2 ) ↔ ( ♯ ‘ 𝑦 ) = ( 𝐿 − 2 ) ) )
142 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐺 Σg 𝑥 ) = ( 𝐺 Σg 𝑦 ) )
143 142 eqeq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ↔ ( 𝐺 Σg 𝑦 ) = ( I ↾ 𝐷 ) ) )
144 141 143 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( ♯ ‘ 𝑥 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ↔ ( ( ♯ ‘ 𝑦 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑦 ) = ( I ↾ 𝐷 ) ) ) )
145 144 cbvrexvw ⊢ ( ∃ 𝑥 ∈ Word 𝑇 ( ( ♯ ‘ 𝑥 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ) ↔ ∃ 𝑦 ∈ Word 𝑇 ( ( ♯ ‘ 𝑦 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑦 ) = ( I ↾ 𝐷 ) ) )
146 8 145 sylnib ⊢ ( 𝜑 → ¬ ∃ 𝑦 ∈ Word 𝑇 ( ( ♯ ‘ 𝑦 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑦 ) = ( I ↾ 𝐷 ) ) )
147 146 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) ) ) → ¬ ∃ 𝑦 ∈ Word 𝑇 ( ( ♯ ‘ 𝑦 ) = ( 𝐿 − 2 ) ∧ ( 𝐺 Σg 𝑦 ) = ( I ↾ 𝐷 ) ) )
148 1 2 129 130 132 134 136 138 140 147 psgnunilem2 ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) ∧ ( 𝑥 ∈ Word 𝑇 ∧ ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝑏 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ ( 𝑏 + 1 ) ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ ( 𝑏 + 1 ) ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) )
149 148 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ( ∃ 𝑥 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝑏 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ ( 𝑏 + 1 ) ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ ( 𝑏 + 1 ) ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) )
150 149 a2i ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ∃ 𝑥 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) ) → ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝑏 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ ( 𝑏 + 1 ) ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ ( 𝑏 + 1 ) ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) )
151 150 a1i ⊢ ( 𝑏 ∈ ℕ0 → ( ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ∃ 𝑥 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑥 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑥 ) = 𝐿 ) ∧ ( 𝑏 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑏 ) ∖ I ) ∧ ∀ 𝑑 ∈ ( 0 ..^ 𝑏 ) ¬ 𝑒 ∈ dom ( ( 𝑥 ‘ 𝑑 ) ∖ I ) ) ) ) → ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( ( 𝑏 + 1 ) ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ ( 𝑏 + 1 ) ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ ( 𝑏 + 1 ) ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) ) )
152 41 77 88 99 128 151 nn0ind ⊢ ( 𝐿 ∈ ℕ0 → ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ∃ 𝑤 ∈ Word 𝑇 ( ( ( 𝐺 Σg 𝑤 ) = ( I ↾ 𝐷 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐿 ) ∧ ( 𝐿 ∈ ( 0 ..^ 𝐿 ) ∧ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝐿 ) ∖ I ) ∧ ∀ 𝑐 ∈ ( 0 ..^ 𝐿 ) ¬ 𝑒 ∈ dom ( ( 𝑤 ‘ 𝑐 ) ∖ I ) ) ) ) )
153 30 152 mtoi ⊢ ( 𝐿 ∈ ℕ0 → ¬ ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) )
154 153 con2i ⊢ ( ( 𝜑 ∧ 𝑒 ∈ dom ( ( 𝑊 ‘ 0 ) ∖ I ) ) → ¬ 𝐿 ∈ ℕ0 )
155 25 154 exlimddv ⊢ ( 𝜑 → ¬ 𝐿 ∈ ℕ0 )
156 10 155 pm2.65i ⊢ ¬ 𝜑