MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elmpt2cl Structured version   Unicode version

Theorem elmpt2cl 6521
Description: If a two-parameter class is not empty, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015.)
Hypothesis
Ref Expression
elmpt2cl.f  |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )
Assertion
Ref Expression
elmpt2cl  |-  ( X  e.  ( S F T )  ->  ( S  e.  A  /\  T  e.  B )
)
Distinct variable groups:    x, A, y    x, B, y
Allowed substitution hints:    C( x, y)    S( x, y)    T( x, y)    F( x, y)    X( x, y)

Proof of Theorem elmpt2cl
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 elmpt2cl.f . . . . . 6  |-  F  =  ( x  e.  A ,  y  e.  B  |->  C )
2 df-mpt2 6306 . . . . . 6  |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
31, 2eqtri 2451 . . . . 5  |-  F  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
43dmeqi 5051 . . . 4  |-  dom  F  =  dom  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  A  /\  y  e.  B )  /\  z  =  C
) }
5 dmoprabss 6388 . . . 4  |-  dom  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }  C_  ( A  X.  B
)
64, 5eqsstri 3494 . . 3  |-  dom  F  C_  ( A  X.  B
)
7 elfvdm 5903 . . . 4  |-  ( X  e.  ( F `  <. S ,  T >. )  ->  <. S ,  T >.  e.  dom  F )
8 df-ov 6304 . . . 4  |-  ( S F T )  =  ( F `  <. S ,  T >. )
97, 8eleq2s 2530 . . 3  |-  ( X  e.  ( S F T )  ->  <. S ,  T >.  e.  dom  F
)
106, 9sseldi 3462 . 2  |-  ( X  e.  ( S F T )  ->  <. S ,  T >.  e.  ( A  X.  B ) )
11 opelxp 4879 . 2  |-  ( <. S ,  T >.  e.  ( A  X.  B
)  <->  ( S  e.  A  /\  T  e.  B ) )
1210, 11sylib 199 1  |-  ( X  e.  ( S F T )  ->  ( S  e.  A  /\  T  e.  B )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1868   <.cop 4002    X. cxp 4847   dom cdm 4849   ` cfv 5597  (class class class)co 6301   {coprab 6302    |-> cmpt2 6303
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-xp 4855  df-dm 4859  df-iota 5561  df-fv 5605  df-ov 6304  df-oprab 6305  df-mpt2 6306
This theorem is referenced by:  elmpt2cl1  6522  elmpt2cl2  6523  elovmpt2  6524  elovmpt2rab  6525  elovmpt2rab1  6526  ixxssixx  11649  funcrcl  15753  natrcl  15840  ismhm  16569  isghm  16868  isga  16930  isslw  17245  isrhm  17934  rimrcl  17937  islmhm  18235  iscn2  20238  elflim2  20963  isfcls  21008  isnmhm  21751  limcrcl  22813  clwlkswlks  25469  clwwlkprop  25481  iscvm  29975  mclsrcl  30192  mgmhmrcl  38967  intop  39025  rnghmrcl  39075  rngimrcl  39083
  Copyright terms: Public domain W3C validator