Theorem psgnunilem1 19016

Description: Lemma for psgnuni 19022. 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 2738	. . . . . . . . 9 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
3		psgnunilem1.t	. . . . . . . . 9 ⊢ 𝑇 = ran (pmTrsp‘𝐷)
4	2, 3	pmtrfinv 18984	. . . . . . . 8 ⊢ (𝑄 ∈ 𝑇 → (𝑄 ∘ 𝑄) = ( I ↾ 𝐷))
5	1, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∘ 𝑄) = ( I ↾ 𝐷))
6		coeq1 5755	. . . . . . . 8 ⊢ (𝑃 = 𝑄 → (𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑄))
7	6	eqeq1d 2740	. . . . . . 7 ⊢ (𝑃 = 𝑄 → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ↔ (𝑄 ∘ 𝑄) = ( I ↾ 𝐷)))
8	5, 7	syl5ibrcom 246	. . . . . 6 ⊢ (𝜑 → (𝑃 = 𝑄 → (𝑃 ∘ 𝑄) = ( I ↾ 𝐷)))
9	8	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑃 = 𝑄 → (𝑃 ∘ 𝑄) = ( I ↾ 𝐷)))
10	9	imp 406	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 = 𝑄) → (𝑃 ∘ 𝑄) = ( I ↾ 𝐷))
11	10	orcd 869	. . 3 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 = 𝑄) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
12		psgnunilem1.p	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ 𝑇)
13	2, 3	pmtrfcnv 18987	. . . . . . . . . 10 ⊢ (𝑃 ∈ 𝑇 → ◡𝑃 = 𝑃)
14	12, 13	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ◡𝑃 = 𝑃)
15	14	eqcomd 2744	. . . . . . . 8 ⊢ (𝜑 → 𝑃 = ◡𝑃)
16	15	coeq2d 5760	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ 𝑃) = ((𝑃 ∘ 𝑄) ∘ ◡𝑃))
17	2, 3	pmtrff1o 18986	. . . . . . . . 9 ⊢ (𝑃 ∈ 𝑇 → 𝑃:𝐷–1-1-onto→𝐷)
18	12, 17	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑃:𝐷–1-1-onto→𝐷)
19	2, 3	pmtrfconj 18989	. . . . . . . 8 ⊢ ((𝑄 ∈ 𝑇 ∧ 𝑃:𝐷–1-1-onto→𝐷) → ((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∈ 𝑇)
20	1, 18, 19	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∈ 𝑇)
21	16, 20	eqeltrd 2839	. . . . . 6 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ 𝑃) ∈ 𝑇)
22	21	ad2antrr 722	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∘ 𝑄) ∘ 𝑃) ∈ 𝑇)
23	12	ad2antrr 722	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → 𝑃 ∈ 𝑇)
24		coass 6158	. . . . . . 7 ⊢ (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃) = ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃))
25	2, 3	pmtrfinv 18984	. . . . . . . . . 10 ⊢ (𝑃 ∈ 𝑇 → (𝑃 ∘ 𝑃) = ( I ↾ 𝐷))
26	12, 25	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ∘ 𝑃) = ( I ↾ 𝐷))
27	26	coeq2d 5760	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃)) = ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷)))
28		f1of 6700	. . . . . . . . . . 11 ⊢ (𝑃:𝐷–1-1-onto→𝐷 → 𝑃:𝐷⟶𝐷)
29	18, 28	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃:𝐷⟶𝐷)
30	2, 3	pmtrff1o 18986	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ 𝑇 → 𝑄:𝐷–1-1-onto→𝐷)
31	1, 30	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄:𝐷–1-1-onto→𝐷)
32		f1of 6700	. . . . . . . . . . 11 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → 𝑄:𝐷⟶𝐷)
33	31, 32	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:𝐷⟶𝐷)
34		fco 6608	. . . . . . . . . 10 ⊢ ((𝑃:𝐷⟶𝐷 ∧ 𝑄:𝐷⟶𝐷) → (𝑃 ∘ 𝑄):𝐷⟶𝐷)
35	29, 33, 34	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ∘ 𝑄):𝐷⟶𝐷)
36		fcoi1 6632	. . . . . . . . 9 ⊢ ((𝑃 ∘ 𝑄):𝐷⟶𝐷 → ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷)) = (𝑃 ∘ 𝑄))
37	35, 36	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷)) = (𝑃 ∘ 𝑄))
38	27, 37	eqtrd 2778	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃)) = (𝑃 ∘ 𝑄))
39	24, 38	eqtr2id 2792	. . . . . 6 ⊢ (𝜑 → (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃))
40	39	ad2antrr 722	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃))
41		psgnunilem1.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ dom (𝑃 ∖ I ))
42	41	ad2antrr 722	. . . . 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 18988	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ 𝑇 ↔ (𝐷 ∈ V ∧ 𝑃:𝐷–1-1-onto→𝐷 ∧ dom (𝑃 ∖ I ) ≈ 2o))
46	45	simp3bi 1145	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ 𝑇 → dom (𝑃 ∖ I ) ≈ 2o)
47	12, 46	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom (𝑃 ∖ I ) ≈ 2o)
48	47	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) ≈ 2o)
49		2onn 8433	. . . . . . . . . . . . . . 15 ⊢ 2o ∈ ω
50		nnfi 8912	. . . . . . . . . . . . . . 15 ⊢ (2o ∈ ω → 2o ∈ Fin)
51	49, 50	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 2o ∈ Fin
52	2, 3	pmtrfb 18988	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄 ∈ 𝑇 ↔ (𝐷 ∈ V ∧ 𝑄:𝐷–1-1-onto→𝐷 ∧ dom (𝑄 ∖ I ) ≈ 2o))
53	52	simp3bi 1145	. . . . . . . . . . . . . . . 16 ⊢ (𝑄 ∈ 𝑇 → dom (𝑄 ∖ I ) ≈ 2o)
54	1, 53	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑄 ∖ I ) ≈ 2o)
55		enfi 8933	. . . . . . . . . . . . . . 15 ⊢ (dom (𝑄 ∖ I ) ≈ 2o → (dom (𝑄 ∖ I ) ∈ Fin ↔ 2o ∈ Fin))
56	54, 55	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (dom (𝑄 ∖ I ) ∈ Fin ↔ 2o ∈ Fin))
57	51, 56	mpbiri 257	. . . . . . . . . . . . 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 9695	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ dom (𝑃 ∖ I ) ∧ dom (𝑃 ∖ I ) ≈ 2o) → dom (𝑃 ∖ I ) = {𝐴, ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})})
61	59, 48, 60	syl2anc 583	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) = {𝐴, ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})})
62		simprl 767	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝐴 ∈ dom (𝑄 ∖ I ))
63		f1ofn 6701	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃:𝐷–1-1-onto→𝐷 → 𝑃 Fn 𝐷)
64	18, 63	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 Fn 𝐷)
65	64	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝑃 Fn 𝐷)
66		fimass 6605	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃:𝐷⟶𝐷 → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷)
67	29, 66	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷)
68	67	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷)
69		simprr 769	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))
70		fnfvima 7091	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 Fn 𝐷 ∧ (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷 ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))) → (𝑃‘𝐴) ∈ (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))))
71	65, 68, 69, 70	syl3anc 1369	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃‘𝐴) ∈ (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))))
72		difss 4062	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∖ I ) ⊆ 𝑃
73		dmss 5800	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃 ∖ I ) ⊆ 𝑃 → dom (𝑃 ∖ I ) ⊆ dom 𝑃)
74	72, 73	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom (𝑃 ∖ I ) ⊆ dom 𝑃
75		f1odm 6704	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:𝐷–1-1-onto→𝐷 → dom 𝑃 = 𝐷)
76	18, 75	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → dom 𝑃 = 𝐷)
77	74, 76	sseqtrid 3969	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → dom (𝑃 ∖ I ) ⊆ 𝐷)
78	77, 41	sseldd 3918	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
79		eqid 2738	. . . . . . . . . . . . . . . . . . 19 ⊢ dom (𝑃 ∖ I ) = dom (𝑃 ∖ I )
80	2, 3, 79	pmtrffv 18982	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ 𝑇 ∧ 𝐴 ∈ 𝐷) → (𝑃‘𝐴) = if(𝐴 ∈ dom (𝑃 ∖ I ), ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}), 𝐴))
81	12, 78, 80	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃‘𝐴) = if(𝐴 ∈ dom (𝑃 ∖ I ), ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}), 𝐴))
82	41	iftrued 4464	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝐴 ∈ dom (𝑃 ∖ I ), ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}), 𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}))
83	81, 82	eqtrd 2778	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃‘𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}))
84	83	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃‘𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}))
85		imaco 6144	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∘ 𝑃) “ dom (𝑄 ∖ I )) = (𝑃 “ (𝑃 “ dom (𝑄 ∖ I )))
86	26	imaeq1d 5957	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑃 ∘ 𝑃) “ dom (𝑄 ∖ I )) = (( I ↾ 𝐷) “ dom (𝑄 ∖ I )))
87		difss 4062	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄 ∖ I ) ⊆ 𝑄
88		dmss 5800	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑄 ∖ I ) ⊆ 𝑄 → dom (𝑄 ∖ I ) ⊆ dom 𝑄)
89	87, 88	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom (𝑄 ∖ I ) ⊆ dom 𝑄
90		f1odm 6704	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → dom 𝑄 = 𝐷)
91	89, 90	sseqtrid 3969	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → dom (𝑄 ∖ I ) ⊆ 𝐷)
92	31, 91	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → dom (𝑄 ∖ I ) ⊆ 𝐷)
93		resiima 5973	. . . . . . . . . . . . . . . . . . 19 ⊢ (dom (𝑄 ∖ I ) ⊆ 𝐷 → (( I ↾ 𝐷) “ dom (𝑄 ∖ I )) = dom (𝑄 ∖ I ))
94	92, 93	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (( I ↾ 𝐷) “ dom (𝑄 ∖ I )) = dom (𝑄 ∖ I ))
95	86, 94	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑃 ∘ 𝑃) “ dom (𝑄 ∖ I )) = dom (𝑄 ∖ I ))
96	85, 95	eqtr3id 2793	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))) = dom (𝑄 ∖ I ))
97	96	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))) = dom (𝑄 ∖ I ))
98	71, 84, 97	3eltr3d 2853	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}) ∈ dom (𝑄 ∖ I ))
99	62, 98	prssd 4752	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → {𝐴, ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})} ⊆ dom (𝑄 ∖ I ))
100	61, 99	eqsstrd 3955	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) ⊆ dom (𝑄 ∖ I ))
101	54	ensymd 8746	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2o ≈ dom (𝑄 ∖ I ))
102		entr 8747	. . . . . . . . . . . . . 14 ⊢ ((dom (𝑃 ∖ I ) ≈ 2o ∧ 2o ≈ dom (𝑄 ∖ I )) → dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I ))
103	47, 101, 102	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I ))
104	103	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I ))
105		fisseneq 8963	. . . . . . . . . . . 12 ⊢ ((dom (𝑄 ∖ I ) ∈ Fin ∧ dom (𝑃 ∖ I ) ⊆ dom (𝑄 ∖ I ) ∧ dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I )) → dom (𝑃 ∖ I ) = dom (𝑄 ∖ I ))
106	58, 100, 104, 105	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) = dom (𝑄 ∖ I ))
107	106	eqcomd 2744	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑄 ∖ I ) = dom (𝑃 ∖ I ))
108		f1otrspeq 18970	. . . . . . . . . 10 ⊢ (((𝑃:𝐷–1-1-onto→𝐷 ∧ 𝑄:𝐷–1-1-onto→𝐷) ∧ (dom (𝑃 ∖ I ) ≈ 2o ∧ dom (𝑄 ∖ I ) = dom (𝑃 ∖ I ))) → 𝑃 = 𝑄)
109	43, 44, 48, 107, 108	syl22anc 835	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝑃 = 𝑄)
110	109	expr 456	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )) → 𝑃 = 𝑄))
111	110	necon3ad 2955	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑃 ≠ 𝑄 → ¬ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))))
112	111	imp 406	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ¬ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))
113	16	difeq1d 4052	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) = (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ))
114	113	dmeqd 5803	. . . . . . . . 9 ⊢ (𝜑 → dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) = dom (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ))
115		f1omvdconj 18969	. . . . . . . . . 10 ⊢ ((𝑄:𝐷⟶𝐷 ∧ 𝑃:𝐷–1-1-onto→𝐷) → dom (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ) = (𝑃 “ dom (𝑄 ∖ I )))
116	33, 18, 115	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → dom (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ) = (𝑃 “ dom (𝑄 ∖ I )))
117	114, 116	eqtrd 2778	. . . . . . . 8 ⊢ (𝜑 → dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) = (𝑃 “ dom (𝑄 ∖ I )))
118	117	eleq2d 2824	. . . . . . 7 ⊢ (𝜑 → (𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) ↔ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))))
119	118	ad2antrr 722	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → (𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) ↔ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))))
120	112, 119	mtbird 324	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))
121		coeq1 5755	. . . . . . . 8 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝑟 ∘ 𝑠) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠))
122	121	eqeq2d 2749	. . . . . . 7 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠)))
123		difeq1 4046	. . . . . . . . . 10 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝑟 ∖ I ) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))
124	123	dmeqd 5803	. . . . . . . . 9 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → dom (𝑟 ∖ I ) = dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))
125	124	eleq2d 2824	. . . . . . . 8 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝐴 ∈ dom (𝑟 ∖ I ) ↔ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )))
126	125	notbid 317	. . . . . . 7 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (¬ 𝐴 ∈ dom (𝑟 ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )))
127	122, 126	3anbi13d 1436	. . . . . 6 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))))
128		coeq2 5756	. . . . . . . 8 ⊢ (𝑠 = 𝑃 → (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃))
129	128	eqeq2d 2749	. . . . . . 7 ⊢ (𝑠 = 𝑃 → ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃)))
130		difeq1 4046	. . . . . . . . 9 ⊢ (𝑠 = 𝑃 → (𝑠 ∖ I ) = (𝑃 ∖ I ))
131	130	dmeqd 5803	. . . . . . . 8 ⊢ (𝑠 = 𝑃 → dom (𝑠 ∖ I ) = dom (𝑃 ∖ I ))
132	131	eleq2d 2824	. . . . . . 7 ⊢ (𝑠 = 𝑃 → (𝐴 ∈ dom (𝑠 ∖ I ) ↔ 𝐴 ∈ dom (𝑃 ∖ I )))
133	129, 132	3anbi12d 1435	. . . . . 6 ⊢ (𝑠 = 𝑃 → (((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃) ∧ 𝐴 ∈ dom (𝑃 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))))
134	127, 133	rspc2ev 3564	. . . . 5 ⊢ ((((𝑃 ∘ 𝑄) ∘ 𝑃) ∈ 𝑇 ∧ 𝑃 ∈ 𝑇 ∧ ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃) ∧ 𝐴 ∈ dom (𝑃 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))
135	22, 23, 40, 42, 120, 134	syl113anc 1380	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))
136	135	olcd 870	. . 3 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
137	11, 136	pm2.61dane 3031	. 2 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
138	1	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝑄 ∈ 𝑇)
139		coass 6158	. . . . . . 7 ⊢ ((𝑄 ∘ 𝑃) ∘ 𝑄) = (𝑄 ∘ (𝑃 ∘ 𝑄))
140	2, 3	pmtrfcnv 18987	. . . . . . . . . 10 ⊢ (𝑄 ∈ 𝑇 → ◡𝑄 = 𝑄)
141	1, 140	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ◡𝑄 = 𝑄)
142	141	eqcomd 2744	. . . . . . . 8 ⊢ (𝜑 → 𝑄 = ◡𝑄)
143	142	coeq2d 5760	. . . . . . 7 ⊢ (𝜑 → ((𝑄 ∘ 𝑃) ∘ 𝑄) = ((𝑄 ∘ 𝑃) ∘ ◡𝑄))
144	139, 143	eqtr3id 2793	. . . . . 6 ⊢ (𝜑 → (𝑄 ∘ (𝑃 ∘ 𝑄)) = ((𝑄 ∘ 𝑃) ∘ ◡𝑄))
145	2, 3	pmtrfconj 18989	. . . . . . 7 ⊢ ((𝑃 ∈ 𝑇 ∧ 𝑄:𝐷–1-1-onto→𝐷) → ((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∈ 𝑇)
146	12, 31, 145	syl2anc 583	. . . . . 6 ⊢ (𝜑 → ((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∈ 𝑇)
147	144, 146	eqeltrd 2839	. . . . 5 ⊢ (𝜑 → (𝑄 ∘ (𝑃 ∘ 𝑄)) ∈ 𝑇)
148	147	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑄 ∘ (𝑃 ∘ 𝑄)) ∈ 𝑇)
149	5	coeq1d 5759	. . . . . . 7 ⊢ (𝜑 → ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄)) = (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄)))
150		fcoi2 6633	. . . . . . . 8 ⊢ ((𝑃 ∘ 𝑄):𝐷⟶𝐷 → (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄)) = (𝑃 ∘ 𝑄))
151	35, 150	syl 17	. . . . . . 7 ⊢ (𝜑 → (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄)) = (𝑃 ∘ 𝑄))
152	149, 151	eqtr2d 2779	. . . . . 6 ⊢ (𝜑 → (𝑃 ∘ 𝑄) = ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄)))
153		coass 6158	. . . . . 6 ⊢ ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄)) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄)))
154	152, 153	eqtrdi 2795	. . . . 5 ⊢ (𝜑 → (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))))
155	154	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))))
156		f1ofn 6701	. . . . . . . . . 10 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → 𝑄 Fn 𝐷)
157	31, 156	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 Fn 𝐷)
158		fnelnfp 7031	. . . . . . . . 9 ⊢ ((𝑄 Fn 𝐷 ∧ 𝐴 ∈ 𝐷) → (𝐴 ∈ dom (𝑄 ∖ I ) ↔ (𝑄‘𝐴) ≠ 𝐴))
159	157, 78, 158	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ∈ dom (𝑄 ∖ I ) ↔ (𝑄‘𝐴) ≠ 𝐴))
160	159	necon2bbid 2986	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘𝐴) = 𝐴 ↔ ¬ 𝐴 ∈ dom (𝑄 ∖ I )))
161	160	biimpar 477	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑄‘𝐴) = 𝐴)
162		fnfvima 7091	. . . . . . . 8 ⊢ ((𝑄 Fn 𝐷 ∧ dom (𝑃 ∖ I ) ⊆ 𝐷 ∧ 𝐴 ∈ dom (𝑃 ∖ I )) → (𝑄‘𝐴) ∈ (𝑄 “ dom (𝑃 ∖ I )))
163	157, 77, 41, 162	syl3anc 1369	. . . . . . 7 ⊢ (𝜑 → (𝑄‘𝐴) ∈ (𝑄 “ dom (𝑃 ∖ I )))
164	163	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑄‘𝐴) ∈ (𝑄 “ dom (𝑃 ∖ I )))
165	161, 164	eqeltrrd 2840	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝐴 ∈ (𝑄 “ dom (𝑃 ∖ I )))
166	144	difeq1d 4052	. . . . . . . 8 ⊢ (𝜑 → ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ))
167	166	dmeqd 5803	. . . . . . 7 ⊢ (𝜑 → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ))
168		f1omvdconj 18969	. . . . . . . 8 ⊢ ((𝑃:𝐷⟶𝐷 ∧ 𝑄:𝐷–1-1-onto→𝐷) → dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
169	29, 31, 168	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
170	167, 169	eqtrd 2778	. . . . . 6 ⊢ (𝜑 → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
171	170	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
172	165, 171	eleqtrrd 2842	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ))
173		simpr 484	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → ¬ 𝐴 ∈ dom (𝑄 ∖ I ))
174		coeq1 5755	. . . . . . 7 ⊢ (𝑟 = 𝑄 → (𝑟 ∘ 𝑠) = (𝑄 ∘ 𝑠))
175	174	eqeq2d 2749	. . . . . 6 ⊢ (𝑟 = 𝑄 → ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠)))
176		difeq1 4046	. . . . . . . . 9 ⊢ (𝑟 = 𝑄 → (𝑟 ∖ I ) = (𝑄 ∖ I ))
177	176	dmeqd 5803	. . . . . . . 8 ⊢ (𝑟 = 𝑄 → dom (𝑟 ∖ I ) = dom (𝑄 ∖ I ))
178	177	eleq2d 2824	. . . . . . 7 ⊢ (𝑟 = 𝑄 → (𝐴 ∈ dom (𝑟 ∖ I ) ↔ 𝐴 ∈ dom (𝑄 ∖ I )))
179	178	notbid 317	. . . . . 6 ⊢ (𝑟 = 𝑄 → (¬ 𝐴 ∈ dom (𝑟 ∖ I ) ↔ ¬ 𝐴 ∈ dom (𝑄 ∖ I )))
180	175, 179	3anbi13d 1436	. . . . 5 ⊢ (𝑟 = 𝑄 → (((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I ))))
181		coeq2 5756	. . . . . . 7 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝑄 ∘ 𝑠) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))))
182	181	eqeq2d 2749	. . . . . 6 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → ((𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄)))))
183		difeq1 4046	. . . . . . . 8 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝑠 ∖ I ) = ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ))
184	183	dmeqd 5803	. . . . . . 7 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → dom (𝑠 ∖ I ) = dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ))
185	184	eleq2d 2824	. . . . . 6 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝐴 ∈ dom (𝑠 ∖ I ) ↔ 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I )))
186	182, 185	3anbi12d 1435	. . . . 5 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (((𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))) ∧ 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I ))))
187	180, 186	rspc2ev 3564	. . . 4 ⊢ ((𝑄 ∈ 𝑇 ∧ (𝑄 ∘ (𝑃 ∘ 𝑄)) ∈ 𝑇 ∧ ((𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))) ∧ 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I ))) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))
188	138, 148, 155, 172, 173, 187	syl113anc 1380	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))
189	188	olcd 870	. 2 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
190	137, 189	pm2.61dan 809	1 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  ∃wrex 3064  Vcvv 3422   ∖ cdif 3880   ⊆ wss 3883  ifcif 4456  {csn 4558  {cpr 4560  ∪ cuni 4836   class class class wbr 5070   I cid 5479  ^◡ccnv 5579  dom cdm 5580  ran crn 5581   ↾ cres 5582   “ cima 5583   ∘ ccom 5584   Fn wfn 6413  ⟶wf 6414  –1-1-onto→wf1o 6417  ‘cfv 6418  ωcom 7687  2_oc2o 8261   ≈ cen 8688  Fincfn 8691  pmTrspcpmtr 18964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-om 7688  df-1o 8267  df-2o 8268  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695  df-pmtr 18965

This theorem is referenced by:  psgnunilem2  19018