Theorem psgnunilem1 17736

Description: Lemma for psgnuni 17742. Given two consequtive transpositions in a representation of a permutation, either they are equal and therefore equivalent to the identity, or they are not and it is possible to commute them such that a chosen point in the left transposition is preserved in the right. By repeating this process, a point can be removed from a representation of the identity. (Contributed by Stefan O'Rear, 22-Aug-2015.)

Hypotheses

Ref	Expression
psgnunilem1.t	⊢ 𝑇 = ran (pmTrsp‘𝐷)
psgnunilem1.d	⊢ (𝜑 → 𝐷 ∈ 𝑉)
psgnunilem1.p	⊢ (𝜑 → 𝑃 ∈ 𝑇)
psgnunilem1.q	⊢ (𝜑 → 𝑄 ∈ 𝑇)
psgnunilem1.a	⊢ (𝜑 → 𝐴 ∈ dom (𝑃 ∖ I ))

Assertion

Ref	Expression
psgnunilem1	⊢ (𝜑 → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))

Distinct variable groups:   𝑠,𝑟,𝐴   𝑃,𝑟,𝑠   𝑄,𝑟,𝑠   𝑇,𝑟,𝑠

Allowed substitution hints:   𝜑(𝑠,𝑟)   𝐷(𝑠,𝑟)   𝑉(𝑠,𝑟)

Proof of Theorem psgnunilem1

Step	Hyp	Ref	Expression
1		psgnunilem1.q	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ 𝑇)
2		eqid 2610	. . . . . . . . 9 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
3		psgnunilem1.t	. . . . . . . . 9 ⊢ 𝑇 = ran (pmTrsp‘𝐷)
4	2, 3	pmtrfinv 17704	. . . . . . . 8 ⊢ (𝑄 ∈ 𝑇 → (𝑄 ∘ 𝑄) = ( I ↾ 𝐷))
5	1, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∘ 𝑄) = ( I ↾ 𝐷))
6		coeq1 5201	. . . . . . . 8 ⊢ (𝑃 = 𝑄 → (𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑄))
7	6	eqeq1d 2612	. . . . . . 7 ⊢ (𝑃 = 𝑄 → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ↔ (𝑄 ∘ 𝑄) = ( I ↾ 𝐷)))
8	5, 7	syl5ibrcom 236	. . . . . 6 ⊢ (𝜑 → (𝑃 = 𝑄 → (𝑃 ∘ 𝑄) = ( I ↾ 𝐷)))
9	8	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑃 = 𝑄 → (𝑃 ∘ 𝑄) = ( I ↾ 𝐷)))
10	9	imp 444	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 = 𝑄) → (𝑃 ∘ 𝑄) = ( I ↾ 𝐷))
11	10	orcd 406	. . 3 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 = 𝑄) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
12		psgnunilem1.p	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ 𝑇)
13	2, 3	pmtrfcnv 17707	. . . . . . . . . 10 ⊢ (𝑃 ∈ 𝑇 → ◡𝑃 = 𝑃)
14	12, 13	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ◡𝑃 = 𝑃)
15	14	eqcomd 2616	. . . . . . . 8 ⊢ (𝜑 → 𝑃 = ◡𝑃)
16	15	coeq2d 5206	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ 𝑃) = ((𝑃 ∘ 𝑄) ∘ ◡𝑃))
17	2, 3	pmtrff1o 17706	. . . . . . . . 9 ⊢ (𝑃 ∈ 𝑇 → 𝑃:𝐷–1-1-onto→𝐷)
18	12, 17	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑃:𝐷–1-1-onto→𝐷)
19	2, 3	pmtrfconj 17709	. . . . . . . 8 ⊢ ((𝑄 ∈ 𝑇 ∧ 𝑃:𝐷–1-1-onto→𝐷) → ((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∈ 𝑇)
20	1, 18, 19	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∈ 𝑇)
21	16, 20	eqeltrd 2688	. . . . . 6 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ 𝑃) ∈ 𝑇)
22	21	ad2antrr 758	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∘ 𝑄) ∘ 𝑃) ∈ 𝑇)
23	12	ad2antrr 758	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → 𝑃 ∈ 𝑇)
24		coass 5571	. . . . . . 7 ⊢ (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃) = ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃))
25	2, 3	pmtrfinv 17704	. . . . . . . . . 10 ⊢ (𝑃 ∈ 𝑇 → (𝑃 ∘ 𝑃) = ( I ↾ 𝐷))
26	12, 25	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ∘ 𝑃) = ( I ↾ 𝐷))
27	26	coeq2d 5206	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃)) = ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷)))
28		f1of 6050	. . . . . . . . . . 11 ⊢ (𝑃:𝐷–1-1-onto→𝐷 → 𝑃:𝐷⟶𝐷)
29	18, 28	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃:𝐷⟶𝐷)
30	2, 3	pmtrff1o 17706	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ 𝑇 → 𝑄:𝐷–1-1-onto→𝐷)
31	1, 30	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄:𝐷–1-1-onto→𝐷)
32		f1of 6050	. . . . . . . . . . 11 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → 𝑄:𝐷⟶𝐷)
33	31, 32	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:𝐷⟶𝐷)
34		fco 5971	. . . . . . . . . 10 ⊢ ((𝑃:𝐷⟶𝐷 ∧ 𝑄:𝐷⟶𝐷) → (𝑃 ∘ 𝑄):𝐷⟶𝐷)
35	29, 33, 34	syl2anc 691	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ∘ 𝑄):𝐷⟶𝐷)
36		fcoi1 5991	. . . . . . . . 9 ⊢ ((𝑃 ∘ 𝑄):𝐷⟶𝐷 → ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷)) = (𝑃 ∘ 𝑄))
37	35, 36	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷)) = (𝑃 ∘ 𝑄))
38	27, 37	eqtrd 2644	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃)) = (𝑃 ∘ 𝑄))
39	24, 38	syl5req 2657	. . . . . 6 ⊢ (𝜑 → (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃))
40	39	ad2antrr 758	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃))
41		psgnunilem1.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ dom (𝑃 ∖ I ))
42	41	ad2antrr 758	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → 𝐴 ∈ dom (𝑃 ∖ I ))
43	18	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝑃:𝐷–1-1-onto→𝐷)
44	31	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝑄:𝐷–1-1-onto→𝐷)
45	2, 3	pmtrfb 17708	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ 𝑇 ↔ (𝐷 ∈ V ∧ 𝑃:𝐷–1-1-onto→𝐷 ∧ dom (𝑃 ∖ I ) ≈ 2𝑜))
46	45	simp3bi 1071	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ 𝑇 → dom (𝑃 ∖ I ) ≈ 2𝑜)
47	12, 46	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom (𝑃 ∖ I ) ≈ 2𝑜)
48	47	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) ≈ 2𝑜)
49		2onn 7607	. . . . . . . . . . . . . . 15 ⊢ 2𝑜 ∈ ω
50		nnfi 8038	. . . . . . . . . . . . . . 15 ⊢ (2𝑜 ∈ ω → 2𝑜 ∈ Fin)
51	49, 50	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 2𝑜 ∈ Fin
52	2, 3	pmtrfb 17708	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄 ∈ 𝑇 ↔ (𝐷 ∈ V ∧ 𝑄:𝐷–1-1-onto→𝐷 ∧ dom (𝑄 ∖ I ) ≈ 2𝑜))
53	52	simp3bi 1071	. . . . . . . . . . . . . . . 16 ⊢ (𝑄 ∈ 𝑇 → dom (𝑄 ∖ I ) ≈ 2𝑜)
54	1, 53	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑄 ∖ I ) ≈ 2𝑜)
55		enfi 8061	. . . . . . . . . . . . . . 15 ⊢ (dom (𝑄 ∖ I ) ≈ 2𝑜 → (dom (𝑄 ∖ I ) ∈ Fin ↔ 2𝑜 ∈ Fin))
56	54, 55	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (dom (𝑄 ∖ I ) ∈ Fin ↔ 2𝑜 ∈ Fin))
57	51, 56	mpbiri 247	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (𝑄 ∖ I ) ∈ Fin)
58	57	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑄 ∖ I ) ∈ Fin)
59	41	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝐴 ∈ dom (𝑃 ∖ I ))
60		en2eleq 8714	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ dom (𝑃 ∖ I ) ∧ dom (𝑃 ∖ I ) ≈ 2𝑜) → dom (𝑃 ∖ I ) = {𝐴, ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})})
61	59, 48, 60	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) = {𝐴, ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})})
62		simprl 790	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝐴 ∈ dom (𝑄 ∖ I ))
63		f1ofn 6051	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃:𝐷–1-1-onto→𝐷 → 𝑃 Fn 𝐷)
64	18, 63	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 Fn 𝐷)
65	64	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝑃 Fn 𝐷)
66		imassrn 5396	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 “ dom (𝑄 ∖ I )) ⊆ ran 𝑃
67		frn 5966	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃:𝐷⟶𝐷 → ran 𝑃 ⊆ 𝐷)
68	66, 67	syl5ss 3579	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃:𝐷⟶𝐷 → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷)
69	29, 68	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷)
70	69	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷)
71		simprr 792	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))
72		fnfvima 6400	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 Fn 𝐷 ∧ (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷 ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))) → (𝑃‘𝐴) ∈ (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))))
73	65, 70, 71, 72	syl3anc 1318	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃‘𝐴) ∈ (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))))
74		difss 3699	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∖ I ) ⊆ 𝑃
75		dmss 5245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃 ∖ I ) ⊆ 𝑃 → dom (𝑃 ∖ I ) ⊆ dom 𝑃)
76	74, 75	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom (𝑃 ∖ I ) ⊆ dom 𝑃
77		f1odm 6054	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:𝐷–1-1-onto→𝐷 → dom 𝑃 = 𝐷)
78	18, 77	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → dom 𝑃 = 𝐷)
79	76, 78	syl5sseq 3616	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → dom (𝑃 ∖ I ) ⊆ 𝐷)
80	79, 41	sseldd 3569	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
81		eqid 2610	. . . . . . . . . . . . . . . . . . 19 ⊢ dom (𝑃 ∖ I ) = dom (𝑃 ∖ I )
82	2, 3, 81	pmtrffv 17702	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ 𝑇 ∧ 𝐴 ∈ 𝐷) → (𝑃‘𝐴) = if(𝐴 ∈ dom (𝑃 ∖ I ), ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}), 𝐴))
83	12, 80, 82	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃‘𝐴) = if(𝐴 ∈ dom (𝑃 ∖ I ), ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}), 𝐴))
84	41	iftrued 4044	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝐴 ∈ dom (𝑃 ∖ I ), ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}), 𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}))
85	83, 84	eqtrd 2644	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃‘𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}))
86	85	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃‘𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}))
87		imaco 5557	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∘ 𝑃) “ dom (𝑄 ∖ I )) = (𝑃 “ (𝑃 “ dom (𝑄 ∖ I )))
88	26	imaeq1d 5384	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑃 ∘ 𝑃) “ dom (𝑄 ∖ I )) = (( I ↾ 𝐷) “ dom (𝑄 ∖ I )))
89		difss 3699	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄 ∖ I ) ⊆ 𝑄
90		dmss 5245	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑄 ∖ I ) ⊆ 𝑄 → dom (𝑄 ∖ I ) ⊆ dom 𝑄)
91	89, 90	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom (𝑄 ∖ I ) ⊆ dom 𝑄
92		f1odm 6054	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → dom 𝑄 = 𝐷)
93	91, 92	syl5sseq 3616	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → dom (𝑄 ∖ I ) ⊆ 𝐷)
94	31, 93	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → dom (𝑄 ∖ I ) ⊆ 𝐷)
95		resiima 5399	. . . . . . . . . . . . . . . . . . 19 ⊢ (dom (𝑄 ∖ I ) ⊆ 𝐷 → (( I ↾ 𝐷) “ dom (𝑄 ∖ I )) = dom (𝑄 ∖ I ))
96	94, 95	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (( I ↾ 𝐷) “ dom (𝑄 ∖ I )) = dom (𝑄 ∖ I ))
97	88, 96	eqtrd 2644	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑃 ∘ 𝑃) “ dom (𝑄 ∖ I )) = dom (𝑄 ∖ I ))
98	87, 97	syl5eqr 2658	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))) = dom (𝑄 ∖ I ))
99	98	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))) = dom (𝑄 ∖ I ))
100	73, 86, 99	3eltr3d 2702	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}) ∈ dom (𝑄 ∖ I ))
101		prssi 4293	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ dom (𝑄 ∖ I ) ∧ ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}) ∈ dom (𝑄 ∖ I )) → {𝐴, ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})} ⊆ dom (𝑄 ∖ I ))
102	62, 100, 101	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → {𝐴, ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})} ⊆ dom (𝑄 ∖ I ))
103	61, 102	eqsstrd 3602	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) ⊆ dom (𝑄 ∖ I ))
104	54	ensymd 7893	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2𝑜 ≈ dom (𝑄 ∖ I ))
105		entr 7894	. . . . . . . . . . . . . 14 ⊢ ((dom (𝑃 ∖ I ) ≈ 2𝑜 ∧ 2𝑜 ≈ dom (𝑄 ∖ I )) → dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I ))
106	47, 104, 105	syl2anc 691	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I ))
107	106	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I ))
108		fisseneq 8056	. . . . . . . . . . . 12 ⊢ ((dom (𝑄 ∖ I ) ∈ Fin ∧ dom (𝑃 ∖ I ) ⊆ dom (𝑄 ∖ I ) ∧ dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I )) → dom (𝑃 ∖ I ) = dom (𝑄 ∖ I ))
109	58, 103, 107, 108	syl3anc 1318	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) = dom (𝑄 ∖ I ))
110	109	eqcomd 2616	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑄 ∖ I ) = dom (𝑃 ∖ I ))
111		f1otrspeq 17690	. . . . . . . . . 10 ⊢ (((𝑃:𝐷–1-1-onto→𝐷 ∧ 𝑄:𝐷–1-1-onto→𝐷) ∧ (dom (𝑃 ∖ I ) ≈ 2𝑜 ∧ dom (𝑄 ∖ I ) = dom (𝑃 ∖ I ))) → 𝑃 = 𝑄)
112	43, 44, 48, 110, 111	syl22anc 1319	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝑃 = 𝑄)
113	112	expr 641	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )) → 𝑃 = 𝑄))
114	113	necon3ad 2795	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑃 ≠ 𝑄 → ¬ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))))
115	114	imp 444	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ¬ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))
116	16	difeq1d 3689	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) = (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ))
117	116	dmeqd 5248	. . . . . . . . 9 ⊢ (𝜑 → dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) = dom (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ))
118		f1omvdconj 17689	. . . . . . . . . 10 ⊢ ((𝑄:𝐷⟶𝐷 ∧ 𝑃:𝐷–1-1-onto→𝐷) → dom (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ) = (𝑃 “ dom (𝑄 ∖ I )))
119	33, 18, 118	syl2anc 691	. . . . . . . . 9 ⊢ (𝜑 → dom (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ) = (𝑃 “ dom (𝑄 ∖ I )))
120	117, 119	eqtrd 2644	. . . . . . . 8 ⊢ (𝜑 → dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) = (𝑃 “ dom (𝑄 ∖ I )))
121	120	eleq2d 2673	. . . . . . 7 ⊢ (𝜑 → (𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) ↔ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))))
122	121	ad2antrr 758	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → (𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) ↔ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))))
123	115, 122	mtbird 314	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))
124		coeq1 5201	. . . . . . . 8 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝑟 ∘ 𝑠) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠))
125	124	eqeq2d 2620	. . . . . . 7 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠)))
126		difeq1 3683	. . . . . . . . . 10 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝑟 ∖ I ) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))
127	126	dmeqd 5248	. . . . . . . . 9 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → dom (𝑟 ∖ I ) = dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))
128	127	eleq2d 2673	. . . . . . . 8 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝐴 ∈ dom (𝑟 ∖ I ) ↔ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )))
129	128	notbid 307	. . . . . . 7 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (¬ 𝐴 ∈ dom (𝑟 ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )))
130	125, 129	3anbi13d 1393	. . . . . 6 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))))
131		coeq2 5202	. . . . . . . 8 ⊢ (𝑠 = 𝑃 → (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃))
132	131	eqeq2d 2620	. . . . . . 7 ⊢ (𝑠 = 𝑃 → ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃)))
133		difeq1 3683	. . . . . . . . 9 ⊢ (𝑠 = 𝑃 → (𝑠 ∖ I ) = (𝑃 ∖ I ))
134	133	dmeqd 5248	. . . . . . . 8 ⊢ (𝑠 = 𝑃 → dom (𝑠 ∖ I ) = dom (𝑃 ∖ I ))
135	134	eleq2d 2673	. . . . . . 7 ⊢ (𝑠 = 𝑃 → (𝐴 ∈ dom (𝑠 ∖ I ) ↔ 𝐴 ∈ dom (𝑃 ∖ I )))
136	132, 135	3anbi12d 1392	. . . . . 6 ⊢ (𝑠 = 𝑃 → (((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃) ∧ 𝐴 ∈ dom (𝑃 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))))
137	130, 136	rspc2ev 3295	. . . . 5 ⊢ ((((𝑃 ∘ 𝑄) ∘ 𝑃) ∈ 𝑇 ∧ 𝑃 ∈ 𝑇 ∧ ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃) ∧ 𝐴 ∈ dom (𝑃 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))
138	22, 23, 40, 42, 123, 137	syl113anc 1330	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))
139	138	olcd 407	. . 3 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
140	11, 139	pm2.61dane 2869	. 2 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
141	1	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝑄 ∈ 𝑇)
142		coass 5571	. . . . . . 7 ⊢ ((𝑄 ∘ 𝑃) ∘ 𝑄) = (𝑄 ∘ (𝑃 ∘ 𝑄))
143	2, 3	pmtrfcnv 17707	. . . . . . . . . 10 ⊢ (𝑄 ∈ 𝑇 → ◡𝑄 = 𝑄)
144	1, 143	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ◡𝑄 = 𝑄)
145	144	eqcomd 2616	. . . . . . . 8 ⊢ (𝜑 → 𝑄 = ◡𝑄)
146	145	coeq2d 5206	. . . . . . 7 ⊢ (𝜑 → ((𝑄 ∘ 𝑃) ∘ 𝑄) = ((𝑄 ∘ 𝑃) ∘ ◡𝑄))
147	142, 146	syl5eqr 2658	. . . . . 6 ⊢ (𝜑 → (𝑄 ∘ (𝑃 ∘ 𝑄)) = ((𝑄 ∘ 𝑃) ∘ ◡𝑄))
148	2, 3	pmtrfconj 17709	. . . . . . 7 ⊢ ((𝑃 ∈ 𝑇 ∧ 𝑄:𝐷–1-1-onto→𝐷) → ((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∈ 𝑇)
149	12, 31, 148	syl2anc 691	. . . . . 6 ⊢ (𝜑 → ((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∈ 𝑇)
150	147, 149	eqeltrd 2688	. . . . 5 ⊢ (𝜑 → (𝑄 ∘ (𝑃 ∘ 𝑄)) ∈ 𝑇)
151	150	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑄 ∘ (𝑃 ∘ 𝑄)) ∈ 𝑇)
152	5	coeq1d 5205	. . . . . . 7 ⊢ (𝜑 → ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄)) = (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄)))
153		fcoi2 5992	. . . . . . . 8 ⊢ ((𝑃 ∘ 𝑄):𝐷⟶𝐷 → (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄)) = (𝑃 ∘ 𝑄))
154	35, 153	syl 17	. . . . . . 7 ⊢ (𝜑 → (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄)) = (𝑃 ∘ 𝑄))
155	152, 154	eqtr2d 2645	. . . . . 6 ⊢ (𝜑 → (𝑃 ∘ 𝑄) = ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄)))
156		coass 5571	. . . . . 6 ⊢ ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄)) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄)))
157	155, 156	syl6eq 2660	. . . . 5 ⊢ (𝜑 → (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))))
158	157	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))))
159		f1ofn 6051	. . . . . . . . . 10 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → 𝑄 Fn 𝐷)
160	31, 159	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 Fn 𝐷)
161		fnelnfp 6348	. . . . . . . . 9 ⊢ ((𝑄 Fn 𝐷 ∧ 𝐴 ∈ 𝐷) → (𝐴 ∈ dom (𝑄 ∖ I ) ↔ (𝑄‘𝐴) ≠ 𝐴))
162	160, 80, 161	syl2anc 691	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ∈ dom (𝑄 ∖ I ) ↔ (𝑄‘𝐴) ≠ 𝐴))
163	162	necon2bbid 2825	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘𝐴) = 𝐴 ↔ ¬ 𝐴 ∈ dom (𝑄 ∖ I )))
164	163	biimpar 501	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑄‘𝐴) = 𝐴)
165		fnfvima 6400	. . . . . . . 8 ⊢ ((𝑄 Fn 𝐷 ∧ dom (𝑃 ∖ I ) ⊆ 𝐷 ∧ 𝐴 ∈ dom (𝑃 ∖ I )) → (𝑄‘𝐴) ∈ (𝑄 “ dom (𝑃 ∖ I )))
166	160, 79, 41, 165	syl3anc 1318	. . . . . . 7 ⊢ (𝜑 → (𝑄‘𝐴) ∈ (𝑄 “ dom (𝑃 ∖ I )))
167	166	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑄‘𝐴) ∈ (𝑄 “ dom (𝑃 ∖ I )))
168	164, 167	eqeltrrd 2689	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝐴 ∈ (𝑄 “ dom (𝑃 ∖ I )))
169	147	difeq1d 3689	. . . . . . . 8 ⊢ (𝜑 → ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ))
170	169	dmeqd 5248	. . . . . . 7 ⊢ (𝜑 → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ))
171		f1omvdconj 17689	. . . . . . . 8 ⊢ ((𝑃:𝐷⟶𝐷 ∧ 𝑄:𝐷–1-1-onto→𝐷) → dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
172	29, 31, 171	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
173	170, 172	eqtrd 2644	. . . . . 6 ⊢ (𝜑 → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
174	173	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
175	168, 174	eleqtrrd 2691	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ))
176		simpr 476	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → ¬ 𝐴 ∈ dom (𝑄 ∖ I ))
177		coeq1 5201	. . . . . . 7 ⊢ (𝑟 = 𝑄 → (𝑟 ∘ 𝑠) = (𝑄 ∘ 𝑠))
178	177	eqeq2d 2620	. . . . . 6 ⊢ (𝑟 = 𝑄 → ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠)))
179		difeq1 3683	. . . . . . . . 9 ⊢ (𝑟 = 𝑄 → (𝑟 ∖ I ) = (𝑄 ∖ I ))
180	179	dmeqd 5248	. . . . . . . 8 ⊢ (𝑟 = 𝑄 → dom (𝑟 ∖ I ) = dom (𝑄 ∖ I ))
181	180	eleq2d 2673	. . . . . . 7 ⊢ (𝑟 = 𝑄 → (𝐴 ∈ dom (𝑟 ∖ I ) ↔ 𝐴 ∈ dom (𝑄 ∖ I )))
182	181	notbid 307	. . . . . 6 ⊢ (𝑟 = 𝑄 → (¬ 𝐴 ∈ dom (𝑟 ∖ I ) ↔ ¬ 𝐴 ∈ dom (𝑄 ∖ I )))
183	178, 182	3anbi13d 1393	. . . . 5 ⊢ (𝑟 = 𝑄 → (((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I ))))
184		coeq2 5202	. . . . . . 7 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝑄 ∘ 𝑠) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))))
185	184	eqeq2d 2620	. . . . . 6 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → ((𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄)))))
186		difeq1 3683	. . . . . . . 8 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝑠 ∖ I ) = ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ))
187	186	dmeqd 5248	. . . . . . 7 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → dom (𝑠 ∖ I ) = dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ))
188	187	eleq2d 2673	. . . . . 6 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝐴 ∈ dom (𝑠 ∖ I ) ↔ 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I )))
189	185, 188	3anbi12d 1392	. . . . 5 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (((𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))) ∧ 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I ))))
190	183, 189	rspc2ev 3295	. . . 4 ⊢ ((𝑄 ∈ 𝑇 ∧ (𝑄 ∘ (𝑃 ∘ 𝑄)) ∈ 𝑇 ∧ ((𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))) ∧ 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I ))) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))
191	141, 151, 158, 175, 176, 190	syl113anc 1330	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))
192	191	olcd 407	. 2 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
193	140, 192	pm2.61dan 828	1 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ⊆ wss 3540  ifcif 4036  {csn 4125  {cpr 4127  ∪ cuni 4372   class class class wbr 4583   I cid 4948  ^◡ccnv 5037  dom cdm 5038  ran crn 5039   ↾ cres 5040   “ cima 5041   ∘ ccom 5042   Fn wfn 5799  ⟶wf 5800  –1-1-onto→wf1o 5803  ‘cfv 5804  ωcom 6957  2_𝑜c2o 7441   ≈ cen 7838  Fincfn 7841  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

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  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-ral 2901  df-rex 2902  df-reu 2903  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-uni 4373  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-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-om 6958  df-1o 7447  df-2o 7448  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-pmtr 17685

This theorem is referenced by:  psgnunilem2  17738