ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2ndconst GIF version

Theorem 2ndconst 6226
Description: The mapping of a restriction of the 2nd function to a converse constant function. (Contributed by NM, 27-Mar-2008.)
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 snmg 3712 . . 3 (š“ ∈ š‘‰ → āˆƒš‘„ š‘„ ∈ {š“})
2 fo2ndresm 6166 . . 3 (āˆƒš‘„ š‘„ ∈ {š“} → (2nd ↾ ({š“} Ɨ šµ)):({š“} Ɨ šµ)–ontoā†’šµ)
31, 2syl 14 . 2 (š“ ∈ š‘‰ → (2nd ↾ ({š“} Ɨ šµ)):({š“} Ɨ šµ)–ontoā†’šµ)
4 moeq 2914 . . . . . 6 ∃*š‘„ š‘„ = āŸØš“, š‘¦āŸ©
54moani 2096 . . . . 5 ∃*š‘„(š‘¦ ∈ šµ ∧ š‘„ = āŸØš“, š‘¦āŸ©)
6 vex 2742 . . . . . . . 8 š‘¦ ∈ V
76brres 4915 . . . . . . 7 (š‘„(2nd ↾ ({š“} Ɨ šµ))š‘¦ ↔ (š‘„2nd š‘¦ ∧ š‘„ ∈ ({š“} Ɨ šµ)))
8 fo2nd 6162 . . . . . . . . . . 11 2nd :V–onto→V
9 fofn 5442 . . . . . . . . . . 11 (2nd :V–onto→V → 2nd Fn V)
108, 9ax-mp 5 . . . . . . . . . 10 2nd Fn V
11 vex 2742 . . . . . . . . . 10 š‘„ ∈ V
12 fnbrfvb 5559 . . . . . . . . . 10 ((2nd Fn V ∧ š‘„ ∈ V) → ((2nd ā€˜š‘„) = š‘¦ ↔ š‘„2nd š‘¦))
1310, 11, 12mp2an 426 . . . . . . . . 9 ((2nd ā€˜š‘„) = š‘¦ ↔ š‘„2nd š‘¦)
1413anbi1i 458 . . . . . . . 8 (((2nd ā€˜š‘„) = š‘¦ ∧ š‘„ ∈ ({š“} Ɨ šµ)) ↔ (š‘„2nd š‘¦ ∧ š‘„ ∈ ({š“} Ɨ šµ)))
15 elxp7 6174 . . . . . . . . . . 11 (š‘„ ∈ ({š“} Ɨ šµ) ↔ (š‘„ ∈ (V Ɨ V) ∧ ((1st ā€˜š‘„) ∈ {š“} ∧ (2nd ā€˜š‘„) ∈ šµ)))
16 eleq1 2240 . . . . . . . . . . . . . . 15 ((2nd ā€˜š‘„) = š‘¦ → ((2nd ā€˜š‘„) ∈ šµ ↔ š‘¦ ∈ šµ))
1716biimpa 296 . . . . . . . . . . . . . 14 (((2nd ā€˜š‘„) = š‘¦ ∧ (2nd ā€˜š‘„) ∈ šµ) → š‘¦ ∈ šµ)
1817adantrl 478 . . . . . . . . . . . . 13 (((2nd ā€˜š‘„) = š‘¦ ∧ ((1st ā€˜š‘„) ∈ {š“} ∧ (2nd ā€˜š‘„) ∈ šµ)) → š‘¦ ∈ šµ)
1918adantrl 478 . . . . . . . . . . . 12 (((2nd ā€˜š‘„) = š‘¦ ∧ (š‘„ ∈ (V Ɨ V) ∧ ((1st ā€˜š‘„) ∈ {š“} ∧ (2nd ā€˜š‘„) ∈ šµ))) → š‘¦ ∈ šµ)
20 elsni 3612 . . . . . . . . . . . . . 14 ((1st ā€˜š‘„) ∈ {š“} → (1st ā€˜š‘„) = š“)
21 eqopi 6176 . . . . . . . . . . . . . . . 16 ((š‘„ ∈ (V Ɨ V) ∧ ((1st ā€˜š‘„) = š“ ∧ (2nd ā€˜š‘„) = š‘¦)) → š‘„ = āŸØš“, š‘¦āŸ©)
2221ancom2s 566 . . . . . . . . . . . . . . 15 ((š‘„ ∈ (V Ɨ V) ∧ ((2nd ā€˜š‘„) = š‘¦ ∧ (1st ā€˜š‘„) = š“)) → š‘„ = āŸØš“, š‘¦āŸ©)
2322an12s 565 . . . . . . . . . . . . . 14 (((2nd ā€˜š‘„) = š‘¦ ∧ (š‘„ ∈ (V Ɨ V) ∧ (1st ā€˜š‘„) = š“)) → š‘„ = āŸØš“, š‘¦āŸ©)
2420, 23sylanr2 405 . . . . . . . . . . . . 13 (((2nd ā€˜š‘„) = š‘¦ ∧ (š‘„ ∈ (V Ɨ V) ∧ (1st ā€˜š‘„) ∈ {š“})) → š‘„ = āŸØš“, š‘¦āŸ©)
2524adantrrr 487 . . . . . . . . . . . 12 (((2nd ā€˜š‘„) = š‘¦ ∧ (š‘„ ∈ (V Ɨ V) ∧ ((1st ā€˜š‘„) ∈ {š“} ∧ (2nd ā€˜š‘„) ∈ šµ))) → š‘„ = āŸØš“, š‘¦āŸ©)
2619, 25jca 306 . . . . . . . . . . 11 (((2nd ā€˜š‘„) = š‘¦ ∧ (š‘„ ∈ (V Ɨ V) ∧ ((1st ā€˜š‘„) ∈ {š“} ∧ (2nd ā€˜š‘„) ∈ šµ))) → (š‘¦ ∈ šµ ∧ š‘„ = āŸØš“, š‘¦āŸ©))
2715, 26sylan2b 287 . . . . . . . . . 10 (((2nd ā€˜š‘„) = š‘¦ ∧ š‘„ ∈ ({š“} Ɨ šµ)) → (š‘¦ ∈ šµ ∧ š‘„ = āŸØš“, š‘¦āŸ©))
2827adantl 277 . . . . . . . . 9 ((š“ ∈ š‘‰ ∧ ((2nd ā€˜š‘„) = š‘¦ ∧ š‘„ ∈ ({š“} Ɨ šµ))) → (š‘¦ ∈ šµ ∧ š‘„ = āŸØš“, š‘¦āŸ©))
29 fveq2 5517 . . . . . . . . . . . 12 (š‘„ = āŸØš“, š‘¦āŸ© → (2nd ā€˜š‘„) = (2nd ā€˜āŸØš“, š‘¦āŸ©))
30 op2ndg 6155 . . . . . . . . . . . . 13 ((š“ ∈ š‘‰ ∧ š‘¦ ∈ V) → (2nd ā€˜āŸØš“, š‘¦āŸ©) = š‘¦)
316, 30mpan2 425 . . . . . . . . . . . 12 (š“ ∈ š‘‰ → (2nd ā€˜āŸØš“, š‘¦āŸ©) = š‘¦)
3229, 31sylan9eqr 2232 . . . . . . . . . . 11 ((š“ ∈ š‘‰ ∧ š‘„ = āŸØš“, š‘¦āŸ©) → (2nd ā€˜š‘„) = š‘¦)
3332adantrl 478 . . . . . . . . . 10 ((š“ ∈ š‘‰ ∧ (š‘¦ ∈ šµ ∧ š‘„ = āŸØš“, š‘¦āŸ©)) → (2nd ā€˜š‘„) = š‘¦)
34 simprr 531 . . . . . . . . . . 11 ((š“ ∈ š‘‰ ∧ (š‘¦ ∈ šµ ∧ š‘„ = āŸØš“, š‘¦āŸ©)) → š‘„ = āŸØš“, š‘¦āŸ©)
35 snidg 3623 . . . . . . . . . . . . 13 (š“ ∈ š‘‰ → š“ ∈ {š“})
3635adantr 276 . . . . . . . . . . . 12 ((š“ ∈ š‘‰ ∧ (š‘¦ ∈ šµ ∧ š‘„ = āŸØš“, š‘¦āŸ©)) → š“ ∈ {š“})
37 simprl 529 . . . . . . . . . . . 12 ((š“ ∈ š‘‰ ∧ (š‘¦ ∈ šµ ∧ š‘„ = āŸØš“, š‘¦āŸ©)) → š‘¦ ∈ šµ)
38 opelxpi 4660 . . . . . . . . . . . 12 ((š“ ∈ {š“} ∧ š‘¦ ∈ šµ) → āŸØš“, š‘¦āŸ© ∈ ({š“} Ɨ šµ))
3936, 37, 38syl2anc 411 . . . . . . . . . . 11 ((š“ ∈ š‘‰ ∧ (š‘¦ ∈ šµ ∧ š‘„ = āŸØš“, š‘¦āŸ©)) → āŸØš“, š‘¦āŸ© ∈ ({š“} Ɨ šµ))
4034, 39eqeltrd 2254 . . . . . . . . . 10 ((š“ ∈ š‘‰ ∧ (š‘¦ ∈ šµ ∧ š‘„ = āŸØš“, š‘¦āŸ©)) → š‘„ ∈ ({š“} Ɨ šµ))
4133, 40jca 306 . . . . . . . . 9 ((š“ ∈ š‘‰ ∧ (š‘¦ ∈ šµ ∧ š‘„ = āŸØš“, š‘¦āŸ©)) → ((2nd ā€˜š‘„) = š‘¦ ∧ š‘„ ∈ ({š“} Ɨ šµ)))
4228, 41impbida 596 . . . . . . . 8 (š“ ∈ š‘‰ → (((2nd ā€˜š‘„) = š‘¦ ∧ š‘„ ∈ ({š“} Ɨ šµ)) ↔ (š‘¦ ∈ šµ ∧ š‘„ = āŸØš“, š‘¦āŸ©)))
4314, 42bitr3id 194 . . . . . . 7 (š“ ∈ š‘‰ → ((š‘„2nd š‘¦ ∧ š‘„ ∈ ({š“} Ɨ šµ)) ↔ (š‘¦ ∈ šµ ∧ š‘„ = āŸØš“, š‘¦āŸ©)))
447, 43bitrid 192 . . . . . 6 (š“ ∈ š‘‰ → (š‘„(2nd ↾ ({š“} Ɨ šµ))š‘¦ ↔ (š‘¦ ∈ šµ ∧ š‘„ = āŸØš“, š‘¦āŸ©)))
4544mobidv 2062 . . . . 5 (š“ ∈ š‘‰ → (∃*š‘„ š‘„(2nd ↾ ({š“} Ɨ šµ))š‘¦ ↔ ∃*š‘„(š‘¦ ∈ šµ ∧ š‘„ = āŸØš“, š‘¦āŸ©)))
465, 45mpbiri 168 . . . 4 (š“ ∈ š‘‰ → ∃*š‘„ š‘„(2nd ↾ ({š“} Ɨ šµ))š‘¦)
4746alrimiv 1874 . . 3 (š“ ∈ š‘‰ → āˆ€š‘¦āˆƒ*š‘„ š‘„(2nd ↾ ({š“} Ɨ šµ))š‘¦)
48 funcnv2 5278 . . 3 (Fun ā—”(2nd ↾ ({š“} Ɨ šµ)) ↔ āˆ€š‘¦āˆƒ*š‘„ š‘„(2nd ↾ ({š“} Ɨ šµ))š‘¦)
4947, 48sylibr 134 . 2 (š“ ∈ š‘‰ → Fun ā—”(2nd ↾ ({š“} Ɨ šµ)))
50 dff1o3 5469 . 2 ((2nd ↾ ({š“} Ɨ šµ)):({š“} Ɨ šµ)–1-1-ontoā†’šµ ↔ ((2nd ↾ ({š“} Ɨ šµ)):({š“} Ɨ šµ)–ontoā†’šµ ∧ Fun ā—”(2nd ↾ ({š“} Ɨ šµ))))
513, 49, 50sylanbrc 417 1 (š“ ∈ š‘‰ → (2nd ↾ ({š“} Ɨ šµ)):({š“} Ɨ šµ)–1-1-ontoā†’šµ)
Colors of variables: wff set class
Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  āˆ€wal 1351   = wceq 1353  āˆƒwex 1492  āˆƒ*wmo 2027   ∈ wcel 2148  Vcvv 2739  {csn 3594  āŸØcop 3597   class class class wbr 4005   Ɨ cxp 4626  ā—”ccnv 4627   ↾ cres 4630  Fun wfun 5212   Fn wfn 5213  ā€“onto→wfo 5216  ā€“1-1-onto→wf1o 5217  ā€˜cfv 5218  1st c1st 6142  2nd c2nd 6143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-1st 6144  df-2nd 6145
This theorem is referenced by:  xpfi  6932  fsum2dlemstep  11445  fprod2dlemstep  11633
  Copyright terms: Public domain W3C validator