Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nvof1o Unicode version

Theorem nvof1o 24091
Description: An involution is a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016.)
Assertion
Ref Expression
nvof1o

Proof of Theorem nvof1o
StepHypRef Expression
1 fnfun 5593 . . . . . 6
2 fdmrn 24090 . . . . . 6
31, 2sylib 190 . . . . 5
43adantr 453 . . . 4
5 fndm 5595 . . . . . 6
65adantr 453 . . . . 5
7 df-rn 4934 . . . . . . 7
8 dmeq 5118 . . . . . . 7
97, 8syl5eq 2491 . . . . . 6
109, 5sylan9eqr 2501 . . . . 5
116, 10feq23d 5639 . . . 4
124, 11mpbid 203 . . 3
131adantr 453 . . . 4
14 funeq 5524 . . . . 5
1514adantl 454 . . . 4
1613, 15mpbird 225 . . 3
17 df-f1 5510 . . 3
1812, 16, 17sylanbrc 647 . 2
19 simpl 445 . . 3
20 df-fo 5511 . . 3
2119, 10, 20sylanbrc 647 . 2
22 df-f1o 5512 . 2
2318, 21, 22sylanbrc 647 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  /\wa 360  =wceq 1654  `'ccnv 4922  domcdm 4923  rancrn 4924  Funwfun 5499  Fnwfn 5500  -->wf 5501  -1-1->wf1 5502  -onto->wfo 5503  -1-1-onto->wf1o 5504
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1955  ax-ext 2428
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2434  df-cleq 2440  df-clel 2443  df-nfc 2572  df-rab 2725  df-v 2971  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-nul 3621  df-if 3770  df-sn 3851  df-pr 3852  df-op 3854  df-br 4248  df-opab 4306  df-rel 4930  df-cnv 4931  df-co 4932  df-dm 4933  df-rn 4934  df-fun 5507  df-fn 5508  df-f 5509  df-f1 5510  df-fo 5511  df-f1o 5512
  Copyright terms: Public domain W3C validator