Theorem psgnunilem3 17739

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

Hypotheses

Ref	Expression
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

Ref	Expression
psgnunilem3	⊢ ¬ 𝜑

Distinct variable groups:   𝑥,𝐷   𝑥,𝐺   𝑥,𝐿   𝑥,𝑇   𝑥,𝑊   𝜑,𝑥

Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem psgnunilem3

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑤 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		psgnunilem3.l	. . . 4 ⊢ (𝜑 → (#‘𝑊) = 𝐿)
2		psgnunilem3.w2	. . . 4 ⊢ (𝜑 → (#‘𝑊) ∈ ℕ)
3	1, 2	eqeltrrd 2689	. . 3 ⊢ (𝜑 → 𝐿 ∈ ℕ)
4	3	nnnn0d 11228	. 2 ⊢ (𝜑 → 𝐿 ∈ ℕ0)
5		psgnunilem3.w1	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ Word 𝑇)
6		wrdf 13165	. . . . . . 7 ⊢ (𝑊 ∈ Word 𝑇 → 𝑊:(0..^(#‘𝑊))⟶𝑇)
7	5, 6	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑊:(0..^(#‘𝑊))⟶𝑇)
8		0nn0 11184	. . . . . . . . 9 ⊢ 0 ∈ ℕ0
9	8	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℕ0)
10	3	nngt0d 10941	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝐿)
11		elfzo0 12376	. . . . . . . 8 ⊢ (0 ∈ (0..^𝐿) ↔ (0 ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ 0 < 𝐿))
12	9, 3, 10, 11	syl3anbrc 1239	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0..^𝐿))
13	1	oveq2d 6565	. . . . . . 7 ⊢ (𝜑 → (0..^(#‘𝑊)) = (0..^𝐿))
14	12, 13	eleqtrrd 2691	. . . . . 6 ⊢ (𝜑 → 0 ∈ (0..^(#‘𝑊)))
15	7, 14	ffvelrnd 6268	. . . . 5 ⊢ (𝜑 → (𝑊‘0) ∈ 𝑇)
16		eqid 2610	. . . . . 6 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
17		psgnunilem3.t	. . . . . 6 ⊢ 𝑇 = ran (pmTrsp‘𝐷)
18	16, 17	pmtrfmvdn0 17705	. . . . 5 ⊢ ((𝑊‘0) ∈ 𝑇 → dom ((𝑊‘0) ∖ I ) ≠ ∅)
19	15, 18	syl 17	. . . 4 ⊢ (𝜑 → dom ((𝑊‘0) ∖ I ) ≠ ∅)
20		n0 3890	. . . 4 ⊢ (dom ((𝑊‘0) ∖ I ) ≠ ∅ ↔ ∃𝑒 𝑒 ∈ dom ((𝑊‘0) ∖ I ))
21	19, 20	sylib 207	. . 3 ⊢ (𝜑 → ∃𝑒 𝑒 ∈ dom ((𝑊‘0) ∖ I ))
22		fzonel 12352	. . . . . . . 8 ⊢ ¬ 𝐿 ∈ (0..^𝐿)
23		simpr1 1060	. . . . . . . 8 ⊢ ((((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝐿) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝐿) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))) → 𝐿 ∈ (0..^𝐿))
24	22, 23	mto 187	. . . . . . 7 ⊢ ¬ (((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝐿) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝐿) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))
25	24	a1i 11	. . . . . 6 ⊢ (𝑤 ∈ Word 𝑇 → ¬ (((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝐿) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝐿) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))))
26	25	nrex 2983	. . . . 5 ⊢ ¬ ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝐿) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝐿) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))
27		eleq1 2676	. . . . . . . . . 10 ⊢ (𝑎 = 0 → (𝑎 ∈ (0..^𝐿) ↔ 0 ∈ (0..^𝐿)))
28		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑎 = 0 → (𝑤‘𝑎) = (𝑤‘0))
29	28	difeq1d 3689	. . . . . . . . . . . 12 ⊢ (𝑎 = 0 → ((𝑤‘𝑎) ∖ I ) = ((𝑤‘0) ∖ I ))
30	29	dmeqd 5248	. . . . . . . . . . 11 ⊢ (𝑎 = 0 → dom ((𝑤‘𝑎) ∖ I ) = dom ((𝑤‘0) ∖ I ))
31	30	eleq2d 2673	. . . . . . . . . 10 ⊢ (𝑎 = 0 → (𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ↔ 𝑒 ∈ dom ((𝑤‘0) ∖ I )))
32		oveq2 6557	. . . . . . . . . . 11 ⊢ (𝑎 = 0 → (0..^𝑎) = (0..^0))
33	32	raleqdv 3121	. . . . . . . . . 10 ⊢ (𝑎 = 0 → (∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ) ↔ ∀𝑐 ∈ (0..^0) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))
34	27, 31, 33	3anbi123d 1391	. . . . . . . . 9 ⊢ (𝑎 = 0 → ((𝑎 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )) ↔ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘0) ∖ I ) ∧ ∀𝑐 ∈ (0..^0) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))))
35	34	anbi2d 736	. . . . . . . 8 ⊢ (𝑎 = 0 → ((((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝑎 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))) ↔ (((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘0) ∖ I ) ∧ ∀𝑐 ∈ (0..^0) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))))
36	35	rexbidv 3034	. . . . . . 7 ⊢ (𝑎 = 0 → (∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝑎 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))) ↔ ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘0) ∖ I ) ∧ ∀𝑐 ∈ (0..^0) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))))
37	36	imbi2d 329	. . . . . 6 ⊢ (𝑎 = 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 ))))))
38		eleq1 2676	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → (𝑎 ∈ (0..^𝐿) ↔ 𝑏 ∈ (0..^𝐿)))
39		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → (𝑤‘𝑎) = (𝑤‘𝑏))
40	39	difeq1d 3689	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑏 → ((𝑤‘𝑎) ∖ I ) = ((𝑤‘𝑏) ∖ I ))
41	40	dmeqd 5248	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑏 → dom ((𝑤‘𝑎) ∖ I ) = dom ((𝑤‘𝑏) ∖ I ))
42	41	eleq2d 2673	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → (𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ↔ 𝑒 ∈ dom ((𝑤‘𝑏) ∖ I )))
43		oveq2 6557	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑏 → (0..^𝑎) = (0..^𝑏))
44	43	raleqdv 3121	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → (∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ) ↔ ∀𝑐 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))
45	38, 42, 44	3anbi123d 1391	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → ((𝑎 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )) ↔ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑏) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))))
46	45	anbi2d 736	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → ((((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝑎 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))) ↔ (((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑏) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))))
47	46	rexbidv 3034	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝑎 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))) ↔ ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑏) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))))
48		oveq2 6557	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑥 → (𝐺 Σg 𝑤) = (𝐺 Σg 𝑥))
49	48	eqeq1d 2612	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑥 → ((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ↔ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
50		fveq2 6103	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑥 → (#‘𝑤) = (#‘𝑥))
51	50	eqeq1d 2612	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑥 → ((#‘𝑤) = 𝐿 ↔ (#‘𝑥) = 𝐿))
52	49, 51	anbi12d 743	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → (((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ↔ ((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿)))
53		fveq1 6102	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → (𝑤‘𝑏) = (𝑥‘𝑏))
54	53	difeq1d 3689	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → ((𝑤‘𝑏) ∖ I ) = ((𝑥‘𝑏) ∖ I ))
55	54	dmeqd 5248	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑥 → dom ((𝑤‘𝑏) ∖ I ) = dom ((𝑥‘𝑏) ∖ I ))
56	55	eleq2d 2673	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑥 → (𝑒 ∈ dom ((𝑤‘𝑏) ∖ I ) ↔ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I )))
57		fveq1 6102	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑥 → (𝑤‘𝑐) = (𝑥‘𝑐))
58	57	difeq1d 3689	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑥 → ((𝑤‘𝑐) ∖ I ) = ((𝑥‘𝑐) ∖ I ))
59	58	dmeqd 5248	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑥 → dom ((𝑤‘𝑐) ∖ I ) = dom ((𝑥‘𝑐) ∖ I ))
60	59	eleq2d 2673	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → (𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ) ↔ 𝑒 ∈ dom ((𝑥‘𝑐) ∖ I )))
61	60	notbid 307	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → (¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ) ↔ ¬ 𝑒 ∈ dom ((𝑥‘𝑐) ∖ I )))
62	61	ralbidv 2969	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑥 → (∀𝑐 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ) ↔ ∀𝑐 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑐) ∖ I )))
63		fveq2 6103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑑 → (𝑥‘𝑐) = (𝑥‘𝑑))
64	63	difeq1d 3689	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑑 → ((𝑥‘𝑐) ∖ I ) = ((𝑥‘𝑑) ∖ I ))
65	64	dmeqd 5248	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑑 → dom ((𝑥‘𝑐) ∖ I ) = dom ((𝑥‘𝑑) ∖ I ))
66	65	eleq2d 2673	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑑 → (𝑒 ∈ dom ((𝑥‘𝑐) ∖ I ) ↔ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I )))
67	66	notbid 307	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑑 → (¬ 𝑒 ∈ dom ((𝑥‘𝑐) ∖ I ) ↔ ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I )))
68	67	cbvralv 3147	. . . . . . . . . . . 12 ⊢ (∀𝑐 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑐) ∖ I ) ↔ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))
69	62, 68	syl6bb 275	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑥 → (∀𝑐 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ) ↔ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I )))
70	56, 69	3anbi23d 1394	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → ((𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑏) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )) ↔ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))))
71	52, 70	anbi12d 743	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → ((((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑏) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))) ↔ (((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I )))))
72	71	cbvrexv 3148	. . . . . . . 8 ⊢ (∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑏) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))) ↔ ∃𝑥 ∈ Word 𝑇(((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))))
73	47, 72	syl6bb 275	. . . . . . 7 ⊢ (𝑎 = 𝑏 → (∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝑎 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))) ↔ ∃𝑥 ∈ Word 𝑇(((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I )))))
74	73	imbi2d 329	. . . . . 6 ⊢ (𝑎 = 𝑏 → (((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝑎 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))) ↔ ((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) → ∃𝑥 ∈ Word 𝑇(((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))))))
75		eleq1 2676	. . . . . . . . . 10 ⊢ (𝑎 = (𝑏 + 1) → (𝑎 ∈ (0..^𝐿) ↔ (𝑏 + 1) ∈ (0..^𝐿)))
76		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝑏 + 1) → (𝑤‘𝑎) = (𝑤‘(𝑏 + 1)))
77	76	difeq1d 3689	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑏 + 1) → ((𝑤‘𝑎) ∖ I ) = ((𝑤‘(𝑏 + 1)) ∖ I ))
78	77	dmeqd 5248	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑏 + 1) → dom ((𝑤‘𝑎) ∖ I ) = dom ((𝑤‘(𝑏 + 1)) ∖ I ))
79	78	eleq2d 2673	. . . . . . . . . 10 ⊢ (𝑎 = (𝑏 + 1) → (𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ↔ 𝑒 ∈ dom ((𝑤‘(𝑏 + 1)) ∖ I )))
80		oveq2 6557	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑏 + 1) → (0..^𝑎) = (0..^(𝑏 + 1)))
81	80	raleqdv 3121	. . . . . . . . . 10 ⊢ (𝑎 = (𝑏 + 1) → (∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ) ↔ ∀𝑐 ∈ (0..^(𝑏 + 1)) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))
82	75, 79, 81	3anbi123d 1391	. . . . . . . . 9 ⊢ (𝑎 = (𝑏 + 1) → ((𝑎 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )) ↔ ((𝑏 + 1) ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘(𝑏 + 1)) ∖ I ) ∧ ∀𝑐 ∈ (0..^(𝑏 + 1)) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))))
83	82	anbi2d 736	. . . . . . . 8 ⊢ (𝑎 = (𝑏 + 1) → ((((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝑎 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))) ↔ (((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝑏 + 1) ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘(𝑏 + 1)) ∖ I ) ∧ ∀𝑐 ∈ (0..^(𝑏 + 1)) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))))
84	83	rexbidv 3034	. . . . . . 7 ⊢ (𝑎 = (𝑏 + 1) → (∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝑎 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))) ↔ ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝑏 + 1) ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘(𝑏 + 1)) ∖ I ) ∧ ∀𝑐 ∈ (0..^(𝑏 + 1)) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))))
85	84	imbi2d 329	. . . . . 6 ⊢ (𝑎 = (𝑏 + 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 ))))))
86		eleq1 2676	. . . . . . . . . 10 ⊢ (𝑎 = 𝐿 → (𝑎 ∈ (0..^𝐿) ↔ 𝐿 ∈ (0..^𝐿)))
87		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝐿 → (𝑤‘𝑎) = (𝑤‘𝐿))
88	87	difeq1d 3689	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝐿 → ((𝑤‘𝑎) ∖ I ) = ((𝑤‘𝐿) ∖ I ))
89	88	dmeqd 5248	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐿 → dom ((𝑤‘𝑎) ∖ I ) = dom ((𝑤‘𝐿) ∖ I ))
90	89	eleq2d 2673	. . . . . . . . . 10 ⊢ (𝑎 = 𝐿 → (𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ↔ 𝑒 ∈ dom ((𝑤‘𝐿) ∖ I )))
91		oveq2 6557	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐿 → (0..^𝑎) = (0..^𝐿))
92	91	raleqdv 3121	. . . . . . . . . 10 ⊢ (𝑎 = 𝐿 → (∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ) ↔ ∀𝑐 ∈ (0..^𝐿) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))
93	86, 90, 92	3anbi123d 1391	. . . . . . . . 9 ⊢ (𝑎 = 𝐿 → ((𝑎 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )) ↔ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝐿) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝐿) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))))
94	93	anbi2d 736	. . . . . . . 8 ⊢ (𝑎 = 𝐿 → ((((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝑎 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))) ↔ (((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝐿) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝐿) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))))
95	94	rexbidv 3034	. . . . . . 7 ⊢ (𝑎 = 𝐿 → (∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝑎 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))) ↔ ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝐿) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝐿) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))))
96	95	imbi2d 329	. . . . . 6 ⊢ (𝑎 = 𝐿 → (((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝑎 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝑎) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝑎) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))) ↔ ((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝐿) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝐿) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))))))
97	5	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) → 𝑊 ∈ Word 𝑇)
98		psgnunilem3.w3	. . . . . . . . 9 ⊢ (𝜑 → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))
99	98, 1	jca 553	. . . . . . . 8 ⊢ (𝜑 → ((𝐺 Σg 𝑊) = ( I ↾ 𝐷) ∧ (#‘𝑊) = 𝐿))
100	99	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) → ((𝐺 Σg 𝑊) = ( I ↾ 𝐷) ∧ (#‘𝑊) = 𝐿))
101	12	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) → 0 ∈ (0..^𝐿))
102		simpr 476	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) → 𝑒 ∈ dom ((𝑊‘0) ∖ I ))
103		ral0 4028	. . . . . . . . . 10 ⊢ ∀𝑐 ∈ ∅ ¬ 𝑒 ∈ dom ((𝑊‘𝑐) ∖ I )
104		fzo0 12361	. . . . . . . . . . 11 ⊢ (0..^0) = ∅
105	104	raleqi 3119	. . . . . . . . . 10 ⊢ (∀𝑐 ∈ (0..^0) ¬ 𝑒 ∈ dom ((𝑊‘𝑐) ∖ I ) ↔ ∀𝑐 ∈ ∅ ¬ 𝑒 ∈ dom ((𝑊‘𝑐) ∖ I ))
106	103, 105	mpbir 220	. . . . . . . . 9 ⊢ ∀𝑐 ∈ (0..^0) ¬ 𝑒 ∈ dom ((𝑊‘𝑐) ∖ I )
107	106	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) → ∀𝑐 ∈ (0..^0) ¬ 𝑒 ∈ dom ((𝑊‘𝑐) ∖ I ))
108	101, 102, 107	3jca 1235	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) → (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I ) ∧ ∀𝑐 ∈ (0..^0) ¬ 𝑒 ∈ dom ((𝑊‘𝑐) ∖ I )))
109		oveq2 6557	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (𝐺 Σg 𝑤) = (𝐺 Σg 𝑊))
110	109	eqeq1d 2612	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ↔ (𝐺 Σg 𝑊) = ( I ↾ 𝐷)))
111		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (#‘𝑤) = (#‘𝑊))
112	111	eqeq1d 2612	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → ((#‘𝑤) = 𝐿 ↔ (#‘𝑊) = 𝐿))
113	110, 112	anbi12d 743	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → (((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ↔ ((𝐺 Σg 𝑊) = ( I ↾ 𝐷) ∧ (#‘𝑊) = 𝐿)))
114		fveq1 6102	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑊 → (𝑤‘0) = (𝑊‘0))
115	114	difeq1d 3689	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → ((𝑤‘0) ∖ I ) = ((𝑊‘0) ∖ I ))
116	115	dmeqd 5248	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → dom ((𝑤‘0) ∖ I ) = dom ((𝑊‘0) ∖ I ))
117	116	eleq2d 2673	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (𝑒 ∈ dom ((𝑤‘0) ∖ I ) ↔ 𝑒 ∈ dom ((𝑊‘0) ∖ I )))
118		fveq1 6102	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑊 → (𝑤‘𝑐) = (𝑊‘𝑐))
119	118	difeq1d 3689	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑊 → ((𝑤‘𝑐) ∖ I ) = ((𝑊‘𝑐) ∖ I ))
120	119	dmeqd 5248	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑊 → dom ((𝑤‘𝑐) ∖ I ) = dom ((𝑊‘𝑐) ∖ I ))
121	120	eleq2d 2673	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑊 → (𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ) ↔ 𝑒 ∈ dom ((𝑊‘𝑐) ∖ I )))
122	121	notbid 307	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑊 → (¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ) ↔ ¬ 𝑒 ∈ dom ((𝑊‘𝑐) ∖ I )))
123	122	ralbidv 2969	. . . . . . . . . 10 ⊢ (𝑤 = 𝑊 → (∀𝑐 ∈ (0..^0) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ) ↔ ∀𝑐 ∈ (0..^0) ¬ 𝑒 ∈ dom ((𝑊‘𝑐) ∖ I )))
124	117, 123	3anbi23d 1394	. . . . . . . . 9 ⊢ (𝑤 = 𝑊 → ((0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘0) ∖ I ) ∧ ∀𝑐 ∈ (0..^0) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )) ↔ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I ) ∧ ∀𝑐 ∈ (0..^0) ¬ 𝑒 ∈ dom ((𝑊‘𝑐) ∖ I ))))
125	113, 124	anbi12d 743	. . . . . . . 8 ⊢ (𝑤 = 𝑊 → ((((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘0) ∖ I ) ∧ ∀𝑐 ∈ (0..^0) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))) ↔ (((𝐺 Σg 𝑊) = ( I ↾ 𝐷) ∧ (#‘𝑊) = 𝐿) ∧ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I ) ∧ ∀𝑐 ∈ (0..^0) ¬ 𝑒 ∈ dom ((𝑊‘𝑐) ∖ I )))))
126	125	rspcev 3282	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑇 ∧ (((𝐺 Σg 𝑊) = ( I ↾ 𝐷) ∧ (#‘𝑊) = 𝐿) ∧ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I ) ∧ ∀𝑐 ∈ (0..^0) ¬ 𝑒 ∈ dom ((𝑊‘𝑐) ∖ I )))) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘0) ∖ I ) ∧ ∀𝑐 ∈ (0..^0) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))))
127	97, 100, 108, 126	syl12anc 1316	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (0 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘0) ∖ I ) ∧ ∀𝑐 ∈ (0..^0) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))))
128		psgnunilem3.g	. . . . . . . . . 10 ⊢ 𝐺 = (SymGrp‘𝐷)
129		psgnunilem3.d	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ 𝑉)
130	129	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) ∧ (𝑥 ∈ Word 𝑇 ∧ (((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))))) → 𝐷 ∈ 𝑉)
131		simprl 790	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) ∧ (𝑥 ∈ Word 𝑇 ∧ (((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))))) → 𝑥 ∈ Word 𝑇)
132		simpll 786	. . . . . . . . . . 11 ⊢ ((((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))) → (𝐺 Σg 𝑥) = ( I ↾ 𝐷))
133	132	ad2antll 761	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) ∧ (𝑥 ∈ Word 𝑇 ∧ (((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))))) → (𝐺 Σg 𝑥) = ( I ↾ 𝐷))
134		simplr 788	. . . . . . . . . . 11 ⊢ ((((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))) → (#‘𝑥) = 𝐿)
135	134	ad2antll 761	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) ∧ (𝑥 ∈ Word 𝑇 ∧ (((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))))) → (#‘𝑥) = 𝐿)
136		simpr1 1060	. . . . . . . . . . 11 ⊢ ((((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))) → 𝑏 ∈ (0..^𝐿))
137	136	ad2antll 761	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) ∧ (𝑥 ∈ Word 𝑇 ∧ (((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))))) → 𝑏 ∈ (0..^𝐿))
138		simpr2 1061	. . . . . . . . . . 11 ⊢ ((((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))) → 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ))
139	138	ad2antll 761	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) ∧ (𝑥 ∈ Word 𝑇 ∧ (((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))))) → 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ))
140		simpr3 1062	. . . . . . . . . . 11 ⊢ ((((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))) → ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))
141	140	ad2antll 761	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) ∧ (𝑥 ∈ Word 𝑇 ∧ (((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))))) → ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))
142		psgnunilem3.in	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ ∃𝑥 ∈ Word 𝑇((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))
143		fveq2 6103	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (#‘𝑥) = (#‘𝑦))
144	143	eqeq1d 2612	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((#‘𝑥) = (𝐿 − 2) ↔ (#‘𝑦) = (𝐿 − 2)))
145		oveq2 6557	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝐺 Σg 𝑥) = (𝐺 Σg 𝑦))
146	145	eqeq1d 2612	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → ((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ↔ (𝐺 Σg 𝑦) = ( I ↾ 𝐷)))
147	144, 146	anbi12d 743	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) ↔ ((#‘𝑦) = (𝐿 − 2) ∧ (𝐺 Σg 𝑦) = ( I ↾ 𝐷))))
148	147	cbvrexv 3148	. . . . . . . . . . . 12 ⊢ (∃𝑥 ∈ Word 𝑇((#‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)) ↔ ∃𝑦 ∈ Word 𝑇((#‘𝑦) = (𝐿 − 2) ∧ (𝐺 Σg 𝑦) = ( I ↾ 𝐷)))
149	142, 148	sylnib 317	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ ∃𝑦 ∈ Word 𝑇((#‘𝑦) = (𝐿 − 2) ∧ (𝐺 Σg 𝑦) = ( I ↾ 𝐷)))
150	149	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) ∧ (𝑥 ∈ Word 𝑇 ∧ (((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))))) → ¬ ∃𝑦 ∈ Word 𝑇((#‘𝑦) = (𝐿 − 2) ∧ (𝐺 Σg 𝑦) = ( I ↾ 𝐷)))
151	128, 17, 130, 131, 133, 135, 137, 139, 141, 150	psgnunilem2 17738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) ∧ (𝑥 ∈ Word 𝑇 ∧ (((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))))) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝑏 + 1) ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘(𝑏 + 1)) ∖ I ) ∧ ∀𝑐 ∈ (0..^(𝑏 + 1)) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I ))))
152	151	rexlimdvaa 3014	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) → (∃𝑥 ∈ Word 𝑇(((𝐺 Σg 𝑥) = ( I ↾ 𝐷) ∧ (#‘𝑥) = 𝐿) ∧ (𝑏 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑥‘𝑏) ∖ I ) ∧ ∀𝑑 ∈ (0..^𝑏) ¬ 𝑒 ∈ dom ((𝑥‘𝑑) ∖ I ))) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ ((𝑏 + 1) ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘(𝑏 + 1)) ∖ I ) ∧ ∀𝑐 ∈ (0..^(𝑏 + 1)) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))))
153	152	a2i 14	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ 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 )))))
154	153	a1i 11	. . . . . 6 ⊢ (𝑏 ∈ ℕ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 ))))))
155	37, 74, 85, 96, 127, 154	nn0ind 11348	. . . . 5 ⊢ (𝐿 ∈ ℕ0 → ((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (#‘𝑤) = 𝐿) ∧ (𝐿 ∈ (0..^𝐿) ∧ 𝑒 ∈ dom ((𝑤‘𝐿) ∖ I ) ∧ ∀𝑐 ∈ (0..^𝐿) ¬ 𝑒 ∈ dom ((𝑤‘𝑐) ∖ I )))))
156	26, 155	mtoi 189	. . . 4 ⊢ (𝐿 ∈ ℕ0 → ¬ (𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )))
157	156	con2i 133	. . 3 ⊢ ((𝜑 ∧ 𝑒 ∈ dom ((𝑊‘0) ∖ I )) → ¬ 𝐿 ∈ ℕ0)
158	21, 157	exlimddv 1850	. 2 ⊢ (𝜑 → ¬ 𝐿 ∈ ℕ0)
159	4, 158	pm2.65i 184	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897   ∖ cdif 3537  ∅c0 3874   class class class wbr 4583   I cid 4948  dom cdm 5038  ran crn 5039   ↾ cres 5040  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  0cc0 9815  1c1 9816   + caddc 9818   < clt 9953   − cmin 10145  ℕcn 10897  2c2 10947  ℕ₀cn0 11169  ..^cfzo 12334  #chash 12979  Word cword 13146   Σ_g cgsu 15924  SymGrpcsymg 17620  pmTrspcpmtr 17684

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-xor 1457  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-ot 4134  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-word 13154  df-lsw 13155  df-concat 13156  df-s1 13157  df-substr 13158  df-splice 13159  df-s2 13444  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-tset 15787  df-0g 15925  df-gsum 15926  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-grp 17248  df-minusg 17249  df-subg 17414  df-symg 17621  df-pmtr 17685

This theorem is referenced by:  psgnunilem4  17740