Theorem psgnunilem1 19101

Description: Lemma for psgnuni 19107. 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 19069	. . . . . . . 8 ⊢ (𝑄 ∈ 𝑇 → (𝑄 ∘ 𝑄) = ( I ↾ 𝐷))
5	1, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∘ 𝑄) = ( I ↾ 𝐷))
6		coeq1 5766	. . . . . . . 8 ⊢ (𝑃 = 𝑄 → (𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑄))
7	6	eqeq1d 2740	. . . . . . 7 ⊢ (𝑃 = 𝑄 → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ↔ (𝑄 ∘ 𝑄) = ( I ↾ 𝐷)))
8	5, 7	syl5ibrcom 246	. . . . . 6 ⊢ (𝜑 → (𝑃 = 𝑄 → (𝑃 ∘ 𝑄) = ( I ↾ 𝐷)))
9	8	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑃 = 𝑄 → (𝑃 ∘ 𝑄) = ( I ↾ 𝐷)))
10	9	imp 407	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 = 𝑄) → (𝑃 ∘ 𝑄) = ( I ↾ 𝐷))
11	10	orcd 870	. . 3 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 = 𝑄) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
12		psgnunilem1.p	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ 𝑇)
13	2, 3	pmtrfcnv 19072	. . . . . . . . . 10 ⊢ (𝑃 ∈ 𝑇 → ◡𝑃 = 𝑃)
14	12, 13	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ◡𝑃 = 𝑃)
15	14	eqcomd 2744	. . . . . . . 8 ⊢ (𝜑 → 𝑃 = ◡𝑃)
16	15	coeq2d 5771	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ 𝑃) = ((𝑃 ∘ 𝑄) ∘ ◡𝑃))
17	2, 3	pmtrff1o 19071	. . . . . . . . 9 ⊢ (𝑃 ∈ 𝑇 → 𝑃:𝐷–1-1-onto→𝐷)
18	12, 17	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑃:𝐷–1-1-onto→𝐷)
19	2, 3	pmtrfconj 19074	. . . . . . . 8 ⊢ ((𝑄 ∈ 𝑇 ∧ 𝑃:𝐷–1-1-onto→𝐷) → ((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∈ 𝑇)
20	1, 18, 19	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∈ 𝑇)
21	16, 20	eqeltrd 2839	. . . . . 6 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ 𝑃) ∈ 𝑇)
22	21	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∘ 𝑄) ∘ 𝑃) ∈ 𝑇)
23	12	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → 𝑃 ∈ 𝑇)
24		coass 6169	. . . . . . 7 ⊢ (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃) = ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃))
25	2, 3	pmtrfinv 19069	. . . . . . . . . 10 ⊢ (𝑃 ∈ 𝑇 → (𝑃 ∘ 𝑃) = ( I ↾ 𝐷))
26	12, 25	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ∘ 𝑃) = ( I ↾ 𝐷))
27	26	coeq2d 5771	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃)) = ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷)))
28		f1of 6716	. . . . . . . . . . 11 ⊢ (𝑃:𝐷–1-1-onto→𝐷 → 𝑃:𝐷⟶𝐷)
29	18, 28	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃:𝐷⟶𝐷)
30	2, 3	pmtrff1o 19071	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ 𝑇 → 𝑄:𝐷–1-1-onto→𝐷)
31	1, 30	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄:𝐷–1-1-onto→𝐷)
32		f1of 6716	. . . . . . . . . . 11 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → 𝑄:𝐷⟶𝐷)
33	31, 32	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:𝐷⟶𝐷)
34		fco 6624	. . . . . . . . . 10 ⊢ ((𝑃:𝐷⟶𝐷 ∧ 𝑄:𝐷⟶𝐷) → (𝑃 ∘ 𝑄):𝐷⟶𝐷)
35	29, 33, 34	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ∘ 𝑄):𝐷⟶𝐷)
36		fcoi1 6648	. . . . . . . . 9 ⊢ ((𝑃 ∘ 𝑄):𝐷⟶𝐷 → ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷)) = (𝑃 ∘ 𝑄))
37	35, 36	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷)) = (𝑃 ∘ 𝑄))
38	27, 37	eqtrd 2778	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃)) = (𝑃 ∘ 𝑄))
39	24, 38	eqtr2id 2791	. . . . . 6 ⊢ (𝜑 → (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃))
40	39	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃))
41		psgnunilem1.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ dom (𝑃 ∖ I ))
42	41	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → 𝐴 ∈ dom (𝑃 ∖ I ))
43	18	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝑃:𝐷–1-1-onto→𝐷)
44	31	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝑄:𝐷–1-1-onto→𝐷)
45	2, 3	pmtrfb 19073	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ 𝑇 ↔ (𝐷 ∈ V ∧ 𝑃:𝐷–1-1-onto→𝐷 ∧ dom (𝑃 ∖ I ) ≈ 2o))
46	45	simp3bi 1146	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ 𝑇 → dom (𝑃 ∖ I ) ≈ 2o)
47	12, 46	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → dom (𝑃 ∖ I ) ≈ 2o)
48	47	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) ≈ 2o)
49		2onn 8472	. . . . . . . . . . . . . . 15 ⊢ 2o ∈ ω
50		nnfi 8950	. . . . . . . . . . . . . . 15 ⊢ (2o ∈ ω → 2o ∈ Fin)
51	49, 50	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 2o ∈ Fin
52	2, 3	pmtrfb 19073	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄 ∈ 𝑇 ↔ (𝐷 ∈ V ∧ 𝑄:𝐷–1-1-onto→𝐷 ∧ dom (𝑄 ∖ I ) ≈ 2o))
53	52	simp3bi 1146	. . . . . . . . . . . . . . . 16 ⊢ (𝑄 ∈ 𝑇 → dom (𝑄 ∖ I ) ≈ 2o)
54	1, 53	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑄 ∖ I ) ≈ 2o)
55		enfi 8973	. . . . . . . . . . . . . . 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 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑄 ∖ I ) ∈ Fin)
59	41	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝐴 ∈ dom (𝑃 ∖ I ))
60		en2eleq 9764	. . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝐴 ∈ dom (𝑄 ∖ I ))
63		f1ofn 6717	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃:𝐷–1-1-onto→𝐷 → 𝑃 Fn 𝐷)
64	18, 63	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 Fn 𝐷)
65	64	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝑃 Fn 𝐷)
66		fimass 6621	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃:𝐷⟶𝐷 → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷)
67	29, 66	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷)
68	67	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷)
69		simprr 770	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))
70		fnfvima 7109	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 Fn 𝐷 ∧ (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷 ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))) → (𝑃‘𝐴) ∈ (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))))
71	65, 68, 69, 70	syl3anc 1370	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃‘𝐴) ∈ (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))))
72		difss 4066	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∖ I ) ⊆ 𝑃
73		dmss 5811	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃 ∖ I ) ⊆ 𝑃 → dom (𝑃 ∖ I ) ⊆ dom 𝑃)
74	72, 73	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom (𝑃 ∖ I ) ⊆ dom 𝑃
75		f1odm 6720	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:𝐷–1-1-onto→𝐷 → dom 𝑃 = 𝐷)
76	18, 75	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → dom 𝑃 = 𝐷)
77	74, 76	sseqtrid 3973	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → dom (𝑃 ∖ I ) ⊆ 𝐷)
78	77, 41	sseldd 3922	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
79		eqid 2738	. . . . . . . . . . . . . . . . . . 19 ⊢ dom (𝑃 ∖ I ) = dom (𝑃 ∖ I )
80	2, 3, 79	pmtrffv 19067	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ 𝑇 ∧ 𝐴 ∈ 𝐷) → (𝑃‘𝐴) = if(𝐴 ∈ dom (𝑃 ∖ I ), ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}), 𝐴))
81	12, 78, 80	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃‘𝐴) = if(𝐴 ∈ dom (𝑃 ∖ I ), ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}), 𝐴))
82	41	iftrued 4467	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝐴 ∈ dom (𝑃 ∖ I ), ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}), 𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}))
83	81, 82	eqtrd 2778	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃‘𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}))
84	83	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃‘𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}))
85		imaco 6155	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∘ 𝑃) “ dom (𝑄 ∖ I )) = (𝑃 “ (𝑃 “ dom (𝑄 ∖ I )))
86	26	imaeq1d 5968	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑃 ∘ 𝑃) “ dom (𝑄 ∖ I )) = (( I ↾ 𝐷) “ dom (𝑄 ∖ I )))
87		difss 4066	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄 ∖ I ) ⊆ 𝑄
88		dmss 5811	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑄 ∖ I ) ⊆ 𝑄 → dom (𝑄 ∖ I ) ⊆ dom 𝑄)
89	87, 88	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom (𝑄 ∖ I ) ⊆ dom 𝑄
90		f1odm 6720	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → dom 𝑄 = 𝐷)
91	89, 90	sseqtrid 3973	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → dom (𝑄 ∖ I ) ⊆ 𝐷)
92	31, 91	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → dom (𝑄 ∖ I ) ⊆ 𝐷)
93		resiima 5984	. . . . . . . . . . . . . . . . . . 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 2792	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))) = dom (𝑄 ∖ I ))
97	96	adantr 481	. . . . . . . . . . . . . . 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 4755	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → {𝐴, ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})} ⊆ dom (𝑄 ∖ I ))
100	61, 99	eqsstrd 3959	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) ⊆ dom (𝑄 ∖ I ))
101	54	ensymd 8791	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2o ≈ dom (𝑄 ∖ I ))
102		entr 8792	. . . . . . . . . . . . . 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 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I ))
105		fisseneq 9034	. . . . . . . . . . . 12 ⊢ ((dom (𝑄 ∖ I ) ∈ Fin ∧ dom (𝑃 ∖ I ) ⊆ dom (𝑄 ∖ I ) ∧ dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I )) → dom (𝑃 ∖ I ) = dom (𝑄 ∖ I ))
106	58, 100, 104, 105	syl3anc 1370	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) = dom (𝑄 ∖ I ))
107	106	eqcomd 2744	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑄 ∖ I ) = dom (𝑃 ∖ I ))
108		f1otrspeq 19055	. . . . . . . . . 10 ⊢ (((𝑃:𝐷–1-1-onto→𝐷 ∧ 𝑄:𝐷–1-1-onto→𝐷) ∧ (dom (𝑃 ∖ I ) ≈ 2o ∧ dom (𝑄 ∖ I ) = dom (𝑃 ∖ I ))) → 𝑃 = 𝑄)
109	43, 44, 48, 107, 108	syl22anc 836	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝑃 = 𝑄)
110	109	expr 457	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )) → 𝑃 = 𝑄))
111	110	necon3ad 2956	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑃 ≠ 𝑄 → ¬ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))))
112	111	imp 407	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ¬ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))
113	16	difeq1d 4056	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) = (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ))
114	113	dmeqd 5814	. . . . . . . . 9 ⊢ (𝜑 → dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) = dom (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ))
115		f1omvdconj 19054	. . . . . . . . . 10 ⊢ ((𝑄:𝐷⟶𝐷 ∧ 𝑃:𝐷–1-1-onto→𝐷) → dom (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ) = (𝑃 “ dom (𝑄 ∖ I )))
116	33, 18, 115	syl2anc 584	. . . . . . . . 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 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → (𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) ↔ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))))
120	112, 119	mtbird 325	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))
121		coeq1 5766	. . . . . . . 8 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝑟 ∘ 𝑠) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠))
122	121	eqeq2d 2749	. . . . . . 7 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠)))
123		difeq1 4050	. . . . . . . . . 10 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝑟 ∖ I ) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))
124	123	dmeqd 5814	. . . . . . . . 9 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → dom (𝑟 ∖ I ) = dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))
125	124	eleq2d 2824	. . . . . . . 8 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝐴 ∈ dom (𝑟 ∖ I ) ↔ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )))
126	125	notbid 318	. . . . . . 7 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (¬ 𝐴 ∈ dom (𝑟 ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )))
127	122, 126	3anbi13d 1437	. . . . . 6 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))))
128		coeq2 5767	. . . . . . . 8 ⊢ (𝑠 = 𝑃 → (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃))
129	128	eqeq2d 2749	. . . . . . 7 ⊢ (𝑠 = 𝑃 → ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃)))
130		difeq1 4050	. . . . . . . . 9 ⊢ (𝑠 = 𝑃 → (𝑠 ∖ I ) = (𝑃 ∖ I ))
131	130	dmeqd 5814	. . . . . . . 8 ⊢ (𝑠 = 𝑃 → dom (𝑠 ∖ I ) = dom (𝑃 ∖ I ))
132	131	eleq2d 2824	. . . . . . 7 ⊢ (𝑠 = 𝑃 → (𝐴 ∈ dom (𝑠 ∖ I ) ↔ 𝐴 ∈ dom (𝑃 ∖ I )))
133	129, 132	3anbi12d 1436	. . . . . 6 ⊢ (𝑠 = 𝑃 → (((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃) ∧ 𝐴 ∈ dom (𝑃 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))))
134	127, 133	rspc2ev 3572	. . . . 5 ⊢ ((((𝑃 ∘ 𝑄) ∘ 𝑃) ∈ 𝑇 ∧ 𝑃 ∈ 𝑇 ∧ ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃) ∧ 𝐴 ∈ dom (𝑃 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))
135	22, 23, 40, 42, 120, 134	syl113anc 1381	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))
136	135	olcd 871	. . 3 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
137	11, 136	pm2.61dane 3032	. 2 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
138	1	adantr 481	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝑄 ∈ 𝑇)
139		coass 6169	. . . . . . 7 ⊢ ((𝑄 ∘ 𝑃) ∘ 𝑄) = (𝑄 ∘ (𝑃 ∘ 𝑄))
140	2, 3	pmtrfcnv 19072	. . . . . . . . . 10 ⊢ (𝑄 ∈ 𝑇 → ◡𝑄 = 𝑄)
141	1, 140	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ◡𝑄 = 𝑄)
142	141	eqcomd 2744	. . . . . . . 8 ⊢ (𝜑 → 𝑄 = ◡𝑄)
143	142	coeq2d 5771	. . . . . . 7 ⊢ (𝜑 → ((𝑄 ∘ 𝑃) ∘ 𝑄) = ((𝑄 ∘ 𝑃) ∘ ◡𝑄))
144	139, 143	eqtr3id 2792	. . . . . 6 ⊢ (𝜑 → (𝑄 ∘ (𝑃 ∘ 𝑄)) = ((𝑄 ∘ 𝑃) ∘ ◡𝑄))
145	2, 3	pmtrfconj 19074	. . . . . . 7 ⊢ ((𝑃 ∈ 𝑇 ∧ 𝑄:𝐷–1-1-onto→𝐷) → ((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∈ 𝑇)
146	12, 31, 145	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∈ 𝑇)
147	144, 146	eqeltrd 2839	. . . . 5 ⊢ (𝜑 → (𝑄 ∘ (𝑃 ∘ 𝑄)) ∈ 𝑇)
148	147	adantr 481	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑄 ∘ (𝑃 ∘ 𝑄)) ∈ 𝑇)
149	5	coeq1d 5770	. . . . . . 7 ⊢ (𝜑 → ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄)) = (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄)))
150		fcoi2 6649	. . . . . . . 8 ⊢ ((𝑃 ∘ 𝑄):𝐷⟶𝐷 → (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄)) = (𝑃 ∘ 𝑄))
151	35, 150	syl 17	. . . . . . 7 ⊢ (𝜑 → (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄)) = (𝑃 ∘ 𝑄))
152	149, 151	eqtr2d 2779	. . . . . 6 ⊢ (𝜑 → (𝑃 ∘ 𝑄) = ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄)))
153		coass 6169	. . . . . 6 ⊢ ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄)) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄)))
154	152, 153	eqtrdi 2794	. . . . 5 ⊢ (𝜑 → (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))))
155	154	adantr 481	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))))
156		f1ofn 6717	. . . . . . . . . 10 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → 𝑄 Fn 𝐷)
157	31, 156	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 Fn 𝐷)
158		fnelnfp 7049	. . . . . . . . 9 ⊢ ((𝑄 Fn 𝐷 ∧ 𝐴 ∈ 𝐷) → (𝐴 ∈ dom (𝑄 ∖ I ) ↔ (𝑄‘𝐴) ≠ 𝐴))
159	157, 78, 158	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ∈ dom (𝑄 ∖ I ) ↔ (𝑄‘𝐴) ≠ 𝐴))
160	159	necon2bbid 2987	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘𝐴) = 𝐴 ↔ ¬ 𝐴 ∈ dom (𝑄 ∖ I )))
161	160	biimpar 478	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑄‘𝐴) = 𝐴)
162		fnfvima 7109	. . . . . . . 8 ⊢ ((𝑄 Fn 𝐷 ∧ dom (𝑃 ∖ I ) ⊆ 𝐷 ∧ 𝐴 ∈ dom (𝑃 ∖ I )) → (𝑄‘𝐴) ∈ (𝑄 “ dom (𝑃 ∖ I )))
163	157, 77, 41, 162	syl3anc 1370	. . . . . . 7 ⊢ (𝜑 → (𝑄‘𝐴) ∈ (𝑄 “ dom (𝑃 ∖ I )))
164	163	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑄‘𝐴) ∈ (𝑄 “ dom (𝑃 ∖ I )))
165	161, 164	eqeltrrd 2840	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝐴 ∈ (𝑄 “ dom (𝑃 ∖ I )))
166	144	difeq1d 4056	. . . . . . . 8 ⊢ (𝜑 → ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ))
167	166	dmeqd 5814	. . . . . . 7 ⊢ (𝜑 → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ))
168		f1omvdconj 19054	. . . . . . . 8 ⊢ ((𝑃:𝐷⟶𝐷 ∧ 𝑄:𝐷–1-1-onto→𝐷) → dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
169	29, 31, 168	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
170	167, 169	eqtrd 2778	. . . . . 6 ⊢ (𝜑 → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
171	170	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
172	165, 171	eleqtrrd 2842	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ))
173		simpr 485	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → ¬ 𝐴 ∈ dom (𝑄 ∖ I ))
174		coeq1 5766	. . . . . . 7 ⊢ (𝑟 = 𝑄 → (𝑟 ∘ 𝑠) = (𝑄 ∘ 𝑠))
175	174	eqeq2d 2749	. . . . . 6 ⊢ (𝑟 = 𝑄 → ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠)))
176		difeq1 4050	. . . . . . . . 9 ⊢ (𝑟 = 𝑄 → (𝑟 ∖ I ) = (𝑄 ∖ I ))
177	176	dmeqd 5814	. . . . . . . 8 ⊢ (𝑟 = 𝑄 → dom (𝑟 ∖ I ) = dom (𝑄 ∖ I ))
178	177	eleq2d 2824	. . . . . . 7 ⊢ (𝑟 = 𝑄 → (𝐴 ∈ dom (𝑟 ∖ I ) ↔ 𝐴 ∈ dom (𝑄 ∖ I )))
179	178	notbid 318	. . . . . 6 ⊢ (𝑟 = 𝑄 → (¬ 𝐴 ∈ dom (𝑟 ∖ I ) ↔ ¬ 𝐴 ∈ dom (𝑄 ∖ I )))
180	175, 179	3anbi13d 1437	. . . . 5 ⊢ (𝑟 = 𝑄 → (((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I ))))
181		coeq2 5767	. . . . . . 7 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝑄 ∘ 𝑠) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))))
182	181	eqeq2d 2749	. . . . . 6 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → ((𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄)))))
183		difeq1 4050	. . . . . . . 8 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝑠 ∖ I ) = ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ))
184	183	dmeqd 5814	. . . . . . 7 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → dom (𝑠 ∖ I ) = dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ))
185	184	eleq2d 2824	. . . . . 6 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝐴 ∈ dom (𝑠 ∖ I ) ↔ 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I )))
186	182, 185	3anbi12d 1436	. . . . 5 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (((𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))) ∧ 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I ))))
187	180, 186	rspc2ev 3572	. . . 4 ⊢ ((𝑄 ∈ 𝑇 ∧ (𝑄 ∘ (𝑃 ∘ 𝑄)) ∈ 𝑇 ∧ ((𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))) ∧ 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I ))) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))
188	138, 148, 155, 172, 173, 187	syl113anc 1381	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))
189	188	olcd 871	. 2 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
190	137, 189	pm2.61dan 810	1 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106   ≠ wne 2943  ∃wrex 3065  Vcvv 3432   ∖ cdif 3884   ⊆ wss 3887  ifcif 4459  {csn 4561  {cpr 4563  ∪ cuni 4839   class class class wbr 5074   I cid 5488  ^◡ccnv 5588  dom cdm 5589  ran crn 5590   ↾ cres 5591   “ cima 5592   ∘ ccom 5593   Fn wfn 6428  ⟶wf 6429  –1-1-onto→wf1o 6432  ‘cfv 6433  ωcom 7712  2_oc2o 8291   ≈ cen 8730  Fincfn 8733  pmTrspcpmtr 19049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-om 7713  df-1o 8297  df-2o 8298  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-pmtr 19050

This theorem is referenced by:  psgnunilem2  19103