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

Theorem 2ndconst 8086
Description: The mapping of a restriction of the 2nd function to a converse constant function. (Contributed by NM, 27-Mar-2008.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
Assertion
Ref Expression
2ndconst (š“ āˆˆ š‘‰ ā†’ (2nd ā†¾ ({š“} Ɨ šµ)):({š“} Ɨ šµ)ā€“1-1-ontoā†’šµ)

Proof of Theorem 2ndconst
Dummy variables š‘„ š‘¦ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snnzg 4778 . . 3 (š“ āˆˆ š‘‰ ā†’ {š“} ā‰  āˆ…)
2 fo2ndres 8001 . . 3 ({š“} ā‰  āˆ… ā†’ (2nd ā†¾ ({š“} Ɨ šµ)):({š“} Ɨ šµ)ā€“ontoā†’šµ)
31, 2syl 17 . 2 (š“ āˆˆ š‘‰ ā†’ (2nd ā†¾ ({š“} Ɨ šµ)):({š“} Ɨ šµ)ā€“ontoā†’šµ)
4 moeq 3703 . . . . . 6 āˆƒ*š‘„ š‘„ = āŸØš“, š‘¦āŸ©
54moani 2547 . . . . 5 āˆƒ*š‘„(š‘¦ āˆˆ šµ āˆ§ š‘„ = āŸØš“, š‘¦āŸ©)
6 vex 3478 . . . . . . . 8 š‘¦ āˆˆ V
76brresi 5990 . . . . . . 7 (š‘„(2nd ā†¾ ({š“} Ɨ šµ))š‘¦ ā†” (š‘„ āˆˆ ({š“} Ɨ šµ) āˆ§ š‘„2nd š‘¦))
8 fo2nd 7995 . . . . . . . . . . 11 2nd :Vā€“ontoā†’V
9 fofn 6807 . . . . . . . . . . 11 (2nd :Vā€“ontoā†’V ā†’ 2nd Fn V)
108, 9ax-mp 5 . . . . . . . . . 10 2nd Fn V
11 vex 3478 . . . . . . . . . 10 š‘„ āˆˆ V
12 fnbrfvb 6944 . . . . . . . . . 10 ((2nd Fn V āˆ§ š‘„ āˆˆ V) ā†’ ((2nd ā€˜š‘„) = š‘¦ ā†” š‘„2nd š‘¦))
1310, 11, 12mp2an 690 . . . . . . . . 9 ((2nd ā€˜š‘„) = š‘¦ ā†” š‘„2nd š‘¦)
1413anbi2i 623 . . . . . . . 8 ((š‘„ āˆˆ ({š“} Ɨ šµ) āˆ§ (2nd ā€˜š‘„) = š‘¦) ā†” (š‘„ āˆˆ ({š“} Ɨ šµ) āˆ§ š‘„2nd š‘¦))
15 elxp7 8009 . . . . . . . . . . 11 (š‘„ āˆˆ ({š“} Ɨ šµ) ā†” (š‘„ āˆˆ (V Ɨ V) āˆ§ ((1st ā€˜š‘„) āˆˆ {š“} āˆ§ (2nd ā€˜š‘„) āˆˆ šµ)))
16 eleq1 2821 . . . . . . . . . . . . . . 15 ((2nd ā€˜š‘„) = š‘¦ ā†’ ((2nd ā€˜š‘„) āˆˆ šµ ā†” š‘¦ āˆˆ šµ))
1716biimpac 479 . . . . . . . . . . . . . 14 (((2nd ā€˜š‘„) āˆˆ šµ āˆ§ (2nd ā€˜š‘„) = š‘¦) ā†’ š‘¦ āˆˆ šµ)
1817adantll 712 . . . . . . . . . . . . 13 ((((1st ā€˜š‘„) āˆˆ {š“} āˆ§ (2nd ā€˜š‘„) āˆˆ šµ) āˆ§ (2nd ā€˜š‘„) = š‘¦) ā†’ š‘¦ āˆˆ šµ)
1918adantll 712 . . . . . . . . . . . 12 (((š‘„ āˆˆ (V Ɨ V) āˆ§ ((1st ā€˜š‘„) āˆˆ {š“} āˆ§ (2nd ā€˜š‘„) āˆˆ šµ)) āˆ§ (2nd ā€˜š‘„) = š‘¦) ā†’ š‘¦ āˆˆ šµ)
20 elsni 4645 . . . . . . . . . . . . . 14 ((1st ā€˜š‘„) āˆˆ {š“} ā†’ (1st ā€˜š‘„) = š“)
21 eqopi 8010 . . . . . . . . . . . . . . 15 ((š‘„ āˆˆ (V Ɨ V) āˆ§ ((1st ā€˜š‘„) = š“ āˆ§ (2nd ā€˜š‘„) = š‘¦)) ā†’ š‘„ = āŸØš“, š‘¦āŸ©)
2221anassrs 468 . . . . . . . . . . . . . 14 (((š‘„ āˆˆ (V Ɨ V) āˆ§ (1st ā€˜š‘„) = š“) āˆ§ (2nd ā€˜š‘„) = š‘¦) ā†’ š‘„ = āŸØš“, š‘¦āŸ©)
2320, 22sylanl2 679 . . . . . . . . . . . . 13 (((š‘„ āˆˆ (V Ɨ V) āˆ§ (1st ā€˜š‘„) āˆˆ {š“}) āˆ§ (2nd ā€˜š‘„) = š‘¦) ā†’ š‘„ = āŸØš“, š‘¦āŸ©)
2423adantlrr 719 . . . . . . . . . . . 12 (((š‘„ āˆˆ (V Ɨ V) āˆ§ ((1st ā€˜š‘„) āˆˆ {š“} āˆ§ (2nd ā€˜š‘„) āˆˆ šµ)) āˆ§ (2nd ā€˜š‘„) = š‘¦) ā†’ š‘„ = āŸØš“, š‘¦āŸ©)
2519, 24jca 512 . . . . . . . . . . 11 (((š‘„ āˆˆ (V Ɨ V) āˆ§ ((1st ā€˜š‘„) āˆˆ {š“} āˆ§ (2nd ā€˜š‘„) āˆˆ šµ)) āˆ§ (2nd ā€˜š‘„) = š‘¦) ā†’ (š‘¦ āˆˆ šµ āˆ§ š‘„ = āŸØš“, š‘¦āŸ©))
2615, 25sylanb 581 . . . . . . . . . 10 ((š‘„ āˆˆ ({š“} Ɨ šµ) āˆ§ (2nd ā€˜š‘„) = š‘¦) ā†’ (š‘¦ āˆˆ šµ āˆ§ š‘„ = āŸØš“, š‘¦āŸ©))
2726adantl 482 . . . . . . . . 9 ((š“ āˆˆ š‘‰ āˆ§ (š‘„ āˆˆ ({š“} Ɨ šµ) āˆ§ (2nd ā€˜š‘„) = š‘¦)) ā†’ (š‘¦ āˆˆ šµ āˆ§ š‘„ = āŸØš“, š‘¦āŸ©))
28 simprr 771 . . . . . . . . . . 11 ((š“ āˆˆ š‘‰ āˆ§ (š‘¦ āˆˆ šµ āˆ§ š‘„ = āŸØš“, š‘¦āŸ©)) ā†’ š‘„ = āŸØš“, š‘¦āŸ©)
29 snidg 4662 . . . . . . . . . . . . 13 (š“ āˆˆ š‘‰ ā†’ š“ āˆˆ {š“})
3029adantr 481 . . . . . . . . . . . 12 ((š“ āˆˆ š‘‰ āˆ§ (š‘¦ āˆˆ šµ āˆ§ š‘„ = āŸØš“, š‘¦āŸ©)) ā†’ š“ āˆˆ {š“})
31 simprl 769 . . . . . . . . . . . 12 ((š“ āˆˆ š‘‰ āˆ§ (š‘¦ āˆˆ šµ āˆ§ š‘„ = āŸØš“, š‘¦āŸ©)) ā†’ š‘¦ āˆˆ šµ)
3230, 31opelxpd 5715 . . . . . . . . . . 11 ((š“ āˆˆ š‘‰ āˆ§ (š‘¦ āˆˆ šµ āˆ§ š‘„ = āŸØš“, š‘¦āŸ©)) ā†’ āŸØš“, š‘¦āŸ© āˆˆ ({š“} Ɨ šµ))
3328, 32eqeltrd 2833 . . . . . . . . . 10 ((š“ āˆˆ š‘‰ āˆ§ (š‘¦ āˆˆ šµ āˆ§ š‘„ = āŸØš“, š‘¦āŸ©)) ā†’ š‘„ āˆˆ ({š“} Ɨ šµ))
34 fveq2 6891 . . . . . . . . . . . 12 (š‘„ = āŸØš“, š‘¦āŸ© ā†’ (2nd ā€˜š‘„) = (2nd ā€˜āŸØš“, š‘¦āŸ©))
35 op2ndg 7987 . . . . . . . . . . . . 13 ((š“ āˆˆ š‘‰ āˆ§ š‘¦ āˆˆ V) ā†’ (2nd ā€˜āŸØš“, š‘¦āŸ©) = š‘¦)
3635elvd 3481 . . . . . . . . . . . 12 (š“ āˆˆ š‘‰ ā†’ (2nd ā€˜āŸØš“, š‘¦āŸ©) = š‘¦)
3734, 36sylan9eqr 2794 . . . . . . . . . . 11 ((š“ āˆˆ š‘‰ āˆ§ š‘„ = āŸØš“, š‘¦āŸ©) ā†’ (2nd ā€˜š‘„) = š‘¦)
3837adantrl 714 . . . . . . . . . 10 ((š“ āˆˆ š‘‰ āˆ§ (š‘¦ āˆˆ šµ āˆ§ š‘„ = āŸØš“, š‘¦āŸ©)) ā†’ (2nd ā€˜š‘„) = š‘¦)
3933, 38jca 512 . . . . . . . . 9 ((š“ āˆˆ š‘‰ āˆ§ (š‘¦ āˆˆ šµ āˆ§ š‘„ = āŸØš“, š‘¦āŸ©)) ā†’ (š‘„ āˆˆ ({š“} Ɨ šµ) āˆ§ (2nd ā€˜š‘„) = š‘¦))
4027, 39impbida 799 . . . . . . . 8 (š“ āˆˆ š‘‰ ā†’ ((š‘„ āˆˆ ({š“} Ɨ šµ) āˆ§ (2nd ā€˜š‘„) = š‘¦) ā†” (š‘¦ āˆˆ šµ āˆ§ š‘„ = āŸØš“, š‘¦āŸ©)))
4114, 40bitr3id 284 . . . . . . 7 (š“ āˆˆ š‘‰ ā†’ ((š‘„ āˆˆ ({š“} Ɨ šµ) āˆ§ š‘„2nd š‘¦) ā†” (š‘¦ āˆˆ šµ āˆ§ š‘„ = āŸØš“, š‘¦āŸ©)))
427, 41bitrid 282 . . . . . 6 (š“ āˆˆ š‘‰ ā†’ (š‘„(2nd ā†¾ ({š“} Ɨ šµ))š‘¦ ā†” (š‘¦ āˆˆ šµ āˆ§ š‘„ = āŸØš“, š‘¦āŸ©)))
4342mobidv 2543 . . . . 5 (š“ āˆˆ š‘‰ ā†’ (āˆƒ*š‘„ š‘„(2nd ā†¾ ({š“} Ɨ šµ))š‘¦ ā†” āˆƒ*š‘„(š‘¦ āˆˆ šµ āˆ§ š‘„ = āŸØš“, š‘¦āŸ©)))
445, 43mpbiri 257 . . . 4 (š“ āˆˆ š‘‰ ā†’ āˆƒ*š‘„ š‘„(2nd ā†¾ ({š“} Ɨ šµ))š‘¦)
4544alrimiv 1930 . . 3 (š“ āˆˆ š‘‰ ā†’ āˆ€š‘¦āˆƒ*š‘„ š‘„(2nd ā†¾ ({š“} Ɨ šµ))š‘¦)
46 funcnv2 6616 . . 3 (Fun ā—”(2nd ā†¾ ({š“} Ɨ šµ)) ā†” āˆ€š‘¦āˆƒ*š‘„ š‘„(2nd ā†¾ ({š“} Ɨ šµ))š‘¦)
4745, 46sylibr 233 . 2 (š“ āˆˆ š‘‰ ā†’ Fun ā—”(2nd ā†¾ ({š“} Ɨ šµ)))
48 dff1o3 6839 . 2 ((2nd ā†¾ ({š“} Ɨ šµ)):({š“} Ɨ šµ)ā€“1-1-ontoā†’šµ ā†” ((2nd ā†¾ ({š“} Ɨ šµ)):({š“} Ɨ šµ)ā€“ontoā†’šµ āˆ§ Fun ā—”(2nd ā†¾ ({š“} Ɨ šµ))))
493, 47, 48sylanbrc 583 1 (š“ āˆˆ š‘‰ ā†’ (2nd ā†¾ ({š“} Ɨ šµ)):({š“} Ɨ šµ)ā€“1-1-ontoā†’šµ)
Colors of variables: wff setvar class
Syntax hints:   ā†’ wi 4   ā†” wb 205   āˆ§ wa 396  āˆ€wal 1539   = wceq 1541   āˆˆ wcel 2106  āˆƒ*wmo 2532   ā‰  wne 2940  Vcvv 3474  āˆ…c0 4322  {csn 4628  āŸØcop 4634   class class class wbr 5148   Ɨ cxp 5674  ā—”ccnv 5675   ā†¾ cres 5678  Fun wfun 6537   Fn wfn 6538  ā€“ontoā†’wfo 6541  ā€“1-1-ontoā†’wf1o 6542  ā€˜cfv 6543  1st c1st 7972  2nd c2nd 7973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7724
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-1st 7974  df-2nd 7975
This theorem is referenced by:  curry1  8089  xpfiOLD  9317  fsum2dlem  15715  fprod2dlem  15923  gsum2dlem2  19838  ovoliunlem1  25018  gsummpt2d  32196  fv2ndcnv  34744
  Copyright terms: Public domain W3C validator