Theorem psgnunilem1 19413

Description: Lemma for psgnuni 19419. 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 2726	. . . . . . . . 9 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
3		psgnunilem1.t	. . . . . . . . 9 ⊢ 𝑇 = ran (pmTrsp‘𝐷)
4	2, 3	pmtrfinv 19381	. . . . . . . 8 ⊢ (𝑄 ∈ 𝑇 → (𝑄 ∘ 𝑄) = ( I ↾ 𝐷))
5	1, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∘ 𝑄) = ( I ↾ 𝐷))
6		coeq1 5851	. . . . . . . 8 ⊢ (𝑃 = 𝑄 → (𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑄))
7	6	eqeq1d 2728	. . . . . . 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 870	. . 3 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 = 𝑄) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
12		psgnunilem1.p	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ 𝑇)
13	2, 3	pmtrfcnv 19384	. . . . . . . . . 10 ⊢ (𝑃 ∈ 𝑇 → ◡𝑃 = 𝑃)
14	12, 13	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ◡𝑃 = 𝑃)
15	14	eqcomd 2732	. . . . . . . 8 ⊢ (𝜑 → 𝑃 = ◡𝑃)
16	15	coeq2d 5856	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ 𝑃) = ((𝑃 ∘ 𝑄) ∘ ◡𝑃))
17	2, 3	pmtrff1o 19383	. . . . . . . . 9 ⊢ (𝑃 ∈ 𝑇 → 𝑃:𝐷–1-1-onto→𝐷)
18	12, 17	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑃:𝐷–1-1-onto→𝐷)
19	2, 3	pmtrfconj 19386	. . . . . . . 8 ⊢ ((𝑄 ∈ 𝑇 ∧ 𝑃:𝐷–1-1-onto→𝐷) → ((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∈ 𝑇)
20	1, 18, 19	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∈ 𝑇)
21	16, 20	eqeltrd 2827	. . . . . 6 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ 𝑃) ∈ 𝑇)
22	21	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∘ 𝑄) ∘ 𝑃) ∈ 𝑇)
23	12	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → 𝑃 ∈ 𝑇)
24		coass 6258	. . . . . . 7 ⊢ (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃) = ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃))
25	2, 3	pmtrfinv 19381	. . . . . . . . . 10 ⊢ (𝑃 ∈ 𝑇 → (𝑃 ∘ 𝑃) = ( I ↾ 𝐷))
26	12, 25	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ∘ 𝑃) = ( I ↾ 𝐷))
27	26	coeq2d 5856	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃)) = ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷)))
28		f1of 6827	. . . . . . . . . . 11 ⊢ (𝑃:𝐷–1-1-onto→𝐷 → 𝑃:𝐷⟶𝐷)
29	18, 28	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃:𝐷⟶𝐷)
30	2, 3	pmtrff1o 19383	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ 𝑇 → 𝑄:𝐷–1-1-onto→𝐷)
31	1, 30	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑄:𝐷–1-1-onto→𝐷)
32		f1of 6827	. . . . . . . . . . 11 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → 𝑄:𝐷⟶𝐷)
33	31, 32	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:𝐷⟶𝐷)
34		fco 6735	. . . . . . . . . 10 ⊢ ((𝑃:𝐷⟶𝐷 ∧ 𝑄:𝐷⟶𝐷) → (𝑃 ∘ 𝑄):𝐷⟶𝐷)
35	29, 33, 34	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ∘ 𝑄):𝐷⟶𝐷)
36		fcoi1 6759	. . . . . . . . 9 ⊢ ((𝑃 ∘ 𝑄):𝐷⟶𝐷 → ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷)) = (𝑃 ∘ 𝑄))
37	35, 36	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷)) = (𝑃 ∘ 𝑄))
38	27, 37	eqtrd 2766	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃)) = (𝑃 ∘ 𝑄))
39	24, 38	eqtr2id 2779	. . . . . 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 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 19385	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ 𝑇 ↔ (𝐷 ∈ V ∧ 𝑃:𝐷–1-1-onto→𝐷 ∧ dom (𝑃 ∖ I ) ≈ 2o))
46	45	simp3bi 1144	. . . . . . . . . . . 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 8643	. . . . . . . . . . . . . . 15 ⊢ 2o ∈ ω
50		nnfi 9169	. . . . . . . . . . . . . . 15 ⊢ (2o ∈ ω → 2o ∈ Fin)
51	49, 50	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 2o ∈ Fin
52	2, 3	pmtrfb 19385	. . . . . . . . . . . . . . . . 17 ⊢ (𝑄 ∈ 𝑇 ↔ (𝐷 ∈ V ∧ 𝑄:𝐷–1-1-onto→𝐷 ∧ dom (𝑄 ∖ I ) ≈ 2o))
53	52	simp3bi 1144	. . . . . . . . . . . . . . . 16 ⊢ (𝑄 ∈ 𝑇 → dom (𝑄 ∖ I ) ≈ 2o)
54	1, 53	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom (𝑄 ∖ I ) ≈ 2o)
55		enfi 9192	. . . . . . . . . . . . . . 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 10005	. . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝐴 ∈ dom (𝑄 ∖ I ))
63		f1ofn 6828	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃:𝐷–1-1-onto→𝐷 → 𝑃 Fn 𝐷)
64	18, 63	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 Fn 𝐷)
65	64	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝑃 Fn 𝐷)
66		fimass 6732	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃:𝐷⟶𝐷 → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷)
67	29, 66	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷)
68	67	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷)
69		simprr 770	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))
70		fnfvima 7230	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 Fn 𝐷 ∧ (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷 ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))) → (𝑃‘𝐴) ∈ (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))))
71	65, 68, 69, 70	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃‘𝐴) ∈ (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))))
72		difss 4126	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∖ I ) ⊆ 𝑃
73		dmss 5896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃 ∖ I ) ⊆ 𝑃 → dom (𝑃 ∖ I ) ⊆ dom 𝑃)
74	72, 73	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom (𝑃 ∖ I ) ⊆ dom 𝑃
75		f1odm 6831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:𝐷–1-1-onto→𝐷 → dom 𝑃 = 𝐷)
76	18, 75	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → dom 𝑃 = 𝐷)
77	74, 76	sseqtrid 4029	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → dom (𝑃 ∖ I ) ⊆ 𝐷)
78	77, 41	sseldd 3978	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
79		eqid 2726	. . . . . . . . . . . . . . . . . . 19 ⊢ dom (𝑃 ∖ I ) = dom (𝑃 ∖ I )
80	2, 3, 79	pmtrffv 19379	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ 𝑇 ∧ 𝐴 ∈ 𝐷) → (𝑃‘𝐴) = if(𝐴 ∈ dom (𝑃 ∖ I ), ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}), 𝐴))
81	12, 78, 80	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑃‘𝐴) = if(𝐴 ∈ dom (𝑃 ∖ I ), ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}), 𝐴))
82	41	iftrued 4531	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝐴 ∈ dom (𝑃 ∖ I ), ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}), 𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}))
83	81, 82	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃‘𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}))
84	83	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃‘𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}))
85		imaco 6244	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∘ 𝑃) “ dom (𝑄 ∖ I )) = (𝑃 “ (𝑃 “ dom (𝑄 ∖ I )))
86	26	imaeq1d 6052	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑃 ∘ 𝑃) “ dom (𝑄 ∖ I )) = (( I ↾ 𝐷) “ dom (𝑄 ∖ I )))
87		difss 4126	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑄 ∖ I ) ⊆ 𝑄
88		dmss 5896	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑄 ∖ I ) ⊆ 𝑄 → dom (𝑄 ∖ I ) ⊆ dom 𝑄)
89	87, 88	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ dom (𝑄 ∖ I ) ⊆ dom 𝑄
90		f1odm 6831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → dom 𝑄 = 𝐷)
91	89, 90	sseqtrid 4029	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → dom (𝑄 ∖ I ) ⊆ 𝐷)
92	31, 91	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → dom (𝑄 ∖ I ) ⊆ 𝐷)
93		resiima 6069	. . . . . . . . . . . . . . . . . . 19 ⊢ (dom (𝑄 ∖ I ) ⊆ 𝐷 → (( I ↾ 𝐷) “ dom (𝑄 ∖ I )) = dom (𝑄 ∖ I ))
94	92, 93	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (( I ↾ 𝐷) “ dom (𝑄 ∖ I )) = dom (𝑄 ∖ I ))
95	86, 94	eqtrd 2766	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑃 ∘ 𝑃) “ dom (𝑄 ∖ I )) = dom (𝑄 ∖ I ))
96	85, 95	eqtr3id 2780	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))) = dom (𝑄 ∖ I ))
97	96	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))) = dom (𝑄 ∖ I ))
98	71, 84, 97	3eltr3d 2841	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}) ∈ dom (𝑄 ∖ I ))
99	62, 98	prssd 4820	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → {𝐴, ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})} ⊆ dom (𝑄 ∖ I ))
100	61, 99	eqsstrd 4015	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) ⊆ dom (𝑄 ∖ I ))
101	54	ensymd 9003	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2o ≈ dom (𝑄 ∖ I ))
102		entr 9004	. . . . . . . . . . . . . 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 9259	. . . . . . . . . . . 12 ⊢ ((dom (𝑄 ∖ I ) ∈ Fin ∧ dom (𝑃 ∖ I ) ⊆ dom (𝑄 ∖ I ) ∧ dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I )) → dom (𝑃 ∖ I ) = dom (𝑄 ∖ I ))
106	58, 100, 104, 105	syl3anc 1368	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) = dom (𝑄 ∖ I ))
107	106	eqcomd 2732	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑄 ∖ I ) = dom (𝑃 ∖ I ))
108		f1otrspeq 19367	. . . . . . . . . 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 456	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )) → 𝑃 = 𝑄))
111	110	necon3ad 2947	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑃 ≠ 𝑄 → ¬ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))))
112	111	imp 406	. . . . . 6 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ¬ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))
113	16	difeq1d 4116	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) = (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ))
114	113	dmeqd 5899	. . . . . . . . 9 ⊢ (𝜑 → dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) = dom (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ))
115		f1omvdconj 19366	. . . . . . . . . 10 ⊢ ((𝑄:𝐷⟶𝐷 ∧ 𝑃:𝐷–1-1-onto→𝐷) → dom (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ) = (𝑃 “ dom (𝑄 ∖ I )))
116	33, 18, 115	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → dom (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ) = (𝑃 “ dom (𝑄 ∖ I )))
117	114, 116	eqtrd 2766	. . . . . . . 8 ⊢ (𝜑 → dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) = (𝑃 “ dom (𝑄 ∖ I )))
118	117	eleq2d 2813	. . . . . . 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 5851	. . . . . . . 8 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝑟 ∘ 𝑠) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠))
122	121	eqeq2d 2737	. . . . . . 7 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠)))
123		difeq1 4110	. . . . . . . . . 10 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝑟 ∖ I ) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))
124	123	dmeqd 5899	. . . . . . . . 9 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → dom (𝑟 ∖ I ) = dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))
125	124	eleq2d 2813	. . . . . . . 8 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝐴 ∈ dom (𝑟 ∖ I ) ↔ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )))
126	125	notbid 318	. . . . . . 7 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (¬ 𝐴 ∈ dom (𝑟 ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )))
127	122, 126	3anbi13d 1434	. . . . . 6 ⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))))
128		coeq2 5852	. . . . . . . 8 ⊢ (𝑠 = 𝑃 → (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃))
129	128	eqeq2d 2737	. . . . . . 7 ⊢ (𝑠 = 𝑃 → ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃)))
130		difeq1 4110	. . . . . . . . 9 ⊢ (𝑠 = 𝑃 → (𝑠 ∖ I ) = (𝑃 ∖ I ))
131	130	dmeqd 5899	. . . . . . . 8 ⊢ (𝑠 = 𝑃 → dom (𝑠 ∖ I ) = dom (𝑃 ∖ I ))
132	131	eleq2d 2813	. . . . . . 7 ⊢ (𝑠 = 𝑃 → (𝐴 ∈ dom (𝑠 ∖ I ) ↔ 𝐴 ∈ dom (𝑃 ∖ I )))
133	129, 132	3anbi12d 1433	. . . . . 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 1379	. . . 4 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))
136	135	olcd 871	. . 3 ⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
137	11, 136	pm2.61dane 3023	. 2 ⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
138	1	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝑄 ∈ 𝑇)
139		coass 6258	. . . . . . 7 ⊢ ((𝑄 ∘ 𝑃) ∘ 𝑄) = (𝑄 ∘ (𝑃 ∘ 𝑄))
140	2, 3	pmtrfcnv 19384	. . . . . . . . . 10 ⊢ (𝑄 ∈ 𝑇 → ◡𝑄 = 𝑄)
141	1, 140	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ◡𝑄 = 𝑄)
142	141	eqcomd 2732	. . . . . . . 8 ⊢ (𝜑 → 𝑄 = ◡𝑄)
143	142	coeq2d 5856	. . . . . . 7 ⊢ (𝜑 → ((𝑄 ∘ 𝑃) ∘ 𝑄) = ((𝑄 ∘ 𝑃) ∘ ◡𝑄))
144	139, 143	eqtr3id 2780	. . . . . 6 ⊢ (𝜑 → (𝑄 ∘ (𝑃 ∘ 𝑄)) = ((𝑄 ∘ 𝑃) ∘ ◡𝑄))
145	2, 3	pmtrfconj 19386	. . . . . . 7 ⊢ ((𝑃 ∈ 𝑇 ∧ 𝑄:𝐷–1-1-onto→𝐷) → ((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∈ 𝑇)
146	12, 31, 145	syl2anc 583	. . . . . 6 ⊢ (𝜑 → ((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∈ 𝑇)
147	144, 146	eqeltrd 2827	. . . . 5 ⊢ (𝜑 → (𝑄 ∘ (𝑃 ∘ 𝑄)) ∈ 𝑇)
148	147	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑄 ∘ (𝑃 ∘ 𝑄)) ∈ 𝑇)
149	5	coeq1d 5855	. . . . . . 7 ⊢ (𝜑 → ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄)) = (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄)))
150		fcoi2 6760	. . . . . . . 8 ⊢ ((𝑃 ∘ 𝑄):𝐷⟶𝐷 → (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄)) = (𝑃 ∘ 𝑄))
151	35, 150	syl 17	. . . . . . 7 ⊢ (𝜑 → (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄)) = (𝑃 ∘ 𝑄))
152	149, 151	eqtr2d 2767	. . . . . 6 ⊢ (𝜑 → (𝑃 ∘ 𝑄) = ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄)))
153		coass 6258	. . . . . 6 ⊢ ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄)) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄)))
154	152, 153	eqtrdi 2782	. . . . 5 ⊢ (𝜑 → (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))))
155	154	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))))
156		f1ofn 6828	. . . . . . . . . 10 ⊢ (𝑄:𝐷–1-1-onto→𝐷 → 𝑄 Fn 𝐷)
157	31, 156	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 Fn 𝐷)
158		fnelnfp 7171	. . . . . . . . 9 ⊢ ((𝑄 Fn 𝐷 ∧ 𝐴 ∈ 𝐷) → (𝐴 ∈ dom (𝑄 ∖ I ) ↔ (𝑄‘𝐴) ≠ 𝐴))
159	157, 78, 158	syl2anc 583	. . . . . . . 8 ⊢ (𝜑 → (𝐴 ∈ dom (𝑄 ∖ I ) ↔ (𝑄‘𝐴) ≠ 𝐴))
160	159	necon2bbid 2978	. . . . . . 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 1368	. . . . . . 7 ⊢ (𝜑 → (𝑄‘𝐴) ∈ (𝑄 “ dom (𝑃 ∖ I )))
164	163	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑄‘𝐴) ∈ (𝑄 “ dom (𝑃 ∖ I )))
165	161, 164	eqeltrrd 2828	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝐴 ∈ (𝑄 “ dom (𝑃 ∖ I )))
166	144	difeq1d 4116	. . . . . . . 8 ⊢ (𝜑 → ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ))
167	166	dmeqd 5899	. . . . . . 7 ⊢ (𝜑 → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ))
168		f1omvdconj 19366	. . . . . . . 8 ⊢ ((𝑃:𝐷⟶𝐷 ∧ 𝑄:𝐷–1-1-onto→𝐷) → dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
169	29, 31, 168	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
170	167, 169	eqtrd 2766	. . . . . 6 ⊢ (𝜑 → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
171	170	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I )))
172	165, 171	eleqtrrd 2830	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ))
173		simpr 484	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → ¬ 𝐴 ∈ dom (𝑄 ∖ I ))
174		coeq1 5851	. . . . . . 7 ⊢ (𝑟 = 𝑄 → (𝑟 ∘ 𝑠) = (𝑄 ∘ 𝑠))
175	174	eqeq2d 2737	. . . . . 6 ⊢ (𝑟 = 𝑄 → ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠)))
176		difeq1 4110	. . . . . . . . 9 ⊢ (𝑟 = 𝑄 → (𝑟 ∖ I ) = (𝑄 ∖ I ))
177	176	dmeqd 5899	. . . . . . . 8 ⊢ (𝑟 = 𝑄 → dom (𝑟 ∖ I ) = dom (𝑄 ∖ I ))
178	177	eleq2d 2813	. . . . . . 7 ⊢ (𝑟 = 𝑄 → (𝐴 ∈ dom (𝑟 ∖ I ) ↔ 𝐴 ∈ dom (𝑄 ∖ I )))
179	178	notbid 318	. . . . . 6 ⊢ (𝑟 = 𝑄 → (¬ 𝐴 ∈ dom (𝑟 ∖ I ) ↔ ¬ 𝐴 ∈ dom (𝑄 ∖ I )))
180	175, 179	3anbi13d 1434	. . . . 5 ⊢ (𝑟 = 𝑄 → (((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I ))))
181		coeq2 5852	. . . . . . 7 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝑄 ∘ 𝑠) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))))
182	181	eqeq2d 2737	. . . . . 6 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → ((𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄)))))
183		difeq1 4110	. . . . . . . 8 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝑠 ∖ I ) = ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ))
184	183	dmeqd 5899	. . . . . . 7 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → dom (𝑠 ∖ I ) = dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ))
185	184	eleq2d 2813	. . . . . 6 ⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝐴 ∈ dom (𝑠 ∖ I ) ↔ 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I )))
186	182, 185	3anbi12d 1433	. . . . 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 1379	. . 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 395   ∨ wo 844   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   ≠ wne 2934  ∃wrex 3064  Vcvv 3468   ∖ cdif 3940   ⊆ wss 3943  ifcif 4523  {csn 4623  {cpr 4625  ∪ cuni 4902   class class class wbr 5141   I cid 5566  ^◡ccnv 5668  dom cdm 5669  ran crn 5670   ↾ cres 5671   “ cima 5672   ∘ ccom 5673   Fn wfn 6532  ⟶wf 6533  –1-1-onto→wf1o 6536  ‘cfv 6537  ωcom 7852  2_oc2o 8461   ≈ cen 8938  Fincfn 8941  pmTrspcpmtr 19361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-om 7853  df-1o 8467  df-2o 8468  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-pmtr 19362

This theorem is referenced by:  psgnunilem2  19415