Metamath Proof Explorer

Theorem psgnunilem1

Description: Lemma for psgnuni . 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)

Ref Expression
Hypotheses psgnunilem1.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
psgnunilem1.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
psgnunilem1.p ⊢ ( 𝜑 → 𝑃 ∈ 𝑇 )
psgnunilem1.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑇 )
psgnunilem1.a ⊢ ( 𝜑 → 𝐴 ∈ dom ( 𝑃 ∖ I ) )
Assertion psgnunilem1 ( 𝜑 → ( ( 𝑃 ∘ 𝑄 ) = ( I ↾ 𝐷 ) ∨ ∃ 𝑟 ∈ 𝑇 ∃ 𝑠 ∈ 𝑇 ( ( 𝑃 ∘ 𝑄 ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) )

Proof

Step Hyp Ref Expression
1 psgnunilem1.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
2 psgnunilem1.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3 psgnunilem1.p ⊢ ( 𝜑 → 𝑃 ∈ 𝑇 )
4 psgnunilem1.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑇 )
5 psgnunilem1.a ⊢ ( 𝜑 → 𝐴 ∈ dom ( 𝑃 ∖ I ) )
6 eqid ⊢ ( pmTrsp ‘ 𝐷 ) = ( pmTrsp ‘ 𝐷 )
7 6 1 pmtrfinv ⊢ ( 𝑄 ∈ 𝑇 → ( 𝑄 ∘ 𝑄 ) = ( I ↾ 𝐷 ) )
8 4 7 syl ⊢ ( 𝜑 → ( 𝑄 ∘ 𝑄 ) = ( I ↾ 𝐷 ) )
9 coeq1 ⊢ ( 𝑃 = 𝑄 → ( 𝑃 ∘ 𝑄 ) = ( 𝑄 ∘ 𝑄 ) )
10 9 eqeq1d ⊢ ( 𝑃 = 𝑄 → ( ( 𝑃 ∘ 𝑄 ) = ( I ↾ 𝐷 ) ↔ ( 𝑄 ∘ 𝑄 ) = ( I ↾ 𝐷 ) ) )
11 8 10 syl5ibrcom ⊢ ( 𝜑 → ( 𝑃 = 𝑄 → ( 𝑃 ∘ 𝑄 ) = ( I ↾ 𝐷 ) ) )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) → ( 𝑃 = 𝑄 → ( 𝑃 ∘ 𝑄 ) = ( I ↾ 𝐷 ) ) )
13 12 imp ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) ∧ 𝑃 = 𝑄 ) → ( 𝑃 ∘ 𝑄 ) = ( I ↾ 𝐷 ) )
14 13 orcd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) ∧ 𝑃 = 𝑄 ) → ( ( 𝑃 ∘ 𝑄 ) = ( I ↾ 𝐷 ) ∨ ∃ 𝑟 ∈ 𝑇 ∃ 𝑠 ∈ 𝑇 ( ( 𝑃 ∘ 𝑄 ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) )
15 6 1 pmtrfcnv ⊢ ( 𝑃 ∈ 𝑇 → ◡ 𝑃 = 𝑃 )
16 3 15 syl ⊢ ( 𝜑 → ◡ 𝑃 = 𝑃 )
17 16 eqcomd ⊢ ( 𝜑 → 𝑃 = ◡ 𝑃 )
18 17 coeq2d ⊢ ( 𝜑 → ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) = ( ( 𝑃 ∘ 𝑄 ) ∘ ◡ 𝑃 ) )
19 6 1 pmtrff1o ⊢ ( 𝑃 ∈ 𝑇 → 𝑃 : 𝐷 –1-1-onto→ 𝐷 )
20 3 19 syl ⊢ ( 𝜑 → 𝑃 : 𝐷 –1-1-onto→ 𝐷 )
21 6 1 pmtrfconj ⊢ ( ( 𝑄 ∈ 𝑇 ∧ 𝑃 : 𝐷 –1-1-onto→ 𝐷 ) → ( ( 𝑃 ∘ 𝑄 ) ∘ ◡ 𝑃 ) ∈ 𝑇 )
22 4 20 21 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 ∘ 𝑄 ) ∘ ◡ 𝑃 ) ∈ 𝑇 )
23 18 22 eqeltrd ⊢ ( 𝜑 → ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∈ 𝑇 )
24 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∈ 𝑇 )
25 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝑃 ∈ 𝑇 )
26 coass ⊢ ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∘ 𝑃 ) = ( ( 𝑃 ∘ 𝑄 ) ∘ ( 𝑃 ∘ 𝑃 ) )
27 6 1 pmtrfinv ⊢ ( 𝑃 ∈ 𝑇 → ( 𝑃 ∘ 𝑃 ) = ( I ↾ 𝐷 ) )
28 3 27 syl ⊢ ( 𝜑 → ( 𝑃 ∘ 𝑃 ) = ( I ↾ 𝐷 ) )
29 28 coeq2d ⊢ ( 𝜑 → ( ( 𝑃 ∘ 𝑄 ) ∘ ( 𝑃 ∘ 𝑃 ) ) = ( ( 𝑃 ∘ 𝑄 ) ∘ ( I ↾ 𝐷 ) ) )
30 f1of ⊢ ( 𝑃 : 𝐷 –1-1-onto→ 𝐷 → 𝑃 : 𝐷 ⟶ 𝐷 )
31 20 30 syl ⊢ ( 𝜑 → 𝑃 : 𝐷 ⟶ 𝐷 )
32 6 1 pmtrff1o ⊢ ( 𝑄 ∈ 𝑇 → 𝑄 : 𝐷 –1-1-onto→ 𝐷 )
33 4 32 syl ⊢ ( 𝜑 → 𝑄 : 𝐷 –1-1-onto→ 𝐷 )
34 f1of ⊢ ( 𝑄 : 𝐷 –1-1-onto→ 𝐷 → 𝑄 : 𝐷 ⟶ 𝐷 )
35 33 34 syl ⊢ ( 𝜑 → 𝑄 : 𝐷 ⟶ 𝐷 )
36 fco ⊢ ( ( 𝑃 : 𝐷 ⟶ 𝐷 ∧ 𝑄 : 𝐷 ⟶ 𝐷 ) → ( 𝑃 ∘ 𝑄 ) : 𝐷 ⟶ 𝐷 )
37 31 35 36 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∘ 𝑄 ) : 𝐷 ⟶ 𝐷 )
38 fcoi1 ⊢ ( ( 𝑃 ∘ 𝑄 ) : 𝐷 ⟶ 𝐷 → ( ( 𝑃 ∘ 𝑄 ) ∘ ( I ↾ 𝐷 ) ) = ( 𝑃 ∘ 𝑄 ) )
39 37 38 syl ⊢ ( 𝜑 → ( ( 𝑃 ∘ 𝑄 ) ∘ ( I ↾ 𝐷 ) ) = ( 𝑃 ∘ 𝑄 ) )
40 29 39 eqtrd ⊢ ( 𝜑 → ( ( 𝑃 ∘ 𝑄 ) ∘ ( 𝑃 ∘ 𝑃 ) ) = ( 𝑃 ∘ 𝑄 ) )
41 26 40 syl5req ⊢ ( 𝜑 → ( 𝑃 ∘ 𝑄 ) = ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∘ 𝑃 ) )
42 41 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ∘ 𝑄 ) = ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∘ 𝑃 ) )
43 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝐴 ∈ dom ( 𝑃 ∖ I ) )
44 20 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → 𝑃 : 𝐷 –1-1-onto→ 𝐷 )
45 33 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → 𝑄 : 𝐷 –1-1-onto→ 𝐷 )
46 6 1 pmtrfb ⊢ ( 𝑃 ∈ 𝑇 ↔ ( 𝐷 ∈ V ∧ 𝑃 : 𝐷 –1-1-onto→ 𝐷 ∧ dom ( 𝑃 ∖ I ) ≈ 2o ) )
47 46 simp3bi ⊢ ( 𝑃 ∈ 𝑇 → dom ( 𝑃 ∖ I ) ≈ 2o )
48 3 47 syl ⊢ ( 𝜑 → dom ( 𝑃 ∖ I ) ≈ 2o )
49 48 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → dom ( 𝑃 ∖ I ) ≈ 2o )
50 2onn ⊢ 2o ∈ ω
51 nnfi ⊢ ( 2o ∈ ω → 2o ∈ Fin )
52 50 51 ax-mp ⊢ 2o ∈ Fin
53 6 1 pmtrfb ⊢ ( 𝑄 ∈ 𝑇 ↔ ( 𝐷 ∈ V ∧ 𝑄 : 𝐷 –1-1-onto→ 𝐷 ∧ dom ( 𝑄 ∖ I ) ≈ 2o ) )
54 53 simp3bi ⊢ ( 𝑄 ∈ 𝑇 → dom ( 𝑄 ∖ I ) ≈ 2o )
55 4 54 syl ⊢ ( 𝜑 → dom ( 𝑄 ∖ I ) ≈ 2o )
56 enfi ⊢ ( dom ( 𝑄 ∖ I ) ≈ 2o → ( dom ( 𝑄 ∖ I ) ∈ Fin ↔ 2o ∈ Fin ) )
57 55 56 syl ⊢ ( 𝜑 → ( dom ( 𝑄 ∖ I ) ∈ Fin ↔ 2o ∈ Fin ) )
58 52 57 mpbiri ⊢ ( 𝜑 → dom ( 𝑄 ∖ I ) ∈ Fin )
59 58 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → dom ( 𝑄 ∖ I ) ∈ Fin )
60 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → 𝐴 ∈ dom ( 𝑃 ∖ I ) )
61 en2eleq ⊢ ( ( 𝐴 ∈ dom ( 𝑃 ∖ I ) ∧ dom ( 𝑃 ∖ I ) ≈ 2o ) → dom ( 𝑃 ∖ I ) = { 𝐴 , ∪ ( dom ( 𝑃 ∖ I ) ∖ { 𝐴 } ) } )
62 60 49 61 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → dom ( 𝑃 ∖ I ) = { 𝐴 , ∪ ( dom ( 𝑃 ∖ I ) ∖ { 𝐴 } ) } )
63 simprl ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → 𝐴 ∈ dom ( 𝑄 ∖ I ) )
64 f1ofn ⊢ ( 𝑃 : 𝐷 –1-1-onto→ 𝐷 → 𝑃 Fn 𝐷 )
65 20 64 syl ⊢ ( 𝜑 → 𝑃 Fn 𝐷 )
66 65 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → 𝑃 Fn 𝐷 )
67 fimass ⊢ ( 𝑃 : 𝐷 ⟶ 𝐷 → ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ⊆ 𝐷 )
68 31 67 syl ⊢ ( 𝜑 → ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ⊆ 𝐷 )
69 68 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ⊆ 𝐷 )
70 simprr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) )
71 fnfvima ⊢ ( ( 𝑃 Fn 𝐷 ∧ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ⊆ 𝐷 ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) → ( 𝑃 ‘ 𝐴 ) ∈ ( 𝑃 “ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) )
72 66 69 70 71 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → ( 𝑃 ‘ 𝐴 ) ∈ ( 𝑃 “ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) )
73 difss ⊢ ( 𝑃 ∖ I ) ⊆ 𝑃
74 dmss ⊢ ( ( 𝑃 ∖ I ) ⊆ 𝑃 → dom ( 𝑃 ∖ I ) ⊆ dom 𝑃 )
75 73 74 ax-mp ⊢ dom ( 𝑃 ∖ I ) ⊆ dom 𝑃
76 f1odm ⊢ ( 𝑃 : 𝐷 –1-1-onto→ 𝐷 → dom 𝑃 = 𝐷 )
77 20 76 syl ⊢ ( 𝜑 → dom 𝑃 = 𝐷 )
78 75 77 sseqtrid ⊢ ( 𝜑 → dom ( 𝑃 ∖ I ) ⊆ 𝐷 )
79 78 5 sseldd ⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
80 eqid ⊢ dom ( 𝑃 ∖ I ) = dom ( 𝑃 ∖ I )
81 6 1 80 pmtrffv ⊢ ( ( 𝑃 ∈ 𝑇 ∧ 𝐴 ∈ 𝐷 ) → ( 𝑃 ‘ 𝐴 ) = if ( 𝐴 ∈ dom ( 𝑃 ∖ I ) , ∪ ( dom ( 𝑃 ∖ I ) ∖ { 𝐴 } ) , 𝐴 ) )
82 3 79 81 syl2anc ⊢ ( 𝜑 → ( 𝑃 ‘ 𝐴 ) = if ( 𝐴 ∈ dom ( 𝑃 ∖ I ) , ∪ ( dom ( 𝑃 ∖ I ) ∖ { 𝐴 } ) , 𝐴 ) )
83 5 iftrued ⊢ ( 𝜑 → if ( 𝐴 ∈ dom ( 𝑃 ∖ I ) , ∪ ( dom ( 𝑃 ∖ I ) ∖ { 𝐴 } ) , 𝐴 ) = ∪ ( dom ( 𝑃 ∖ I ) ∖ { 𝐴 } ) )
84 82 83 eqtrd ⊢ ( 𝜑 → ( 𝑃 ‘ 𝐴 ) = ∪ ( dom ( 𝑃 ∖ I ) ∖ { 𝐴 } ) )
85 84 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → ( 𝑃 ‘ 𝐴 ) = ∪ ( dom ( 𝑃 ∖ I ) ∖ { 𝐴 } ) )
86 imaco ⊢ ( ( 𝑃 ∘ 𝑃 ) “ dom ( 𝑄 ∖ I ) ) = ( 𝑃 “ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) )
87 28 imaeq1d ⊢ ( 𝜑 → ( ( 𝑃 ∘ 𝑃 ) “ dom ( 𝑄 ∖ I ) ) = ( ( I ↾ 𝐷 ) “ dom ( 𝑄 ∖ I ) ) )
88 difss ⊢ ( 𝑄 ∖ I ) ⊆ 𝑄
89 dmss ⊢ ( ( 𝑄 ∖ I ) ⊆ 𝑄 → dom ( 𝑄 ∖ I ) ⊆ dom 𝑄 )
90 88 89 ax-mp ⊢ dom ( 𝑄 ∖ I ) ⊆ dom 𝑄
91 f1odm ⊢ ( 𝑄 : 𝐷 –1-1-onto→ 𝐷 → dom 𝑄 = 𝐷 )
92 90 91 sseqtrid ⊢ ( 𝑄 : 𝐷 –1-1-onto→ 𝐷 → dom ( 𝑄 ∖ I ) ⊆ 𝐷 )
93 33 92 syl ⊢ ( 𝜑 → dom ( 𝑄 ∖ I ) ⊆ 𝐷 )
94 resiima ⊢ ( dom ( 𝑄 ∖ I ) ⊆ 𝐷 → ( ( I ↾ 𝐷 ) “ dom ( 𝑄 ∖ I ) ) = dom ( 𝑄 ∖ I ) )
95 93 94 syl ⊢ ( 𝜑 → ( ( I ↾ 𝐷 ) “ dom ( 𝑄 ∖ I ) ) = dom ( 𝑄 ∖ I ) )
96 87 95 eqtrd ⊢ ( 𝜑 → ( ( 𝑃 ∘ 𝑃 ) “ dom ( 𝑄 ∖ I ) ) = dom ( 𝑄 ∖ I ) )
97 86 96 eqtr3id ⊢ ( 𝜑 → ( 𝑃 “ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) = dom ( 𝑄 ∖ I ) )
98 97 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → ( 𝑃 “ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) = dom ( 𝑄 ∖ I ) )
99 72 85 98 3eltr3d ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → ∪ ( dom ( 𝑃 ∖ I ) ∖ { 𝐴 } ) ∈ dom ( 𝑄 ∖ I ) )
100 63 99 prssd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → { 𝐴 , ∪ ( dom ( 𝑃 ∖ I ) ∖ { 𝐴 } ) } ⊆ dom ( 𝑄 ∖ I ) )
101 62 100 eqsstrd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → dom ( 𝑃 ∖ I ) ⊆ dom ( 𝑄 ∖ I ) )
102 55 ensymd ⊢ ( 𝜑 → 2o ≈ dom ( 𝑄 ∖ I ) )
103 entr ⊢ ( ( dom ( 𝑃 ∖ I ) ≈ 2o ∧ 2o ≈ dom ( 𝑄 ∖ I ) ) → dom ( 𝑃 ∖ I ) ≈ dom ( 𝑄 ∖ I ) )
104 48 102 103 syl2anc ⊢ ( 𝜑 → dom ( 𝑃 ∖ I ) ≈ dom ( 𝑄 ∖ I ) )
105 104 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → dom ( 𝑃 ∖ I ) ≈ dom ( 𝑄 ∖ I ) )
106 fisseneq ⊢ ( ( dom ( 𝑄 ∖ I ) ∈ Fin ∧ dom ( 𝑃 ∖ I ) ⊆ dom ( 𝑄 ∖ I ) ∧ dom ( 𝑃 ∖ I ) ≈ dom ( 𝑄 ∖ I ) ) → dom ( 𝑃 ∖ I ) = dom ( 𝑄 ∖ I ) )
107 59 101 105 106 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → dom ( 𝑃 ∖ I ) = dom ( 𝑄 ∖ I ) )
108 107 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → dom ( 𝑄 ∖ I ) = dom ( 𝑃 ∖ I ) )
109 f1otrspeq ⊢ ( ( ( 𝑃 : 𝐷 –1-1-onto→ 𝐷 ∧ 𝑄 : 𝐷 –1-1-onto→ 𝐷 ) ∧ ( dom ( 𝑃 ∖ I ) ≈ 2o ∧ dom ( 𝑄 ∖ I ) = dom ( 𝑃 ∖ I ) ) ) → 𝑃 = 𝑄 )
110 44 45 49 108 109 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ∧ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) ) → 𝑃 = 𝑄 )
111 110 expr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) → ( 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) → 𝑃 = 𝑄 ) )
112 111 necon3ad ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) → ( 𝑃 ≠ 𝑄 → ¬ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) )
113 112 imp ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) ∧ 𝑃 ≠ 𝑄 ) → ¬ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) )
114 18 difeq1d ⊢ ( 𝜑 → ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∖ I ) = ( ( ( 𝑃 ∘ 𝑄 ) ∘ ◡ 𝑃 ) ∖ I ) )
115 114 dmeqd ⊢ ( 𝜑 → dom ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∖ I ) = dom ( ( ( 𝑃 ∘ 𝑄 ) ∘ ◡ 𝑃 ) ∖ I ) )
116 f1omvdconj ⊢ ( ( 𝑄 : 𝐷 ⟶ 𝐷 ∧ 𝑃 : 𝐷 –1-1-onto→ 𝐷 ) → dom ( ( ( 𝑃 ∘ 𝑄 ) ∘ ◡ 𝑃 ) ∖ I ) = ( 𝑃 “ dom ( 𝑄 ∖ I ) ) )
117 35 20 116 syl2anc ⊢ ( 𝜑 → dom ( ( ( 𝑃 ∘ 𝑄 ) ∘ ◡ 𝑃 ) ∖ I ) = ( 𝑃 “ dom ( 𝑄 ∖ I ) ) )
118 115 117 eqtrd ⊢ ( 𝜑 → dom ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∖ I ) = ( 𝑃 “ dom ( 𝑄 ∖ I ) ) )
119 118 eleq2d ⊢ ( 𝜑 → ( 𝐴 ∈ dom ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∖ I ) ↔ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) )
120 119 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝐴 ∈ dom ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∖ I ) ↔ 𝐴 ∈ ( 𝑃 “ dom ( 𝑄 ∖ I ) ) ) )
121 113 120 mtbird ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) ∧ 𝑃 ≠ 𝑄 ) → ¬ 𝐴 ∈ dom ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∖ I ) )
122 coeq1 ⊢ ( 𝑟 = ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) → ( 𝑟 ∘ 𝑠 ) = ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∘ 𝑠 ) )
123 122 eqeq2d ⊢ ( 𝑟 = ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) → ( ( 𝑃 ∘ 𝑄 ) = ( 𝑟 ∘ 𝑠 ) ↔ ( 𝑃 ∘ 𝑄 ) = ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∘ 𝑠 ) ) )
124 difeq1 ⊢ ( 𝑟 = ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) → ( 𝑟 ∖ I ) = ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∖ I ) )
125 124 dmeqd ⊢ ( 𝑟 = ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) → dom ( 𝑟 ∖ I ) = dom ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∖ I ) )
126 125 eleq2d ⊢ ( 𝑟 = ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) → ( 𝐴 ∈ dom ( 𝑟 ∖ I ) ↔ 𝐴 ∈ dom ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∖ I ) ) )
127 126 notbid ⊢ ( 𝑟 = ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) → ( ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ↔ ¬ 𝐴 ∈ dom ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∖ I ) ) )
128 123 127 3anbi13d ⊢ ( 𝑟 = ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) → ( ( ( 𝑃 ∘ 𝑄 ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ↔ ( ( 𝑃 ∘ 𝑄 ) = ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∖ I ) ) ) )
129 coeq2 ⊢ ( 𝑠 = 𝑃 → ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∘ 𝑠 ) = ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∘ 𝑃 ) )
130 129 eqeq2d ⊢ ( 𝑠 = 𝑃 → ( ( 𝑃 ∘ 𝑄 ) = ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∘ 𝑠 ) ↔ ( 𝑃 ∘ 𝑄 ) = ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∘ 𝑃 ) ) )
131 difeq1 ⊢ ( 𝑠 = 𝑃 → ( 𝑠 ∖ I ) = ( 𝑃 ∖ I ) )
132 131 dmeqd ⊢ ( 𝑠 = 𝑃 → dom ( 𝑠 ∖ I ) = dom ( 𝑃 ∖ I ) )
133 132 eleq2d ⊢ ( 𝑠 = 𝑃 → ( 𝐴 ∈ dom ( 𝑠 ∖ I ) ↔ 𝐴 ∈ dom ( 𝑃 ∖ I ) ) )
134 130 133 3anbi12d ⊢ ( 𝑠 = 𝑃 → ( ( ( 𝑃 ∘ 𝑄 ) = ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∖ I ) ) ↔ ( ( 𝑃 ∘ 𝑄 ) = ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∘ 𝑃 ) ∧ 𝐴 ∈ dom ( 𝑃 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∖ I ) ) ) )
135 128 134 rspc2ev ⊢ ( ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∈ 𝑇 ∧ 𝑃 ∈ 𝑇 ∧ ( ( 𝑃 ∘ 𝑄 ) = ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∘ 𝑃 ) ∧ 𝐴 ∈ dom ( 𝑃 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( ( ( 𝑃 ∘ 𝑄 ) ∘ 𝑃 ) ∖ I ) ) ) → ∃ 𝑟 ∈ 𝑇 ∃ 𝑠 ∈ 𝑇 ( ( 𝑃 ∘ 𝑄 ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) )
136 24 25 42 43 121 135 syl113anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) ∧ 𝑃 ≠ 𝑄 ) → ∃ 𝑟 ∈ 𝑇 ∃ 𝑠 ∈ 𝑇 ( ( 𝑃 ∘ 𝑄 ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) )
137 136 olcd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝑃 ∘ 𝑄 ) = ( I ↾ 𝐷 ) ∨ ∃ 𝑟 ∈ 𝑇 ∃ 𝑠 ∈ 𝑇 ( ( 𝑃 ∘ 𝑄 ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) )
138 14 137 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) → ( ( 𝑃 ∘ 𝑄 ) = ( I ↾ 𝐷 ) ∨ ∃ 𝑟 ∈ 𝑇 ∃ 𝑠 ∈ 𝑇 ( ( 𝑃 ∘ 𝑄 ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) )
139 4 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) → 𝑄 ∈ 𝑇 )
140 coass ⊢ ( ( 𝑄 ∘ 𝑃 ) ∘ 𝑄 ) = ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) )
141 6 1 pmtrfcnv ⊢ ( 𝑄 ∈ 𝑇 → ◡ 𝑄 = 𝑄 )
142 4 141 syl ⊢ ( 𝜑 → ◡ 𝑄 = 𝑄 )
143 142 eqcomd ⊢ ( 𝜑 → 𝑄 = ◡ 𝑄 )
144 143 coeq2d ⊢ ( 𝜑 → ( ( 𝑄 ∘ 𝑃 ) ∘ 𝑄 ) = ( ( 𝑄 ∘ 𝑃 ) ∘ ◡ 𝑄 ) )
145 140 144 eqtr3id ⊢ ( 𝜑 → ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) = ( ( 𝑄 ∘ 𝑃 ) ∘ ◡ 𝑄 ) )
146 6 1 pmtrfconj ⊢ ( ( 𝑃 ∈ 𝑇 ∧ 𝑄 : 𝐷 –1-1-onto→ 𝐷 ) → ( ( 𝑄 ∘ 𝑃 ) ∘ ◡ 𝑄 ) ∈ 𝑇 )
147 3 33 146 syl2anc ⊢ ( 𝜑 → ( ( 𝑄 ∘ 𝑃 ) ∘ ◡ 𝑄 ) ∈ 𝑇 )
148 145 147 eqeltrd ⊢ ( 𝜑 → ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ∈ 𝑇 )
149 148 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) → ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ∈ 𝑇 )
150 8 coeq1d ⊢ ( 𝜑 → ( ( 𝑄 ∘ 𝑄 ) ∘ ( 𝑃 ∘ 𝑄 ) ) = ( ( I ↾ 𝐷 ) ∘ ( 𝑃 ∘ 𝑄 ) ) )
151 fcoi2 ⊢ ( ( 𝑃 ∘ 𝑄 ) : 𝐷 ⟶ 𝐷 → ( ( I ↾ 𝐷 ) ∘ ( 𝑃 ∘ 𝑄 ) ) = ( 𝑃 ∘ 𝑄 ) )
152 37 151 syl ⊢ ( 𝜑 → ( ( I ↾ 𝐷 ) ∘ ( 𝑃 ∘ 𝑄 ) ) = ( 𝑃 ∘ 𝑄 ) )
153 150 152 eqtr2d ⊢ ( 𝜑 → ( 𝑃 ∘ 𝑄 ) = ( ( 𝑄 ∘ 𝑄 ) ∘ ( 𝑃 ∘ 𝑄 ) ) )
154 coass ⊢ ( ( 𝑄 ∘ 𝑄 ) ∘ ( 𝑃 ∘ 𝑄 ) ) = ( 𝑄 ∘ ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) )
155 153 154 eqtrdi ⊢ ( 𝜑 → ( 𝑃 ∘ 𝑄 ) = ( 𝑄 ∘ ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ) )
156 155 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) → ( 𝑃 ∘ 𝑄 ) = ( 𝑄 ∘ ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ) )
157 f1ofn ⊢ ( 𝑄 : 𝐷 –1-1-onto→ 𝐷 → 𝑄 Fn 𝐷 )
158 33 157 syl ⊢ ( 𝜑 → 𝑄 Fn 𝐷 )
159 fnelnfp ⊢ ( ( 𝑄 Fn 𝐷 ∧ 𝐴 ∈ 𝐷 ) → ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ↔ ( 𝑄 ‘ 𝐴 ) ≠ 𝐴 ) )
160 158 79 159 syl2anc ⊢ ( 𝜑 → ( 𝐴 ∈ dom ( 𝑄 ∖ I ) ↔ ( 𝑄 ‘ 𝐴 ) ≠ 𝐴 ) )
161 160 necon2bbid ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐴 ) = 𝐴 ↔ ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) )
162 161 biimpar ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) → ( 𝑄 ‘ 𝐴 ) = 𝐴 )
163 fnfvima ⊢ ( ( 𝑄 Fn 𝐷 ∧ dom ( 𝑃 ∖ I ) ⊆ 𝐷 ∧ 𝐴 ∈ dom ( 𝑃 ∖ I ) ) → ( 𝑄 ‘ 𝐴 ) ∈ ( 𝑄 “ dom ( 𝑃 ∖ I ) ) )
164 158 78 5 163 syl3anc ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐴 ) ∈ ( 𝑄 “ dom ( 𝑃 ∖ I ) ) )
165 164 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) → ( 𝑄 ‘ 𝐴 ) ∈ ( 𝑄 “ dom ( 𝑃 ∖ I ) ) )
166 162 165 eqeltrrd ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) → 𝐴 ∈ ( 𝑄 “ dom ( 𝑃 ∖ I ) ) )
167 145 difeq1d ⊢ ( 𝜑 → ( ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ∖ I ) = ( ( ( 𝑄 ∘ 𝑃 ) ∘ ◡ 𝑄 ) ∖ I ) )
168 167 dmeqd ⊢ ( 𝜑 → dom ( ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ∖ I ) = dom ( ( ( 𝑄 ∘ 𝑃 ) ∘ ◡ 𝑄 ) ∖ I ) )
169 f1omvdconj ⊢ ( ( 𝑃 : 𝐷 ⟶ 𝐷 ∧ 𝑄 : 𝐷 –1-1-onto→ 𝐷 ) → dom ( ( ( 𝑄 ∘ 𝑃 ) ∘ ◡ 𝑄 ) ∖ I ) = ( 𝑄 “ dom ( 𝑃 ∖ I ) ) )
170 31 33 169 syl2anc ⊢ ( 𝜑 → dom ( ( ( 𝑄 ∘ 𝑃 ) ∘ ◡ 𝑄 ) ∖ I ) = ( 𝑄 “ dom ( 𝑃 ∖ I ) ) )
171 168 170 eqtrd ⊢ ( 𝜑 → dom ( ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ∖ I ) = ( 𝑄 “ dom ( 𝑃 ∖ I ) ) )
172 171 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) → dom ( ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ∖ I ) = ( 𝑄 “ dom ( 𝑃 ∖ I ) ) )
173 166 172 eleqtrrd ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) → 𝐴 ∈ dom ( ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ∖ I ) )
174 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) → ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) )
175 coeq1 ⊢ ( 𝑟 = 𝑄 → ( 𝑟 ∘ 𝑠 ) = ( 𝑄 ∘ 𝑠 ) )
176 175 eqeq2d ⊢ ( 𝑟 = 𝑄 → ( ( 𝑃 ∘ 𝑄 ) = ( 𝑟 ∘ 𝑠 ) ↔ ( 𝑃 ∘ 𝑄 ) = ( 𝑄 ∘ 𝑠 ) ) )
177 difeq1 ⊢ ( 𝑟 = 𝑄 → ( 𝑟 ∖ I ) = ( 𝑄 ∖ I ) )
178 177 dmeqd ⊢ ( 𝑟 = 𝑄 → dom ( 𝑟 ∖ I ) = dom ( 𝑄 ∖ I ) )
179 178 eleq2d ⊢ ( 𝑟 = 𝑄 → ( 𝐴 ∈ dom ( 𝑟 ∖ I ) ↔ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) )
180 179 notbid ⊢ ( 𝑟 = 𝑄 → ( ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ↔ ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) )
181 176 180 3anbi13d ⊢ ( 𝑟 = 𝑄 → ( ( ( 𝑃 ∘ 𝑄 ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ↔ ( ( 𝑃 ∘ 𝑄 ) = ( 𝑄 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) ) )
182 coeq2 ⊢ ( 𝑠 = ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) → ( 𝑄 ∘ 𝑠 ) = ( 𝑄 ∘ ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ) )
183 182 eqeq2d ⊢ ( 𝑠 = ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) → ( ( 𝑃 ∘ 𝑄 ) = ( 𝑄 ∘ 𝑠 ) ↔ ( 𝑃 ∘ 𝑄 ) = ( 𝑄 ∘ ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ) ) )
184 difeq1 ⊢ ( 𝑠 = ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) → ( 𝑠 ∖ I ) = ( ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ∖ I ) )
185 184 dmeqd ⊢ ( 𝑠 = ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) → dom ( 𝑠 ∖ I ) = dom ( ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ∖ I ) )
186 185 eleq2d ⊢ ( 𝑠 = ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) → ( 𝐴 ∈ dom ( 𝑠 ∖ I ) ↔ 𝐴 ∈ dom ( ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ∖ I ) ) )
187 183 186 3anbi12d ⊢ ( 𝑠 = ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) → ( ( ( 𝑃 ∘ 𝑄 ) = ( 𝑄 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) ↔ ( ( 𝑃 ∘ 𝑄 ) = ( 𝑄 ∘ ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ) ∧ 𝐴 ∈ dom ( ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) ) )
188 181 187 rspc2ev ⊢ ( ( 𝑄 ∈ 𝑇 ∧ ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ∈ 𝑇 ∧ ( ( 𝑃 ∘ 𝑄 ) = ( 𝑄 ∘ ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ) ∧ 𝐴 ∈ dom ( ( 𝑄 ∘ ( 𝑃 ∘ 𝑄 ) ) ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) ) → ∃ 𝑟 ∈ 𝑇 ∃ 𝑠 ∈ 𝑇 ( ( 𝑃 ∘ 𝑄 ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) )
189 139 149 156 173 174 188 syl113anc ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) → ∃ 𝑟 ∈ 𝑇 ∃ 𝑠 ∈ 𝑇 ( ( 𝑃 ∘ 𝑄 ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) )
190 189 olcd ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ dom ( 𝑄 ∖ I ) ) → ( ( 𝑃 ∘ 𝑄 ) = ( I ↾ 𝐷 ) ∨ ∃ 𝑟 ∈ 𝑇 ∃ 𝑠 ∈ 𝑇 ( ( 𝑃 ∘ 𝑄 ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) )
191 138 190 pm2.61dan ⊢ ( 𝜑 → ( ( 𝑃 ∘ 𝑄 ) = ( I ↾ 𝐷 ) ∨ ∃ 𝑟 ∈ 𝑇 ∃ 𝑠 ∈ 𝑇 ( ( 𝑃 ∘ 𝑄 ) = ( 𝑟 ∘ 𝑠 ) ∧ 𝐴 ∈ dom ( 𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom ( 𝑟 ∖ I ) ) ) )