Theorem pmtrcnel2

Description: Variation on pmtrcnel . (Contributed by Thierry Arnoux, 16-Nov-2023)

	Ref	Expression
Hypotheses	pmtrcnel.s	$$⊢S=\mathrm{SymGrp}\left(D\right)$$
	pmtrcnel.t	$$⊢T=\mathrm{pmTrsp}\left(D\right)$$
	pmtrcnel.b	$$⊢B={\mathrm{Base}}_S$$
	pmtrcnel.j	$$⊢J=F\left(I\right)$$
	pmtrcnel.d	$$⊢\phi \to D\in V$$
	pmtrcnel.f	$$⊢\phi \to F\in B$$
	pmtrcnel.i	$$⊢\phi \to I\in \mathrm{dom}\left(F\setminus \mathrm{I}\right)$$
Assertion	pmtrcnel2	$$⊢\phi \to \mathrm{dom}\left(F\setminus \mathrm{I}\right)\setminus \left\{I,J\right\}\subseteq \mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)$$

Proof

Step	Hyp	Ref	Expression
1		pmtrcnel.s	$$⊢S=\mathrm{SymGrp}\left(D\right)$$
2		pmtrcnel.t	$$⊢T=\mathrm{pmTrsp}\left(D\right)$$
3		pmtrcnel.b	$$⊢B={\mathrm{Base}}_S$$
4		pmtrcnel.j	$$⊢J=F\left(I\right)$$
5		pmtrcnel.d	$$⊢\phi \to D\in V$$
6		pmtrcnel.f	$$⊢\phi \to F\in B$$
7		pmtrcnel.i	$$⊢\phi \to I\in \mathrm{dom}\left(F\setminus \mathrm{I}\right)$$
8		mvdco	$$⊢\mathrm{dom}\left(\left({T\left(\left\{I,J\right\}\right)}^{-1}\circ \left(T\left(\left\{I,J\right\}\right)\circ F\right)\right)\setminus \mathrm{I}\right)\subseteq \mathrm{dom}\left({T\left(\left\{I,J\right\}\right)}^{-1}\setminus \mathrm{I}\right)\cup \mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)$$
9	8	a1i	$$⊢\phi \to \mathrm{dom}\left(\left({T\left(\left\{I,J\right\}\right)}^{-1}\circ \left(T\left(\left\{I,J\right\}\right)\circ F\right)\right)\setminus \mathrm{I}\right)\subseteq \mathrm{dom}\left({T\left(\left\{I,J\right\}\right)}^{-1}\setminus \mathrm{I}\right)\cup \mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)$$
10		coass	$$⊢\left({T\left(\left\{I,J\right\}\right)}^{-1}\circ T\left(\left\{I,J\right\}\right)\right)\circ F={T\left(\left\{I,J\right\}\right)}^{-1}\circ \left(T\left(\left\{I,J\right\}\right)\circ F\right)$$
11		difss	$$⊢F\setminus \mathrm{I}\subseteq F$$
12		dmss	$$⊢F\setminus \mathrm{I}\subseteq F\to \mathrm{dom}\left(F\setminus \mathrm{I}\right)\subseteq \mathrm{dom}F$$
13	11 12	ax-mp	$$⊢\mathrm{dom}\left(F\setminus \mathrm{I}\right)\subseteq \mathrm{dom}F$$
14	13 7	sselid	$$⊢\phi \to I\in \mathrm{dom}F$$
15	1 3	symgbasf1o	$$⊢F\in B\to F:D\underset{1-1\; onto}{⟶}D$$
16		f1of	$$⊢F:D\underset{1-1\; onto}{⟶}D\to F:D⟶D$$
17	6 15 16	3syl	$$⊢\phi \to F:D⟶D$$
18	17	fdmd	$$⊢\phi \to \mathrm{dom}F=D$$
19	14 18	eleqtrd	$$⊢\phi \to I\in D$$
20	17 19	ffvelrnd	$$⊢\phi \to F\left(I\right)\in D$$
21	4 20	eqeltrid	$$⊢\phi \to J\in D$$
22	19 21	prssd	$$⊢\phi \to \left\{I,J\right\}\subseteq D$$
23	17	ffnd	$$⊢\phi \to FFnD$$
24		fnelnfp	$$⊢\left(FFnD\wedge I\in D\right)\to \left(I\in \mathrm{dom}\left(F\setminus \mathrm{I}\right)\leftrightarrow F\left(I\right)\ne I\right)$$
25	24	biimpa	$$⊢\left(\left(FFnD\wedge I\in D\right)\wedge I\in \mathrm{dom}\left(F\setminus \mathrm{I}\right)\right)\to F\left(I\right)\ne I$$
26	23 19 7 25	syl21anc	$$⊢\phi \to F\left(I\right)\ne I$$
27	26	necomd	$$⊢\phi \to I\ne F\left(I\right)$$
28	4	a1i	$$⊢\phi \to J=F\left(I\right)$$
29	27 28	neeqtrrd	$$⊢\phi \to I\ne J$$
30		pr2nelem	$$⊢\left(I\in D\wedge J\in D\wedge I\ne J\right)\to \left\{I,J\right\}\approx 2_{𝑜}$$
31	19 21 29 30	syl3anc	$$⊢\phi \to \left\{I,J\right\}\approx 2_{𝑜}$$
32		eqid	$$⊢\mathrm{ran}T=\mathrm{ran}T$$
33	2 32	pmtrrn	$$⊢\left(D\in V\wedge \left\{I,J\right\}\subseteq D\wedge \left\{I,J\right\}\approx 2_{𝑜}\right)\to T\left(\left\{I,J\right\}\right)\in \mathrm{ran}T$$
34	5 22 31 33	syl3anc	$$⊢\phi \to T\left(\left\{I,J\right\}\right)\in \mathrm{ran}T$$
35	2 32	pmtrff1o	$$⊢T\left(\left\{I,J\right\}\right)\in \mathrm{ran}T\to T\left(\left\{I,J\right\}\right):D\underset{1-1\; onto}{⟶}D$$
36		f1ococnv1	$$⊢T\left(\left\{I,J\right\}\right):D\underset{1-1\; onto}{⟶}D\to {T\left(\left\{I,J\right\}\right)}^{-1}\circ T\left(\left\{I,J\right\}\right)={\mathrm{I}\upharpoonright }_D$$
37	34 35 36	3syl	$$⊢\phi \to {T\left(\left\{I,J\right\}\right)}^{-1}\circ T\left(\left\{I,J\right\}\right)={\mathrm{I}\upharpoonright }_D$$
38	37	coeq1d	$$⊢\phi \to \left({T\left(\left\{I,J\right\}\right)}^{-1}\circ T\left(\left\{I,J\right\}\right)\right)\circ F=\left({\mathrm{I}\upharpoonright }_D\right)\circ F$$
39	10 38	eqtr3id	$$⊢\phi \to {T\left(\left\{I,J\right\}\right)}^{-1}\circ \left(T\left(\left\{I,J\right\}\right)\circ F\right)=\left({\mathrm{I}\upharpoonright }_D\right)\circ F$$
40		fcoi2	$$⊢F:D⟶D\to \left({\mathrm{I}\upharpoonright }_D\right)\circ F=F$$
41	17 40	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_D\right)\circ F=F$$
42	39 41	eqtrd	$$⊢\phi \to {T\left(\left\{I,J\right\}\right)}^{-1}\circ \left(T\left(\left\{I,J\right\}\right)\circ F\right)=F$$
43	42	difeq1d	$$⊢\phi \to \left({T\left(\left\{I,J\right\}\right)}^{-1}\circ \left(T\left(\left\{I,J\right\}\right)\circ F\right)\right)\setminus \mathrm{I}=F\setminus \mathrm{I}$$
44	43	dmeqd	$$⊢\phi \to \mathrm{dom}\left(\left({T\left(\left\{I,J\right\}\right)}^{-1}\circ \left(T\left(\left\{I,J\right\}\right)\circ F\right)\right)\setminus \mathrm{I}\right)=\mathrm{dom}\left(F\setminus \mathrm{I}\right)$$
45	2 32	pmtrfcnv	$$⊢T\left(\left\{I,J\right\}\right)\in \mathrm{ran}T\to {T\left(\left\{I,J\right\}\right)}^{-1}=T\left(\left\{I,J\right\}\right)$$
46	34 45	syl	$$⊢\phi \to {T\left(\left\{I,J\right\}\right)}^{-1}=T\left(\left\{I,J\right\}\right)$$
47	46	difeq1d	$$⊢\phi \to {T\left(\left\{I,J\right\}\right)}^{-1}\setminus \mathrm{I}=T\left(\left\{I,J\right\}\right)\setminus \mathrm{I}$$
48	47	dmeqd	$$⊢\phi \to \mathrm{dom}\left({T\left(\left\{I,J\right\}\right)}^{-1}\setminus \mathrm{I}\right)=\mathrm{dom}\left(T\left(\left\{I,J\right\}\right)\setminus \mathrm{I}\right)$$
49	2	pmtrmvd	$$⊢\left(D\in V\wedge \left\{I,J\right\}\subseteq D\wedge \left\{I,J\right\}\approx 2_{𝑜}\right)\to \mathrm{dom}\left(T\left(\left\{I,J\right\}\right)\setminus \mathrm{I}\right)=\left\{I,J\right\}$$
50	5 22 31 49	syl3anc	$$⊢\phi \to \mathrm{dom}\left(T\left(\left\{I,J\right\}\right)\setminus \mathrm{I}\right)=\left\{I,J\right\}$$
51	48 50	eqtrd	$$⊢\phi \to \mathrm{dom}\left({T\left(\left\{I,J\right\}\right)}^{-1}\setminus \mathrm{I}\right)=\left\{I,J\right\}$$
52	51	uneq1d	$$⊢\phi \to \mathrm{dom}\left({T\left(\left\{I,J\right\}\right)}^{-1}\setminus \mathrm{I}\right)\cup \mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)=\left\{I,J\right\}\cup \mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)$$
53		uncom	$$⊢\left\{I,J\right\}\cup \mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)=\mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)\cup \left\{I,J\right\}$$
54	52 53	eqtrdi	$$⊢\phi \to \mathrm{dom}\left({T\left(\left\{I,J\right\}\right)}^{-1}\setminus \mathrm{I}\right)\cup \mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)=\mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)\cup \left\{I,J\right\}$$
55	9 44 54	3sstr3d	$$⊢\phi \to \mathrm{dom}\left(F\setminus \mathrm{I}\right)\subseteq \mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)\cup \left\{I,J\right\}$$
56	55	ssdifd	$$⊢\phi \to \mathrm{dom}\left(F\setminus \mathrm{I}\right)\setminus \left\{I,J\right\}\subseteq \left(\mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)\cup \left\{I,J\right\}\right)\setminus \left\{I,J\right\}$$
57		difun2	$$⊢\left(\mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)\cup \left\{I,J\right\}\right)\setminus \left\{I,J\right\}=\mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)\setminus \left\{I,J\right\}$$
58		difss	$$⊢\mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)\setminus \left\{I,J\right\}\subseteq \mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)$$
59	57 58	eqsstri	$$⊢\left(\mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)\cup \left\{I,J\right\}\right)\setminus \left\{I,J\right\}\subseteq \mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)$$
60	56 59	sstrdi	$$⊢\phi \to \mathrm{dom}\left(F\setminus \mathrm{I}\right)\setminus \left\{I,J\right\}\subseteq \mathrm{dom}\left(\left(T\left(\left\{I,J\right\}\right)\circ F\right)\setminus \mathrm{I}\right)$$