Theorem psgnunilem1 19479

Description: Lemma for psgnuni 19485. 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 2736	. . . . . . . . 9 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
3		psgnunilem1.t	. . . . . . . . 9 ⊢ 𝑇 = ran (pmTrsp‘𝐷)
4	2, 3	pmtrfinv 19447	. . . . . . . 8 ⊢ (𝑄 ∈ 𝑇 → (𝑄 ∘ 𝑄) = ( I ↾ 𝐷))
5	1, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∘ 𝑄) = ( I ↾ 𝐷))
6		coeq1 5842	. . . . . . . 8 ⊢ (𝑃 = 𝑄 → (𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑄))
7	6	eqeq1d 2738	. . . . . . 7 ⊢ (𝑃 = 𝑄 → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ↔ (𝑄 ∘ 𝑄) = ( I ↾ 𝐷)))
8	5, 7	syl5ibrcom 247	. . . . . 6 ⊢ (𝜑 → (𝑃 = 𝑄 → (𝑃 ∘ 𝑄) = ( I ↾ 𝐷)))
9	8	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑃 = 𝑄 → (𝑃 ∘ 𝑄) = ( I ↾ 𝐷)))
10	9	imp 406	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 = 𝑄) → (𝑃 ∘ 𝑄) = ( I ↾ 𝐷))
11	10	orcd 873	. . 3 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 = 𝑄) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
12		psgnunilem1.p	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ 𝑇)
13	2, 3	pmtrfcnv 19450	. . . . . . . . . 10 ⊢ (𝑃 ∈ 𝑇 → ◡𝑃 = 𝑃)
14	12, 13	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ◡𝑃 = 𝑃)
15	14	eqcomd 2742	. . . . . . . 8 ⊢ (𝜑 → 𝑃 = ◡𝑃)
16	15	coeq2d 5847	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ 𝑃) = ((𝑃 ∘ 𝑄) ∘ ◡𝑃))
17	2, 3	pmtrff1o 19449	. . . . . . . . 9 ⊢ (𝑃 ∈ 𝑇 → 𝑃:𝐷–1-1-onto→𝐷)
18	12, 17	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑃:𝐷–1-1-onto→𝐷)
19	2, 3	pmtrfconj 19452	. . . . . . . 8 ⊢ ((𝑄 ∈ 𝑇 ∧ 𝑃:𝐷–1-1-onto→𝐷) → ((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∈ 𝑇)
20	1, 18, 19	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∈ 𝑇)
21	16, 20	eqeltrd 2835	. . . . . 6 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ 𝑃) ∈ 𝑇)
22	21	ad2antrr 726	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∘ 𝑄) ∘ 𝑃) ∈ 𝑇)
23	12	ad2antrr 726	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → 𝑃 ∈ 𝑇)
24		coass 6259	. . . . . . 7 ⊢ (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃) = ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃))
25	2, 3	pmtrfinv 19447	. . . . . . . . . 10 ⊢ (𝑃 ∈ 𝑇 → (𝑃 ∘ 𝑃) = ( I ↾ 𝐷))
26	12, 25	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ∘ 𝑃) = ( I ↾ 𝐷))
27	26	coeq2d 5847	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃)) = ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷)))
28		f1of 6823	. . . . . . . . . . 11 ⊢ (𝑃:𝐷–1-1-onto→𝐷 → 𝑃:𝐷⟶𝐷)
29	18, 28	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃:𝐷⟶𝐷)
30	2, 3	pmtrff1o 19449	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ 𝑇 → 𝑄:𝐷–1-1-onto→𝐷)
31	1, 30	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄:𝐷–1-1-onto→𝐷)
32		f1of 6823	. . . . . . . . . . 11 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → 𝑄:𝐷⟶𝐷)
33	31, 32	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:𝐷⟶𝐷)
34		fco 6735	. . . . . . . . . 10 ⊢ ((𝑃:𝐷⟶𝐷 ∧ 𝑄:𝐷⟶𝐷) → (𝑃 ∘ 𝑄):𝐷⟶𝐷)
35	29, 33, 34	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ∘ 𝑄):𝐷⟶𝐷)
36		fcoi1 6757	. . . . . . . . 9 ⊢ ((𝑃 ∘ 𝑄):𝐷⟶𝐷 → ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷)) = (𝑃 ∘ 𝑄))
37	35, 36	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷)) = (𝑃 ∘ 𝑄))
38	27, 37	eqtrd 2771	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃)) = (𝑃 ∘ 𝑄))
39	24, 38	eqtr2id 2784	. . . . . 6 ⊢ (𝜑 → (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃))
40	39	ad2antrr 726	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃))
41		psgnunilem1.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ dom (𝑃 ∖ I ))
42	41	ad2antrr 726	. . . . 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 19451	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ 𝑇 ↔ (𝐷 ∈ V ∧ 𝑃:𝐷–1-1-onto→𝐷 ∧ dom (𝑃 ∖ I ) ≈ 2o))
46	45	simp3bi 1147	. . . . . . . . . . . 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 8659	. . . . . . . . . . . . . . 15 ⊢ 2o ∈ ω
50		nnfi 9186	. . . . . . . . . . . . . . 15 ⊢ (2o ∈ ω → 2o ∈ Fin)
51	49, 50	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 2o ∈ Fin
52	2, 3	pmtrfb 19451	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄 ∈ 𝑇 ↔ (𝐷 ∈ V ∧ 𝑄:𝐷–1-1-onto→𝐷 ∧ dom (𝑄 ∖ I ) ≈ 2o))
53	52	simp3bi 1147	. . . . . . . . . . . . . . . 16 ⊢ (𝑄 ∈ 𝑇 → dom (𝑄 ∖ I ) ≈ 2o)
54	1, 53	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑄 ∖ I ) ≈ 2o)
55		enfi 9206	. . . . . . . . . . . . . . 15 ⊢ (dom (𝑄 ∖ I ) ≈ 2o → (dom (𝑄 ∖ I ) ∈ Fin ↔ 2o ∈ Fin))
56	54, 55	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (dom (𝑄 ∖ I ) ∈ Fin ↔ 2o ∈ Fin))
57	51, 56	mpbiri 258	. . . . . . . . . . . . 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 10027	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ dom (𝑃 ∖ I ) ∧ dom (𝑃 ∖ I ) ≈ 2o) → dom (𝑃 ∖ I ) = {𝐴, ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})})
61	59, 48, 60	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) = {𝐴, ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})})
62		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝐴 ∈ dom (𝑄 ∖ I ))
63		f1ofn 6824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃:𝐷–1-1-onto→𝐷 → 𝑃 Fn 𝐷)
64	18, 63	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 Fn 𝐷)
65	64	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝑃 Fn 𝐷)
66		fimass 6731	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃:𝐷⟶𝐷 → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷)
67	29, 66	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷)
68	67	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷)
69		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))
70		fnfvima 7230	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 Fn 𝐷 ∧ (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷 ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))) → (𝑃‘𝐴) ∈ (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))))
71	65, 68, 69, 70	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃‘𝐴) ∈ (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))))
72		difss 4116	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∖ I ) ⊆ 𝑃
73		dmss 5887	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃 ∖ I ) ⊆ 𝑃 → dom (𝑃 ∖ I ) ⊆ dom 𝑃)
74	72, 73	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom (𝑃 ∖ I ) ⊆ dom 𝑃
75		f1odm 6827	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:𝐷–1-1-onto→𝐷 → dom 𝑃 = 𝐷)
76	18, 75	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → dom 𝑃 = 𝐷)
77	74, 76	sseqtrid 4006	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → dom (𝑃 ∖ I ) ⊆ 𝐷)
78	77, 41	sseldd 3964	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
79		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ dom (𝑃 ∖ I ) = dom (𝑃 ∖ I )
80	2, 3, 79	pmtrffv 19445	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ 𝑇 ∧ 𝐴 ∈ 𝐷) → (𝑃‘𝐴) = if(𝐴 ∈ dom (𝑃 ∖ I ), ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}), 𝐴))
81	12, 78, 80	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃‘𝐴) = if(𝐴 ∈ dom (𝑃 ∖ I ), ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}), 𝐴))
82	41	iftrued 4513	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝐴 ∈ dom (𝑃 ∖ I ), ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}), 𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}))
83	81, 82	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃‘𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}))
84	83	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃‘𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}))
85		imaco 6245	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∘ 𝑃) “ dom (𝑄 ∖ I )) = (𝑃 “ (𝑃 “ dom (𝑄 ∖ I )))
86	26	imaeq1d 6051	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑃 ∘ 𝑃) “ dom (𝑄 ∖ I )) = (( I ↾ 𝐷) “ dom (𝑄 ∖ I )))
87		difss 4116	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄 ∖ I ) ⊆ 𝑄
88		dmss 5887	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑄 ∖ I ) ⊆ 𝑄 → dom (𝑄 ∖ I ) ⊆ dom 𝑄)
89	87, 88	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom (𝑄 ∖ I ) ⊆ dom 𝑄
90		f1odm 6827	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → dom 𝑄 = 𝐷)
91	89, 90	sseqtrid 4006	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → dom (𝑄 ∖ I ) ⊆ 𝐷)
92	31, 91	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → dom (𝑄 ∖ I ) ⊆ 𝐷)
93		resiima 6068	. . . . . . . . . . . . . . . . . . 19 ⊢ (dom (𝑄 ∖ I ) ⊆ 𝐷 → (( I ↾ 𝐷) “ dom (𝑄 ∖ I )) = dom (𝑄 ∖ I ))
94	92, 93	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (( I ↾ 𝐷) “ dom (𝑄 ∖ I )) = dom (𝑄 ∖ I ))
95	86, 94	eqtrd 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑃 ∘ 𝑃) “ dom (𝑄 ∖ I )) = dom (𝑄 ∖ I ))
96	85, 95	eqtr3id 2785	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))) = dom (𝑄 ∖ I ))
97	96	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))) = dom (𝑄 ∖ I ))
98	71, 84, 97	3eltr3d 2849	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}) ∈ dom (𝑄 ∖ I ))
99	62, 98	prssd 4803	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → {𝐴, ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})} ⊆ dom (𝑄 ∖ I ))
100	61, 99	eqsstrd 3998	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) ⊆ dom (𝑄 ∖ I ))
101	54	ensymd 9024	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2o ≈ dom (𝑄 ∖ I ))
102		entr 9025	. . . . . . . . . . . . . 14 ⊢ ((dom (𝑃 ∖ I ) ≈ 2o ∧ 2o ≈ dom (𝑄 ∖ I )) → dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I ))
103	47, 101, 102	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I ))
104	103	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I ))
105		fisseneq 9270	. . . . . . . . . . . 12 ⊢ ((dom (𝑄 ∖ I ) ∈ Fin ∧ dom (𝑃 ∖ I ) ⊆ dom (𝑄 ∖ I ) ∧ dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I )) → dom (𝑃 ∖ I ) = dom (𝑄 ∖ I ))
106	58, 100, 104, 105	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) = dom (𝑄 ∖ I ))
107	106	eqcomd 2742	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑄 ∖ I ) = dom (𝑃 ∖ I ))
108		f1otrspeq 19433	. . . . . . . . . 10 ⊢ (((𝑃:𝐷–1-1-onto→𝐷 ∧ 𝑄:𝐷–1-1-onto→𝐷) ∧ (dom (𝑃 ∖ I ) ≈ 2o ∧ dom (𝑄 ∖ I ) = dom (𝑃 ∖ I ))) → 𝑃 = 𝑄)
109	43, 44, 48, 107, 108	syl22anc 838	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝑃 = 𝑄)
110	109	expr 456	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )) → 𝑃 = 𝑄))
111	110	necon3ad 2946	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑃 ≠ 𝑄 → ¬ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))))
112	111	imp 406	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ¬ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))
113	16	difeq1d 4105	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) = (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ))
114	113	dmeqd 5890	. . . . . . . . 9 ⊢ (𝜑 → dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) = dom (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ))
115		f1omvdconj 19432	. . . . . . . . . 10 ⊢ ((𝑄:𝐷⟶𝐷 ∧ 𝑃:𝐷–1-1-onto→𝐷) → dom (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ) = (𝑃 “ dom (𝑄 ∖ I )))
116	33, 18, 115	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → dom (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ) = (𝑃 “ dom (𝑄 ∖ I )))
117	114, 116	eqtrd 2771	. . . . . . . 8 ⊢ (𝜑 → dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) = (𝑃 “ dom (𝑄 ∖ I )))
118	117	eleq2d 2821	. . . . . . 7 ⊢ (𝜑 → (𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) ↔ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))))
119	118	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → (𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) ↔ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))))
120	112, 119	mtbird 325	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))
121		coeq1 5842	. . . . . . . 8 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝑟 ∘ 𝑠) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠))
122	121	eqeq2d 2747	. . . . . . 7 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠)))
123		difeq1 4099	. . . . . . . . . 10 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝑟 ∖ I ) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))
124	123	dmeqd 5890	. . . . . . . . 9 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → dom (𝑟 ∖ I ) = dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))
125	124	eleq2d 2821	. . . . . . . 8 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝐴 ∈ dom (𝑟 ∖ I ) ↔ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )))
126	125	notbid 318	. . . . . . 7 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (¬ 𝐴 ∈ dom (𝑟 ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )))
127	122, 126	3anbi13d 1440	. . . . . 6 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))))
128		coeq2 5843	. . . . . . . 8 ⊢ (𝑠 = 𝑃 → (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃))
129	128	eqeq2d 2747	. . . . . . 7 ⊢ (𝑠 = 𝑃 → ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃)))
130		difeq1 4099	. . . . . . . . 9 ⊢ (𝑠 = 𝑃 → (𝑠 ∖ I ) = (𝑃 ∖ I ))
131	130	dmeqd 5890	. . . . . . . 8 ⊢ (𝑠 = 𝑃 → dom (𝑠 ∖ I ) = dom (𝑃 ∖ I ))
132	131	eleq2d 2821	. . . . . . 7 ⊢ (𝑠 = 𝑃 → (𝐴 ∈ dom (𝑠 ∖ I ) ↔ 𝐴 ∈ dom (𝑃 ∖ I )))
133	129, 132	3anbi12d 1439	. . . . . 6 ⊢ (𝑠 = 𝑃 → (((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃) ∧ 𝐴 ∈ dom (𝑃 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))))
134	127, 133	rspc2ev 3619	. . . . 5 ⊢ ((((𝑃 ∘ 𝑄) ∘ 𝑃) ∈ 𝑇 ∧ 𝑃 ∈ 𝑇 ∧ ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃) ∧ 𝐴 ∈ dom (𝑃 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))
135	22, 23, 40, 42, 120, 134	syl113anc 1384	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))
136	135	olcd 874	. . 3 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
137	11, 136	pm2.61dane 3020	. 2 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
138	1	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝑄 ∈ 𝑇)
139		coass 6259	. . . . . . 7 ⊢ ((𝑄 ∘ 𝑃) ∘ 𝑄) = (𝑄 ∘ (𝑃 ∘ 𝑄))
140	2, 3	pmtrfcnv 19450	. . . . . . . . . 10 ⊢ (𝑄 ∈ 𝑇 → ◡𝑄 = 𝑄)
141	1, 140	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ◡𝑄 = 𝑄)
142	141	eqcomd 2742	. . . . . . . 8 ⊢ (𝜑 → 𝑄 = ◡𝑄)
143	142	coeq2d 5847	. . . . . . 7 ⊢ (𝜑 → ((𝑄 ∘ 𝑃) ∘ 𝑄) = ((𝑄 ∘ 𝑃) ∘ ◡𝑄))
144	139, 143	eqtr3id 2785	. . . . . 6 ⊢ (𝜑 → (𝑄 ∘ (𝑃 ∘ 𝑄)) = ((𝑄 ∘ 𝑃) ∘ ◡𝑄))
145	2, 3	pmtrfconj 19452	. . . . . . 7 ⊢ ((𝑃 ∈ 𝑇 ∧ 𝑄:𝐷–1-1-onto→𝐷) → ((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∈ 𝑇)
146	12, 31, 145	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∈ 𝑇)
147	144, 146	eqeltrd 2835	. . . . 5 ⊢ (𝜑 → (𝑄 ∘ (𝑃 ∘ 𝑄)) ∈ 𝑇)
148	147	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑄 ∘ (𝑃 ∘ 𝑄)) ∈ 𝑇)
149	5	coeq1d 5846	. . . . . . 7 ⊢ (𝜑 → ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄)) = (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄)))
150		fcoi2 6758	. . . . . . . 8 ⊢ ((𝑃 ∘ 𝑄):𝐷⟶𝐷 → (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄)) = (𝑃 ∘ 𝑄))
151	35, 150	syl 17	. . . . . . 7 ⊢ (𝜑 → (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄)) = (𝑃 ∘ 𝑄))
152	149, 151	eqtr2d 2772	. . . . . 6 ⊢ (𝜑 → (𝑃 ∘ 𝑄) = ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄)))
153		coass 6259	. . . . . 6 ⊢ ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄)) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄)))
154	152, 153	eqtrdi 2787	. . . . 5 ⊢ (𝜑 → (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))))
155	154	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))))
156		f1ofn 6824	. . . . . . . . . 10 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → 𝑄 Fn 𝐷)
157	31, 156	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 Fn 𝐷)
158		fnelnfp 7174	. . . . . . . . 9 ⊢ ((𝑄 Fn 𝐷 ∧ 𝐴 ∈ 𝐷) → (𝐴 ∈ dom (𝑄 ∖ I ) ↔ (𝑄‘𝐴) ≠ 𝐴))
159	157, 78, 158	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ∈ dom (𝑄 ∖ I ) ↔ (𝑄‘𝐴) ≠ 𝐴))
160	159	necon2bbid 2976	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘𝐴) = 𝐴 ↔ ¬ 𝐴 ∈ dom (𝑄 ∖ I )))
161	160	biimpar 477	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑄‘𝐴) = 𝐴)
162		fnfvima 7230	. . . . . . . 8 ⊢ ((𝑄 Fn 𝐷 ∧ dom (𝑃 ∖ I ) ⊆ 𝐷 ∧ 𝐴 ∈ dom (𝑃 ∖ I )) → (𝑄‘𝐴) ∈ (𝑄 “ dom (𝑃 ∖ I )))
163	157, 77, 41, 162	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → (𝑄‘𝐴) ∈ (𝑄 “ dom (𝑃 ∖ I )))
164	163	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑄‘𝐴) ∈ (𝑄 “ dom (𝑃 ∖ I )))
165	161, 164	eqeltrrd 2836	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝐴 ∈ (𝑄 “ dom (𝑃 ∖ I )))
166	144	difeq1d 4105	. . . . . . . 8 ⊢ (𝜑 → ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ))
167	166	dmeqd 5890	. . . . . . 7 ⊢ (𝜑 → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ))
168		f1omvdconj 19432	. . . . . . . 8 ⊢ ((𝑃:𝐷⟶𝐷 ∧ 𝑄:𝐷–1-1-onto→𝐷) → dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
169	29, 31, 168	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
170	167, 169	eqtrd 2771	. . . . . 6 ⊢ (𝜑 → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
171	170	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
172	165, 171	eleqtrrd 2838	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ))
173		simpr 484	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → ¬ 𝐴 ∈ dom (𝑄 ∖ I ))
174		coeq1 5842	. . . . . . 7 ⊢ (𝑟 = 𝑄 → (𝑟 ∘ 𝑠) = (𝑄 ∘ 𝑠))
175	174	eqeq2d 2747	. . . . . 6 ⊢ (𝑟 = 𝑄 → ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠)))
176		difeq1 4099	. . . . . . . . 9 ⊢ (𝑟 = 𝑄 → (𝑟 ∖ I ) = (𝑄 ∖ I ))
177	176	dmeqd 5890	. . . . . . . 8 ⊢ (𝑟 = 𝑄 → dom (𝑟 ∖ I ) = dom (𝑄 ∖ I ))
178	177	eleq2d 2821	. . . . . . 7 ⊢ (𝑟 = 𝑄 → (𝐴 ∈ dom (𝑟 ∖ I ) ↔ 𝐴 ∈ dom (𝑄 ∖ I )))
179	178	notbid 318	. . . . . 6 ⊢ (𝑟 = 𝑄 → (¬ 𝐴 ∈ dom (𝑟 ∖ I ) ↔ ¬ 𝐴 ∈ dom (𝑄 ∖ I )))
180	175, 179	3anbi13d 1440	. . . . 5 ⊢ (𝑟 = 𝑄 → (((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I ))))
181		coeq2 5843	. . . . . . 7 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝑄 ∘ 𝑠) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))))
182	181	eqeq2d 2747	. . . . . 6 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → ((𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄)))))
183		difeq1 4099	. . . . . . . 8 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝑠 ∖ I ) = ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ))
184	183	dmeqd 5890	. . . . . . 7 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → dom (𝑠 ∖ I ) = dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ))
185	184	eleq2d 2821	. . . . . 6 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝐴 ∈ dom (𝑠 ∖ I ) ↔ 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I )))
186	182, 185	3anbi12d 1439	. . . . 5 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (((𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))) ∧ 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I ))))
187	180, 186	rspc2ev 3619	. . . 4 ⊢ ((𝑄 ∈ 𝑇 ∧ (𝑄 ∘ (𝑃 ∘ 𝑄)) ∈ 𝑇 ∧ ((𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))) ∧ 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I ))) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))
188	138, 148, 155, 172, 173, 187	syl113anc 1384	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))
189	188	olcd 874	. 2 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
190	137, 189	pm2.61dan 812	1 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2933  ∃wrex 3061  Vcvv 3464   ∖ cdif 3928   ⊆ wss 3931  ifcif 4505  {csn 4606  {cpr 4608  ∪ cuni 4888   class class class wbr 5124   I cid 5552  ^◡ccnv 5658  dom cdm 5659  ran crn 5660   ↾ cres 5661   “ cima 5662   ∘ ccom 5663   Fn wfn 6531  ⟶wf 6532  –1-1-onto→wf1o 6535  ‘cfv 6536  ωcom 7866  2_oc2o 8479   ≈ cen 8961  Fincfn 8964  pmTrspcpmtr 19427

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-om 7867  df-1o 8485  df-2o 8486  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-pmtr 19428

This theorem is referenced by:  psgnunilem2  19481