# Metamath Proof Explorer

## 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 {Q}Fn\left({N}\setminus \left\{{K}\right\}\right)$
15 fndifnfp ${⊢}{Q}Fn\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)↔\left({K}\in {N}\wedge ¬{K}\in \left\{{K}\right\}\right)$
19 elsng ${⊢}{K}\in {N}\to \left({K}\in \left\{{K}\right\}↔{K}={K}\right)$
20 19 notbid ${⊢}{K}\in {N}\to \left(¬{K}\in \left\{{K}\right\}↔¬{K}={K}\right)$
21 eqid ${⊢}{K}={K}$
22 21 pm2.24i ${⊢}¬{K}={K}\to ¬{K}\in {N}$
23 20 22 syl6bi ${⊢}{K}\in {N}\to \left(¬{K}\in \left\{{K}\right\}\to ¬{K}\in {N}\right)$
24 23 imp ${⊢}\left({K}\in {N}\wedge ¬{K}\in \left\{{K}\right\}\right)\to ¬{K}\in {N}$
25 18 24 sylbi ${⊢}{K}\in \left({N}\setminus \left\{{K}\right\}\right)\to ¬{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 ¬{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 ¬{K}\in {N}$
28 27 con2i ${⊢}{K}\in {N}\to ¬{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)↔{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(¬{K}\in \mathrm{dom}\left({Q}\setminus \mathrm{I}\right)↔¬{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 ¬{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 ¬{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 ¬{K}\in \mathrm{dom}\left({Q}\setminus \mathrm{I}\right)\right)$
34 33 imp ${⊢}\left({Q}\in {T}\wedge {K}\in {N}\right)\to ¬{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)↔{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)↔{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 ¬{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}$