Theorem pmtrdifellem4

Description: Lemma 4 for pmtrdifel . (Contributed by AV, 28-Jan-2019)

	Ref	Expression
Hypotheses	pmtrdifel.t	$$⊢T=\mathrm{ran}\mathrm{pmTrsp}\left(N\setminus \left\{K\right\}\right)$$
	pmtrdifel.r	$$⊢R=\mathrm{ran}\mathrm{pmTrsp}\left(N\right)$$
	pmtrdifel.0	$$⊢S=\mathrm{pmTrsp}\left(N\right)\left(\mathrm{dom}\left(Q\setminus \mathrm{I}\right)\right)$$
Assertion	pmtrdifellem4	$$⊢\left(Q\in T\wedge K\in N\right)\to S\left(K\right)=K$$

Proof

Step	Hyp	Ref	Expression
1		pmtrdifel.t	$$⊢T=\mathrm{ran}\mathrm{pmTrsp}\left(N\setminus \left\{K\right\}\right)$$
2		pmtrdifel.r	$$⊢R=\mathrm{ran}\mathrm{pmTrsp}\left(N\right)$$
3		pmtrdifel.0	$$⊢S=\mathrm{pmTrsp}\left(N\right)\left(\mathrm{dom}\left(Q\setminus \mathrm{I}\right)\right)$$
4	1 2 3	pmtrdifellem1	$$⊢Q\in T\to S\in R$$
5		eqid	$$⊢\mathrm{pmTrsp}\left(N\right)=\mathrm{pmTrsp}\left(N\right)$$
6		eqid	$$⊢\mathrm{dom}\left(S\setminus \mathrm{I}\right)=\mathrm{dom}\left(S\setminus \mathrm{I}\right)$$
7	5 2 6	pmtrffv	$$⊢\left(S\in R\wedge K\in N\right)\to S\left(K\right)=if\left(K\in \mathrm{dom}\left(S\setminus \mathrm{I}\right),\bigcup \left(\mathrm{dom}\left(S\setminus \mathrm{I}\right)\setminus \left\{K\right\}\right),K\right)$$
8	4 7	sylan	$$⊢\left(Q\in T\wedge K\in N\right)\to S\left(K\right)=if\left(K\in \mathrm{dom}\left(S\setminus \mathrm{I}\right),\bigcup \left(\mathrm{dom}\left(S\setminus \mathrm{I}\right)\setminus \left\{K\right\}\right),K\right)$$
9		eqid	$$⊢\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)=\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)$$
10		eqid	$$⊢{\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}$$
11	1 9 10	symgtrf	$$⊢T\subseteq {\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}$$
12	11	sseli	$$⊢Q\in T\to Q\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}$$
13	9 10	symgbasf	$$⊢Q\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(N\setminus \left\{K\right\}\right)}\to Q:N\setminus \left\{K\right\}⟶N\setminus \left\{K\right\}$$
14		ffn	$$⊢Q:N\setminus \left\{K\right\}⟶N\setminus \left\{K\right\}\to QFn\left(N\setminus \left\{K\right\}\right)$$
15		fndifnfp	$$⊢QFn\left(N\setminus \left\{K\right\}\right)\to \mathrm{dom}\left(Q\setminus \mathrm{I}\right)=\left\{x\in \left(N\setminus \left\{K\right\}\right)|Q\left(x\right)\ne x\right\}$$
16		ssrab2	$$⊢\left\{x\in \left(N\setminus \left\{K\right\}\right)|Q\left(x\right)\ne x\right\}\subseteq N\setminus \left\{K\right\}$$
17		ssel2	$$⊢\left(\left\{x\in \left(N\setminus \left\{K\right\}\right)|Q\left(x\right)\ne x\right\}\subseteq N\setminus \left\{K\right\}\wedge K\in \left\{x\in \left(N\setminus \left\{K\right\}\right)|Q\left(x\right)\ne x\right\}\right)\to K\in \left(N\setminus \left\{K\right\}\right)$$
18		eldif	$$⊢K\in \left(N\setminus \left\{K\right\}\right)\leftrightarrow \left(K\in N\wedge \neg K\in \left\{K\right\}\right)$$
19		elsng	$$⊢K\in N\to \left(K\in \left\{K\right\}\leftrightarrow K=K\right)$$
20	19	notbid	$$⊢K\in N\to \left(\neg K\in \left\{K\right\}\leftrightarrow \neg K=K\right)$$
21		eqid	$$⊢K=K$$
22	21	pm2.24i	$$⊢\neg K=K\to \neg K\in N$$
23	20 22	syl6bi	$$⊢K\in N\to \left(\neg K\in \left\{K\right\}\to \neg K\in N\right)$$
24	23	imp	$$⊢\left(K\in N\wedge \neg K\in \left\{K\right\}\right)\to \neg K\in N$$
25	18 24	sylbi	$$⊢K\in \left(N\setminus \left\{K\right\}\right)\to \neg K\in N$$
26	17 25	syl	$$⊢\left(\left\{x\in \left(N\setminus \left\{K\right\}\right)|Q\left(x\right)\ne x\right\}\subseteq N\setminus \left\{K\right\}\wedge K\in \left\{x\in \left(N\setminus \left\{K\right\}\right)|Q\left(x\right)\ne x\right\}\right)\to \neg K\in N$$
27	16 26	mpan	$$⊢K\in \left\{x\in \left(N\setminus \left\{K\right\}\right)|Q\left(x\right)\ne x\right\}\to \neg K\in N$$
28	27	con2i	$$⊢K\in N\to \neg K\in \left\{x\in \left(N\setminus \left\{K\right\}\right)|Q\left(x\right)\ne x\right\}$$
29		eleq2	$$⊢\mathrm{dom}\left(Q\setminus \mathrm{I}\right)=\left\{x\in \left(N\setminus \left\{K\right\}\right)|Q\left(x\right)\ne x\right\}\to \left(K\in \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\leftrightarrow K\in \left\{x\in \left(N\setminus \left\{K\right\}\right)|Q\left(x\right)\ne x\right\}\right)$$
30	29	notbid	$$⊢\mathrm{dom}\left(Q\setminus \mathrm{I}\right)=\left\{x\in \left(N\setminus \left\{K\right\}\right)|Q\left(x\right)\ne x\right\}\to \left(\neg K\in \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\leftrightarrow \neg K\in \left\{x\in \left(N\setminus \left\{K\right\}\right)|Q\left(x\right)\ne x\right\}\right)$$
31	28 30	syl5ibr	$$⊢\mathrm{dom}\left(Q\setminus \mathrm{I}\right)=\left\{x\in \left(N\setminus \left\{K\right\}\right)|Q\left(x\right)\ne x\right\}\to \left(K\in N\to \neg K\in \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\right)$$
32	14 15 31	3syl	$$⊢Q:N\setminus \left\{K\right\}⟶N\setminus \left\{K\right\}\to \left(K\in N\to \neg K\in \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\right)$$
33	12 13 32	3syl	$$⊢Q\in T\to \left(K\in N\to \neg K\in \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\right)$$
34	33	imp	$$⊢\left(Q\in T\wedge K\in N\right)\to \neg K\in \mathrm{dom}\left(Q\setminus \mathrm{I}\right)$$
35	1 2 3	pmtrdifellem2	$$⊢Q\in T\to \mathrm{dom}\left(S\setminus \mathrm{I}\right)=\mathrm{dom}\left(Q\setminus \mathrm{I}\right)$$
36	35	eleq2d	$$⊢Q\in T\to \left(K\in \mathrm{dom}\left(S\setminus \mathrm{I}\right)\leftrightarrow K\in \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\right)$$
37	36	adantr	$$⊢\left(Q\in T\wedge K\in N\right)\to \left(K\in \mathrm{dom}\left(S\setminus \mathrm{I}\right)\leftrightarrow K\in \mathrm{dom}\left(Q\setminus \mathrm{I}\right)\right)$$
38	34 37	mtbird	$$⊢\left(Q\in T\wedge K\in N\right)\to \neg K\in \mathrm{dom}\left(S\setminus \mathrm{I}\right)$$
39	38	iffalsed	$$⊢\left(Q\in T\wedge K\in N\right)\to if\left(K\in \mathrm{dom}\left(S\setminus \mathrm{I}\right),\bigcup \left(\mathrm{dom}\left(S\setminus \mathrm{I}\right)\setminus \left\{K\right\}\right),K\right)=K$$
40	8 39	eqtrd	$$⊢\left(Q\in T\wedge K\in N\right)\to S\left(K\right)=K$$