Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  psgnfzto1stlem Structured version   Visualization version   Unicode version

Theorem psgnfzto1stlem 28687
 Description: Lemma for psgnfzto1st 28692. Our permutation of rank can be written as a permutation of rank composed with a transposition. (Contributed by Thierry Arnoux, 21-Aug-2020.)
Hypothesis
Ref Expression
psgnfzto1st.d
Assertion
Ref Expression
psgnfzto1stlem pmTrsp
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Proof of Theorem psgnfzto1stlem
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ovex 6336 . . . . 5
2 ovex 6336 . . . . . 6
3 vex 3034 . . . . . 6
42, 3ifex 3940 . . . . 5
51, 4ifex 3940 . . . 4
6 eqid 2471 . . . 4
75, 6fnmpti 5716 . . 3
87a1i 11 . 2
9 psgnfzto1st.d . . . . 5
10 eqid 2471 . . . . 5 pmTrsp pmTrsp
119, 10pmtrto1cl 28686 . . . 4 pmTrsp pmTrsp
12 eqid 2471 . . . . 5 pmTrsp pmTrsp
1310, 12pmtrff1o 17182 . . . 4 pmTrsp pmTrsp pmTrsp
14 f1ofn 5829 . . . 4 pmTrsp pmTrsp
1511, 13, 143syl 18 . . 3 pmTrsp
16 simpr 468 . . . . . . . 8
1716iftrued 3880 . . . . . . 7
18 simpl 464 . . . . . . . . . 10
1918nnred 10646 . . . . . . . . . . 11
20 fz1ssnn 11856 . . . . . . . . . . . . 13
219eleq2i 2541 . . . . . . . . . . . . . . 15
2221biimpi 199 . . . . . . . . . . . . . 14
2322adantl 473 . . . . . . . . . . . . 13
2420, 23sseldi 3416 . . . . . . . . . . . 12
2524nnred 10646 . . . . . . . . . . 11
26 elfz1b 11890 . . . . . . . . . . . . . . 15
2726simp2bi 1046 . . . . . . . . . . . . . 14
2822, 27syl 17 . . . . . . . . . . . . 13
2928adantl 473 . . . . . . . . . . . 12
3029nnred 10646 . . . . . . . . . . 11
3119lep1d 10560 . . . . . . . . . . 11
32 elfzle2 11829 . . . . . . . . . . . 12
3323, 32syl 17 . . . . . . . . . . 11
3419, 25, 30, 31, 33letrd 9809 . . . . . . . . . 10
3529nnzd 11062 . . . . . . . . . . 11
36 fznn 11889 . . . . . . . . . . 11
3735, 36syl 17 . . . . . . . . . 10
3818, 34, 37mpbir2and 936 . . . . . . . . 9
3938, 9syl6eleqr 2560 . . . . . . . 8
4039ad2antrr 740 . . . . . . 7
4117, 40eqeltrd 2549 . . . . . 6
42 simpr 468 . . . . . . . 8
4342iffalsed 3883 . . . . . . 7
44 simpr 468 . . . . . . . . . 10
4544iftrued 3880 . . . . . . . . 9
4642adantr 472 . . . . . . . . . . . . 13
479, 20eqsstri 3448 . . . . . . . . . . . . . . . 16
48 simpllr 777 . . . . . . . . . . . . . . . 16
4947, 48sseldi 3416 . . . . . . . . . . . . . . 15
50 nn1m1nn 10651 . . . . . . . . . . . . . . 15
5149, 50syl 17 . . . . . . . . . . . . . 14
5251ord 384 . . . . . . . . . . . . 13
5346, 52mpd 15 . . . . . . . . . . . 12
5453nnred 10646 . . . . . . . . . . . . 13
5549nnred 10646 . . . . . . . . . . . . 13
5630ad3antrrr 744 . . . . . . . . . . . . 13
5755lem1d 10562 . . . . . . . . . . . . 13
5848, 9syl6eleq 2559 . . . . . . . . . . . . . 14
59 elfzle2 11829 . . . . . . . . . . . . . 14
6058, 59syl 17 . . . . . . . . . . . . 13
6154, 55, 56, 57, 60letrd 9809 . . . . . . . . . . . 12
6253, 61jca 541 . . . . . . . . . . 11
63 fznn 11889 . . . . . . . . . . . . 13
6435, 63syl 17 . . . . . . . . . . . 12
6564ad3antrrr 744 . . . . . . . . . . 11
6662, 65mpbird 240 . . . . . . . . . 10
6766, 9syl6eleqr 2560 . . . . . . . . 9
6845, 67eqeltrd 2549 . . . . . . . 8
69 simpr 468 . . . . . . . . . 10
7069iffalsed 3883 . . . . . . . . 9
71 simpllr 777 . . . . . . . . 9
7270, 71eqeltrd 2549 . . . . . . . 8
7368, 72pm2.61dan 808 . . . . . . 7
7443, 73eqeltrd 2549 . . . . . 6
7541, 74pm2.61dan 808 . . . . 5
7675ralrimiva 2809 . . . 4
77 eqid 2471 . . . . 5
7877fnmpt 5714 . . . 4
7976, 78syl 17 . . 3
8077rnmptss 6068 . . . 4
8176, 80syl 17 . . 3
82 fnco 5694 . . 3 pmTrsp pmTrsp
8315, 79, 81, 82syl3anc 1292 . 2 pmTrsp
84 simpr 468 . . . . . . . 8
8584iftrued 3880 . . . . . . 7
8685fveq2d 5883 . . . . . 6 pmTrsp pmTrsp
87 fzfi 12223 . . . . . . . . . 10
889, 87eqeltri 2545 . . . . . . . . 9
8988a1i 11 . . . . . . . 8
9023, 21sylibr 217 . . . . . . . 8
9119ltp1d 10559 . . . . . . . . 9
9219, 91ltned 9788 . . . . . . . 8
9310pmtrprfv 17172 . . . . . . . 8 pmTrsp
9489, 39, 90, 92, 93syl13anc 1294 . . . . . . 7 pmTrsp
9594ad2antrr 740 . . . . . 6 pmTrsp
9686, 95eqtr2d 2506 . . . . 5 pmTrsp
9788a1i 11 . . . . . . . . . 10
9839ad4antr 746 . . . . . . . . . 10
9990ad4antr 746 . . . . . . . . . 10
10092ad4antr 746 . . . . . . . . . 10
10110pmtrprfv2 28685 . . . . . . . . . 10 pmTrsp
10297, 98, 99, 100, 101syl13anc 1294 . . . . . . . . 9 pmTrsp
10391ad4antr 746 . . . . . . . . . . . . . 14
104 simpr 468 . . . . . . . . . . . . . 14
105103, 104breqtrrd 4422 . . . . . . . . . . . . 13
10619ad4antr 746 . . . . . . . . . . . . . 14
107 simpr 468 . . . . . . . . . . . . . . . . 17
10847, 107sseldi 3416 . . . . . . . . . . . . . . . 16
109108nnred 10646 . . . . . . . . . . . . . . 15
110109ad3antrrr 744 . . . . . . . . . . . . . 14
111106, 110ltnled 9799 . . . . . . . . . . . . 13
112105, 111mpbid 215 . . . . . . . . . . . 12
113112iffalsed 3883 . . . . . . . . . . 11
114113, 104eqtrd 2505 . . . . . . . . . 10
115114fveq2d 5883 . . . . . . . . 9 pmTrsp pmTrsp
116104oveq1d 6323 . . . . . . . . . 10
117106recnd 9687 . . . . . . . . . . 11
118 1cnd 9677 . . . . . . . . . . 11
119117, 118pncand 10006 . . . . . . . . . 10
120116, 119eqtrd 2505 . . . . . . . . 9
121102, 115, 1203eqtr4rd 2516 . . . . . . . 8 pmTrsp
122 simplr 770 . . . . . . . . . . . . 13
123 simpr 468 . . . . . . . . . . . . . 14
124123necomd 2698 . . . . . . . . . . . . 13
125109ad3antrrr 744 . . . . . . . . . . . . . 14
12625ad4antr 746 . . . . . . . . . . . . . 14
127125, 126ltlend 9797 . . . . . . . . . . . . 13
128122, 124, 127mpbir2and 936 . . . . . . . . . . . 12
129108ad3antrrr 744 . . . . . . . . . . . . 13
130 simpll 768 . . . . . . . . . . . . . 14
131130ad3antrrr 744 . . . . . . . . . . . . 13
132 nnleltp1 11015 . . . . . . . . . . . . 13
133129, 131, 132syl2anc 673 . . . . . . . . . . . 12
134128, 133mpbird 240 . . . . . . . . . . 11
135134iftrued 3880 . . . . . . . . . 10
136135fveq2d 5883 . . . . . . . . 9 pmTrsp pmTrsp
13788a1i 11 . . . . . . . . . 10
13839ad4antr 746 . . . . . . . . . . 11
139 simp-5r 787 . . . . . . . . . . 11
140 simpr 468 . . . . . . . . . . . . . . . . 17
141140ad2antrr 740 . . . . . . . . . . . . . . . 16
142 elnn1uz2 11258 . . . . . . . . . . . . . . . . . 18
143129, 142sylib 201 . . . . . . . . . . . . . . . . 17
144143ord 384 . . . . . . . . . . . . . . . 16
145141, 144mpd 15 . . . . . . . . . . . . . . 15
146 uz2m1nn 11256 . . . . . . . . . . . . . . 15
147145, 146syl 17 . . . . . . . . . . . . . 14
148139, 28syl 17 . . . . . . . . . . . . . 14
149147nnred 10646 . . . . . . . . . . . . . . 15
150131, 139, 30syl2anc 673 . . . . . . . . . . . . . . 15
151125lem1d 10562 . . . . . . . . . . . . . . 15
152107ad3antrrr 744 . . . . . . . . . . . . . . . . 17
153152, 9syl6eleq 2559 . . . . . . . . . . . . . . . 16
154 elfzle2 11829 . . . . . . . . . . . . . . . 16
155153, 154syl 17 . . . . . . . . . . . . . . 15
156149, 125, 150, 151, 155letrd 9809 . . . . . . . . . . . . . 14
157147, 148, 1563jca 1210 . . . . . . . . . . . . 13
158 elfz1b 11890 . . . . . . . . . . . . 13
159157, 158sylibr 217 . . . . . . . . . . . 12
160159, 9syl6eleqr 2560 . . . . . . . . . . 11
161138, 139, 1603jca 1210 . . . . . . . . . 10
162131, 139, 92syl2anc 673 . . . . . . . . . . 11
163 simpr 468 . . . . . . . . . . . . . . . 16
164163oveq1d 6323 . . . . . . . . . . . . . . 15
165109recnd 9687 . . . . . . . . . . . . . . . . 17
166165ad3antrrr 744 . . . . . . . . . . . . . . . 16
167 1cnd 9677 . . . . . . . . . . . . . . . 16
168166, 167npcand 10009 . . . . . . . . . . . . . . 15
169164, 168eqtr2d 2506 . . . . . . . . . . . . . 14
170169ex 441 . . . . . . . . . . . . 13
171170necon3d 2664 . . . . . . . . . . . 12
172171imp 436 . . . . . . . . . . 11
173149, 125, 126, 151, 128lelttrd 9810 . . . . . . . . . . . . 13
174149, 173ltned 9788 . . . . . . . . . . . 12
175174necomd 2698 . . . . . . . . . . 11
176162, 172, 1753jca 1210 . . . . . . . . . 10
17710pmtrprfv3 17173 . . . . . . . . . 10 pmTrsp
178137, 161, 176, 177syl3anc 1292 . . . . . . . . 9 pmTrsp
179136, 178eqtr2d 2506 . . . . . . . 8 pmTrsp
180121, 179pm2.61dane 2730 . . . . . . 7 pmTrsp
181109ad2antrr 740 . . . . . . . . . . . . . 14
18219ad3antrrr 744 . . . . . . . . . . . . . 14
18325ad3antrrr 744 . . . . . . . . . . . . . 14
184 simpr 468 . . . . . . . . . . . . . 14
18531ad3antrrr 744 . . . . . . . . . . . . . 14
186181, 182, 183, 184, 185letrd 9809 . . . . . . . . . . . . 13
187186ex 441 . . . . . . . . . . . 12
188187con3d 140 . . . . . . . . . . 11
189188imp 436 . . . . . . . . . 10
190189iffalsed 3883 . . . . . . . . 9
191190fveq2d 5883 . . . . . . . 8 pmTrsp pmTrsp
19288a1i 11 . . . . . . . . 9
19339ad3antrrr 744 . . . . . . . . . 10
19490ad3antrrr 744 . . . . . . . . . 10
195107ad2antrr 740 . . . . . . . . . 10
196193, 194, 1953jca 1210 . . . . . . . . 9
19792ad3antrrr 744 . . . . . . . . . 10
19819ad3antrrr 744 . . . . . . . . . . 11
19925ad3antrrr 744 . . . . . . . . . . . 12
200109ad2antrr 740 . . . . . . . . . . . 12
20191ad3antrrr 744 . . . . . . . . . . . 12
202 simpr 468 . . . . . . . . . . . . 13
203199, 200ltnled 9799 . . . . . . . . . . . . 13
204202, 203mpbird 240 . . . . . . . . . . . 12
205198, 199, 200, 201, 204lttrd 9813 . . . . . . . . . . 11
206198, 205ltned 9788 . . . . . . . . . 10
207199, 204ltned 9788 . . . . . . . . . 10
208197, 206, 2073jca 1210 . . . . . . . . 9
20910pmtrprfv3 17173 . . . . . . . . 9 pmTrsp
210192, 196, 208, 209syl3anc 1292 . . . . . . . 8 pmTrsp
211191, 210eqtr2d 2506 . . . . . . 7 pmTrsp
212180, 211ifeqda 3905 . . . . . 6 pmTrsp
213140iffalsed 3883 . . . . . . 7
214213fveq2d 5883 . . . . . 6 pmTrsp pmTrsp
215212, 214eqtr4d 2508 . . . . 5 pmTrsp
21696, 215ifeqda 3905 . . . 4 pmTrsp
217 eqidd 2472 . . . . . 6
218 eqeq1 2475 . . . . . . . 8
219 breq1 4398 . . . . . . . . 9
220 oveq1 6315 . . . . . . . . 9
221 id 22 . . . . . . . . 9
222219, 220, 221ifbieq12d 3899 . . . . . . . 8
223218, 222ifbieq2d 3897 . . . . . . 7
224223adantl 473 . . . . . 6
225 ovex 6336 . . . . . . . . 9
226 vex 3034 . . . . . . . . 9
227225, 226keepel 3939 . . . . . . . 8
228227a1i 11 . . . . . . 7
229 ifexg 3941 . . . . . . 7
230130, 228, 229syl2anc 673 . . . . . 6
231217, 224, 107, 230fvmptd 5969 . . . . 5
232231fveq2d 5883 . . . 4 pmTrsp pmTrsp
233216, 232eqtr4d 2508 . . 3 pmTrsp
234 breq1 4398 . . . . . . 7
235234, 220, 221ifbieq12d 3899 . . . . . 6
236218, 235ifbieq2d 3897 . . . . 5
237225, 226ifex 3940 . . . . . 6
2381, 237ifex 3940 . . . . 5
239236, 6, 238fvmpt 5963 . . . 4
240239adantl 473 . . 3
241 funmpt 5625 . . . . 5
242241a1i 11 . . . 4
24376adantr 472 . . . . . 6
244 dmmptg 5339 . . . . . 6
245243, 244syl 17 . . . . 5
246107, 245eleqtrrd 2552 . . . 4
247 fvco 5956 . . . 4 pmTrsp pmTrsp
248242, 246, 247syl2anc 673 . . 3 pmTrsp pmTrsp
249233, 240, 2483eqtr4d 2515 . 2 pmTrsp
2508, 83, 249eqfnfvd 5994 1 pmTrsp
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wo 375   wa 376   w3a 1007   wceq 1452   wcel 1904   wne 2641  wral 2756  cvv 3031   wss 3390  cif 3872  cpr 3961   class class class wbr 4395   cmpt 4454   cdm 4839   crn 4840   ccom 4843   wfun 5583   wfn 5584  wf1o 5588  cfv 5589  (class class class)co 6308  cfn 7587  cc 9555  cr 9556  c1 9558   caddc 9560   clt 9693   cle 9694   cmin 9880  cn 10631  c2 10681  cz 10961  cuz 11182  cfz 11810  pmTrspcpmtr 17160 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-er 7381  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-nn 10632  df-2 10690  df-n0 10894  df-z 10962  df-uz 11183  df-fz 11811  df-pmtr 17161 This theorem is referenced by:  fzto1st  28690  psgnfzto1st  28692
 Copyright terms: Public domain W3C validator