MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  djurf1o Structured version   Visualization version   GIF version

Theorem djurf1o 9856
Description: The right injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.)
Assertion
Ref Expression
djurf1o inr:Vā€“1-1-ontoā†’({1o} Ɨ V)

Proof of Theorem djurf1o
Dummy variables š‘„ š‘¦ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-inr 9846 . . 3 inr = (š‘„ āˆˆ V ā†¦ āŸØ1o, š‘„āŸ©)
2 1onn 8591 . . . . . 6 1o āˆˆ Ļ‰
3 snidg 4625 . . . . . 6 (1o āˆˆ Ļ‰ ā†’ 1o āˆˆ {1o})
42, 3ax-mp 5 . . . . 5 1o āˆˆ {1o}
5 opelxpi 5675 . . . . 5 ((1o āˆˆ {1o} āˆ§ š‘„ āˆˆ V) ā†’ āŸØ1o, š‘„āŸ© āˆˆ ({1o} Ɨ V))
64, 5mpan 689 . . . 4 (š‘„ āˆˆ V ā†’ āŸØ1o, š‘„āŸ© āˆˆ ({1o} Ɨ V))
76adantl 483 . . 3 ((āŠ¤ āˆ§ š‘„ āˆˆ V) ā†’ āŸØ1o, š‘„āŸ© āˆˆ ({1o} Ɨ V))
8 fvexd 6862 . . 3 ((āŠ¤ āˆ§ š‘¦ āˆˆ ({1o} Ɨ V)) ā†’ (2nd ā€˜š‘¦) āˆˆ V)
9 1st2nd2 7965 . . . . . . . 8 (š‘¦ āˆˆ ({1o} Ɨ V) ā†’ š‘¦ = āŸØ(1st ā€˜š‘¦), (2nd ā€˜š‘¦)āŸ©)
10 xp1st 7958 . . . . . . . . . 10 (š‘¦ āˆˆ ({1o} Ɨ V) ā†’ (1st ā€˜š‘¦) āˆˆ {1o})
11 elsni 4608 . . . . . . . . . 10 ((1st ā€˜š‘¦) āˆˆ {1o} ā†’ (1st ā€˜š‘¦) = 1o)
1210, 11syl 17 . . . . . . . . 9 (š‘¦ āˆˆ ({1o} Ɨ V) ā†’ (1st ā€˜š‘¦) = 1o)
1312opeq1d 4841 . . . . . . . 8 (š‘¦ āˆˆ ({1o} Ɨ V) ā†’ āŸØ(1st ā€˜š‘¦), (2nd ā€˜š‘¦)āŸ© = āŸØ1o, (2nd ā€˜š‘¦)āŸ©)
149, 13eqtrd 2777 . . . . . . 7 (š‘¦ āˆˆ ({1o} Ɨ V) ā†’ š‘¦ = āŸØ1o, (2nd ā€˜š‘¦)āŸ©)
1514eqeq2d 2748 . . . . . 6 (š‘¦ āˆˆ ({1o} Ɨ V) ā†’ (āŸØ1o, š‘„āŸ© = š‘¦ ā†” āŸØ1o, š‘„āŸ© = āŸØ1o, (2nd ā€˜š‘¦)āŸ©))
16 eqcom 2744 . . . . . 6 (āŸØ1o, š‘„āŸ© = š‘¦ ā†” š‘¦ = āŸØ1o, š‘„āŸ©)
17 eqid 2737 . . . . . . 7 1o = 1o
18 1oex 8427 . . . . . . . 8 1o āˆˆ V
19 vex 3452 . . . . . . . 8 š‘„ āˆˆ V
2018, 19opth 5438 . . . . . . 7 (āŸØ1o, š‘„āŸ© = āŸØ1o, (2nd ā€˜š‘¦)āŸ© ā†” (1o = 1o āˆ§ š‘„ = (2nd ā€˜š‘¦)))
2117, 20mpbiran 708 . . . . . 6 (āŸØ1o, š‘„āŸ© = āŸØ1o, (2nd ā€˜š‘¦)āŸ© ā†” š‘„ = (2nd ā€˜š‘¦))
2215, 16, 213bitr3g 313 . . . . 5 (š‘¦ āˆˆ ({1o} Ɨ V) ā†’ (š‘¦ = āŸØ1o, š‘„āŸ© ā†” š‘„ = (2nd ā€˜š‘¦)))
2322bicomd 222 . . . 4 (š‘¦ āˆˆ ({1o} Ɨ V) ā†’ (š‘„ = (2nd ā€˜š‘¦) ā†” š‘¦ = āŸØ1o, š‘„āŸ©))
2423ad2antll 728 . . 3 ((āŠ¤ āˆ§ (š‘„ āˆˆ V āˆ§ š‘¦ āˆˆ ({1o} Ɨ V))) ā†’ (š‘„ = (2nd ā€˜š‘¦) ā†” š‘¦ = āŸØ1o, š‘„āŸ©))
251, 7, 8, 24f1o2d 7612 . 2 (āŠ¤ ā†’ inr:Vā€“1-1-ontoā†’({1o} Ɨ V))
2625mptru 1549 1 inr:Vā€“1-1-ontoā†’({1o} Ɨ V)
Colors of variables: wff setvar class
Syntax hints:   ā†” wb 205   āˆ§ wa 397   = wceq 1542  āŠ¤wtru 1543   āˆˆ wcel 2107  Vcvv 3448  {csn 4591  āŸØcop 4597   Ɨ cxp 5636  ā€“1-1-ontoā†’wf1o 6500  ā€˜cfv 6501  Ļ‰com 7807  1st c1st 7924  2nd c2nd 7925  1oc1o 8410  inrcinr 9843
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-om 7808  df-1st 7926  df-2nd 7927  df-1o 8417  df-inr 9846
This theorem is referenced by:  inrresf  9859  inrresf1  9860  djuin  9861  djuun  9869
  Copyright terms: Public domain W3C validator