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 ⊢G=SymGrp⁡D
psgnunilem3.t ⊢T=ran⁡pmTrsp⁡D
psgnunilem3.d ⊢φ→D∈V
psgnunilem3.w1 ⊢φ→W∈WordT
psgnunilem3.l ⊢φ→W=L
psgnunilem3.w2 ⊢φ→W∈ℕ
psgnunilem3.w3 ⊢φ→∑GW=I↾D
psgnunilem3.in ⊢φ→¬∃x∈WordTx=L−2∧∑Gx=I↾D
Assertion psgnunilem3 ⊢¬φ

Proof

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