MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fprg Structured version   Visualization version   Unicode version
Theorem fprg 6422
Description: A function with a domain of two elements. (Contributed by FL, 2-Feb-2014.)
Assertion
Ref Expression
fprg |- ( ( ( A e. E /\ B e. F ) /\ ( C e. G /\ D e. H ) /\ A =/= B ) -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } )
Proof of Theorem fprg
StepHypRef Expression
1 elex 3212 . . . 4 |- ( A e. E -> A e. _V )
2 elex 3212 . . . 4 |- ( B e. F -> B e. _V )
31, 2anim12i 590 . . 3 |- ( ( A e. E /\ B e. F ) -> ( A e. _V /\ B e. _V ) )
4 elex 3212 . . . 4 |- ( C e. G -> C e. _V )
5 elex 3212 . . . 4 |- ( D e. H -> D e. _V )
64, 5anim12i 590 . . 3 |- ( ( C e. G /\ D e. H ) -> ( C e. _V /\ D e. _V ) )
7 neeq1 2856 . . . . 5 |- ( A = if ( A e. _V , A , (/) ) -> ( A =/= B <-> if ( A e. _V , A , (/) ) =/= B ) )
8 opeq1 4402 . . . . . . 7 |- ( A = if ( A e. _V , A , (/) ) -> <. A , C >. = <. if ( A e. _V , A , (/) ) , C >. )
98preq1d 4274 . . . . . 6 |- ( A = if ( A e. _V , A , (/) ) -> { <. A , C >. , <. B , D >. } = { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } )
10 preq1 4268 . . . . . 6 |- ( A = if ( A e. _V , A , (/) ) -> { A , B } = { if ( A e. _V , A , (/) ) , B } )
119, 10feq12d 6033 . . . . 5 |- ( A = if ( A e. _V , A , (/) ) -> ( { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } <-> { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } : { if ( A e. _V , A , (/) ) , B } --> { C , D } ) )
127, 11imbi12d 334 . . . 4 |- ( A = if ( A e. _V , A , (/) ) -> ( ( A =/= B -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } ) <-> ( if ( A e. _V , A , (/) ) =/= B -> { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } : { if ( A e. _V , A , (/) ) , B } --> { C , D } ) ) )
13 neeq2 2857 . . . . 5 |- ( B = if ( B e. _V , B , (/) ) -> ( if ( A e. _V , A , (/) ) =/= B <-> if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) ) )
14 opeq1 4402 . . . . . . 7 |- ( B = if ( B e. _V , B , (/) ) -> <. B , D >. = <. if ( B e. _V , B , (/) ) , D >. )
1514preq2d 4275 . . . . . 6 |- ( B = if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } = { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } )
16 preq2 4269 . . . . . 6 |- ( B = if ( B e. _V , B , (/) ) -> { if ( A e. _V , A , (/) ) , B } = { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } )
1715, 16feq12d 6033 . . . . 5 |- ( B = if ( B e. _V , B , (/) ) -> ( { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } : { if ( A e. _V , A , (/) ) , B } --> { C , D } <-> { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { C , D } ) )
1813, 17imbi12d 334 . . . 4 |- ( B = if ( B e. _V , B , (/) ) -> ( ( if ( A e. _V , A , (/) ) =/= B -> { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } : { if ( A e. _V , A , (/) ) , B } --> { C , D } ) <-> ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { C , D } ) ) )
19 opeq2 4403 . . . . . . 7 |- ( C = if ( C e. _V , C , (/) ) -> <. if ( A e. _V , A , (/) ) , C >. = <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. )
2019preq1d 4274 . . . . . 6 |- ( C = if ( C e. _V , C , (/) ) -> { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } = { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } )
21 eqidd 2623 . . . . . 6 |- ( C = if ( C e. _V , C , (/) ) -> { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } = { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } )
22 preq1 4268 . . . . . 6 |- ( C = if ( C e. _V , C , (/) ) -> { C , D } = { if ( C e. _V , C , (/) ) , D } )
2320, 21, 22feq123d 6034 . . . . 5 |- ( C = if ( C e. _V , C , (/) ) -> ( { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { C , D } <-> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , D } ) )
2423imbi2d 330 . . . 4 |- ( C = if ( C e. _V , C , (/) ) -> ( ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { C , D } ) <-> ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , D } ) ) )
25 opeq2 4403 . . . . . . 7 |- ( D = if ( D e. _V , D , (/) ) -> <. if ( B e. _V , B , (/) ) , D >. = <. if ( B e. _V , B , (/) ) , if ( D e. _V , D , (/) ) >. )
2625preq2d 4275 . . . . . 6 |- ( D = if ( D e. _V , D , (/) ) -> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } = { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , if ( D e. _V , D , (/) ) >. } )
27 eqidd 2623 . . . . . 6 |- ( D = if ( D e. _V , D , (/) ) -> { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } = { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } )
28 preq2 4269 . . . . . 6 |- ( D = if ( D e. _V , D , (/) ) -> { if ( C e. _V , C , (/) ) , D } = { if ( C e. _V , C , (/) ) , if ( D e. _V , D , (/) ) } )
2926, 27, 28feq123d 6034 . . . . 5 |- ( D = if ( D e. _V , D , (/) ) -> ( { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , D } <-> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , if ( D e. _V , D , (/) ) >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , if ( D e. _V , D , (/) ) } ) )
3029imbi2d 330 . . . 4 |- ( D = if ( D e. _V , D , (/) ) -> ( ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , D } ) <-> ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , if ( D e. _V , D , (/) ) >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , if ( D e. _V , D , (/) ) } ) ) )
31 0ex 4790 . . . . . 6 |- (/) e. _V
3231elimel 4150 . . . . 5 |- if ( A e. _V , A , (/) ) e. _V
3331elimel 4150 . . . . 5 |- if ( B e. _V , B , (/) ) e. _V
3431elimel 4150 . . . . 5 |- if ( C e. _V , C , (/) ) e. _V
3531elimel 4150 . . . . 5 |- if ( D e. _V , D , (/) ) e. _V
3632, 33, 34, 35fpr 6421 . . . 4 |- ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , if ( D e. _V , D , (/) ) >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , if ( D e. _V , D , (/) ) } )
3712, 18, 24, 30, 36dedth4h 4142 . . 3 |- ( ( ( A e. _V /\ B e. _V ) /\ ( C e. _V /\ D e. _V ) ) -> ( A =/= B -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } ) )
383, 6, 37syl2an 494 . 2 |- ( ( ( A e. E /\ B e. F ) /\ ( C e. G /\ D e. H ) ) -> ( A =/= B -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } ) )
39383impia 1261 1 |- ( ( ( A e. E /\ B e. F ) /\ ( C e. G /\ D e. H ) /\ A =/= B ) -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   _Vcvv 3200   (/)c0 3915   ifcif 4086   {cpr 4179   <.cop 4183   -->wf 5884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-fun 5890  df-fn 5891  df-f 5892
This theorem is referenced by:  ftpg  6423  fpropnf1  6524  wrdlen2i  13686  umgr2v2e  26421  mapprop  42124  zlmodzxzel  42133  ldepspr  42262  zlmodzxzldeplem1  42289
  Copyright terms: Public domain W3C validator