Metamath Proof Explorer

Theorem pmtrcnel2

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

Ref Expression
Hypotheses pmtrcnel.s 
|- S = ( SymGrp ` D )
pmtrcnel.t 
|- T = ( pmTrsp ` D )
pmtrcnel.b 
|- B = ( Base ` S )
pmtrcnel.j 
|- J = ( F ` I )
pmtrcnel.d 
|- ( ph -> D e. V )
pmtrcnel.f 
|- ( ph -> F e. B )
pmtrcnel.i 
|- ( ph -> I e. dom ( F \ _I ) )
Assertion pmtrcnel2 
|- ( ph -> ( dom ( F \ _I ) \ { I , J } ) C_ dom ( ( ( T ` { I , J } ) o. F ) \ _I ) )

Proof

Step Hyp Ref Expression
1 pmtrcnel.s 
 |-  S = ( SymGrp ` D )
2 pmtrcnel.t 
 |-  T = ( pmTrsp ` D )
3 pmtrcnel.b 
 |-  B = ( Base ` S )
4 pmtrcnel.j 
 |-  J = ( F ` I )
5 pmtrcnel.d 
 |-  ( ph -> D e. V )
6 pmtrcnel.f 
 |-  ( ph -> F e. B )
7 pmtrcnel.i 
 |-  ( ph -> I e. dom ( F \ _I ) )
8 mvdco 
 |-  dom ( ( `' ( T ` { I , J } ) o. ( ( T ` { I , J } ) o. F ) ) \ _I ) C_ ( dom ( `' ( T ` { I , J } ) \ _I ) u. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) )
9 8 a1i 
 |-  ( ph -> dom ( ( `' ( T ` { I , J } ) o. ( ( T ` { I , J } ) o. F ) ) \ _I ) C_ ( dom ( `' ( T ` { I , J } ) \ _I ) u. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) ) )
10 coass 
 |-  ( ( `' ( T ` { I , J } ) o. ( T ` { I , J } ) ) o. F ) = ( `' ( T ` { I , J } ) o. ( ( T ` { I , J } ) o. F ) )
11 difss 
 |-  ( F \ _I ) C_ F
12 dmss 
 |-  ( ( F \ _I ) C_ F -> dom ( F \ _I ) C_ dom F )
13 11 12 ax-mp 
 |-  dom ( F \ _I ) C_ dom F
14 13 7 sselid 
 |-  ( ph -> I e. dom F )
15 1 3 symgbasf1o 
 |-  ( F e. B -> F : D -1-1-onto-> D )
16 f1of 
 |-  ( F : D -1-1-onto-> D -> F : D --> D )
17 6 15 16 3syl 
 |-  ( ph -> F : D --> D )
18 17 fdmd 
 |-  ( ph -> dom F = D )
19 14 18 eleqtrd 
 |-  ( ph -> I e. D )
20 17 19 ffvelcdmd 
 |-  ( ph -> ( F ` I ) e. D )
21 4 20 eqeltrid 
 |-  ( ph -> J e. D )
22 19 21 prssd 
 |-  ( ph -> { I , J } C_ D )
23 17 ffnd 
 |-  ( ph -> F Fn D )
24 fnelnfp 
 |-  ( ( F Fn D /\ I e. D ) -> ( I e. dom ( F \ _I ) <-> ( F ` I ) =/= I ) )
25 24 biimpa 
 |-  ( ( ( F Fn D /\ I e. D ) /\ I e. dom ( F \ _I ) ) -> ( F ` I ) =/= I )
26 23 19 7 25 syl21anc 
 |-  ( ph -> ( F ` I ) =/= I )
27 26 necomd 
 |-  ( ph -> I =/= ( F ` I ) )
28 4 a1i 
 |-  ( ph -> J = ( F ` I ) )
29 27 28 neeqtrrd 
 |-  ( ph -> I =/= J )
30 enpr2 
 |-  ( ( I e. D /\ J e. D /\ I =/= J ) -> { I , J } ~~ 2o )
31 19 21 29 30 syl3anc 
 |-  ( ph -> { I , J } ~~ 2o )
32 eqid 
 |-  ran T = ran T
33 2 32 pmtrrn 
 |-  ( ( D e. V /\ { I , J } C_ D /\ { I , J } ~~ 2o ) -> ( T ` { I , J } ) e. ran T )
34 5 22 31 33 syl3anc 
 |-  ( ph -> ( T ` { I , J } ) e. ran T )
35 2 32 pmtrff1o 
 |-  ( ( T ` { I , J } ) e. ran T -> ( T ` { I , J } ) : D -1-1-onto-> D )
36 f1ococnv1 
 |-  ( ( T ` { I , J } ) : D -1-1-onto-> D -> ( `' ( T ` { I , J } ) o. ( T ` { I , J } ) ) = ( _I |` D ) )
37 34 35 36 3syl 
 |-  ( ph -> ( `' ( T ` { I , J } ) o. ( T ` { I , J } ) ) = ( _I |` D ) )
38 37 coeq1d 
 |-  ( ph -> ( ( `' ( T ` { I , J } ) o. ( T ` { I , J } ) ) o. F ) = ( ( _I |` D ) o. F ) )
39 10 38 eqtr3id 
 |-  ( ph -> ( `' ( T ` { I , J } ) o. ( ( T ` { I , J } ) o. F ) ) = ( ( _I |` D ) o. F ) )
40 fcoi2 
 |-  ( F : D --> D -> ( ( _I |` D ) o. F ) = F )
41 17 40 syl 
 |-  ( ph -> ( ( _I |` D ) o. F ) = F )
42 39 41 eqtrd 
 |-  ( ph -> ( `' ( T ` { I , J } ) o. ( ( T ` { I , J } ) o. F ) ) = F )
43 42 difeq1d 
 |-  ( ph -> ( ( `' ( T ` { I , J } ) o. ( ( T ` { I , J } ) o. F ) ) \ _I ) = ( F \ _I ) )
44 43 dmeqd 
 |-  ( ph -> dom ( ( `' ( T ` { I , J } ) o. ( ( T ` { I , J } ) o. F ) ) \ _I ) = dom ( F \ _I ) )
45 2 32 pmtrfcnv 
 |-  ( ( T ` { I , J } ) e. ran T -> `' ( T ` { I , J } ) = ( T ` { I , J } ) )
46 34 45 syl 
 |-  ( ph -> `' ( T ` { I , J } ) = ( T ` { I , J } ) )
47 46 difeq1d 
 |-  ( ph -> ( `' ( T ` { I , J } ) \ _I ) = ( ( T ` { I , J } ) \ _I ) )
48 47 dmeqd 
 |-  ( ph -> dom ( `' ( T ` { I , J } ) \ _I ) = dom ( ( T ` { I , J } ) \ _I ) )
49 2 pmtrmvd 
 |-  ( ( D e. V /\ { I , J } C_ D /\ { I , J } ~~ 2o ) -> dom ( ( T ` { I , J } ) \ _I ) = { I , J } )
50 5 22 31 49 syl3anc 
 |-  ( ph -> dom ( ( T ` { I , J } ) \ _I ) = { I , J } )
51 48 50 eqtrd 
 |-  ( ph -> dom ( `' ( T ` { I , J } ) \ _I ) = { I , J } )
52 51 uneq1d 
 |-  ( ph -> ( dom ( `' ( T ` { I , J } ) \ _I ) u. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) ) = ( { I , J } u. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) ) )
53 uncom 
 |-  ( { I , J } u. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) ) = ( dom ( ( ( T ` { I , J } ) o. F ) \ _I ) u. { I , J } )
54 52 53 eqtrdi 
 |-  ( ph -> ( dom ( `' ( T ` { I , J } ) \ _I ) u. dom ( ( ( T ` { I , J } ) o. F ) \ _I ) ) = ( dom ( ( ( T ` { I , J } ) o. F ) \ _I ) u. { I , J } ) )
55 9 44 54 3sstr3d 
 |-  ( ph -> dom ( F \ _I ) C_ ( dom ( ( ( T ` { I , J } ) o. F ) \ _I ) u. { I , J } ) )
56 55 ssdifd 
 |-  ( ph -> ( dom ( F \ _I ) \ { I , J } ) C_ ( ( dom ( ( ( T ` { I , J } ) o. F ) \ _I ) u. { I , J } ) \ { I , J } ) )
57 difun2 
 |-  ( ( dom ( ( ( T ` { I , J } ) o. F ) \ _I ) u. { I , J } ) \ { I , J } ) = ( dom ( ( ( T ` { I , J } ) o. F ) \ _I ) \ { I , J } )
58 difss 
 |-  ( dom ( ( ( T ` { I , J } ) o. F ) \ _I ) \ { I , J } ) C_ dom ( ( ( T ` { I , J } ) o. F ) \ _I )
59 57 58 eqsstri 
 |-  ( ( dom ( ( ( T ` { I , J } ) o. F ) \ _I ) u. { I , J } ) \ { I , J } ) C_ dom ( ( ( T ` { I , J } ) o. F ) \ _I )
60 56 59 sstrdi 
 |-  ( ph -> ( dom ( F \ _I ) \ { I , J } ) C_ dom ( ( ( T ` { I , J } ) o. F ) \ _I ) )