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

Theorem fvn0ssdmfun 6035
Description: If a class' function values for certain arguments is not the empty set, the arguments are contained in the domain of the class, and the class restricted to the arguments is a function, analogous to fvfundmfvn0 5919. (Contributed by AV, 27-Jan-2020.)
Assertion
Ref Expression
fvn0ssdmfun  |-  ( A. a  e.  D  ( F `  a )  =/=  (/)  ->  ( D  C_ 
dom  F  /\  Fun  ( F  |`  D ) ) )
Distinct variable groups:    D, a    F, a

Proof of Theorem fvn0ssdmfun
Dummy variables  p  x  y  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvfundmfvn0 5919 . . 3  |-  ( ( F `  a )  =/=  (/)  ->  ( a  e.  dom  F  /\  Fun  ( F  |`  { a } ) ) )
21ralimi 2792 . 2  |-  ( A. a  e.  D  ( F `  a )  =/=  (/)  ->  A. a  e.  D  ( a  e.  dom  F  /\  Fun  ( F  |`  { a } ) ) )
3 r19.26 2928 . . 3  |-  ( A. a  e.  D  (
a  e.  dom  F  /\  Fun  ( F  |`  { a } ) )  <->  ( A. a  e.  D  a  e.  dom  F  /\  A. a  e.  D  Fun  ( F  |`  { a } ) ) )
4 eleq1 2527 . . . . . 6  |-  ( a  =  p  ->  (
a  e.  dom  F  <->  p  e.  dom  F ) )
54rspccv 3158 . . . . 5  |-  ( A. a  e.  D  a  e.  dom  F  ->  (
p  e.  D  ->  p  e.  dom  F ) )
65ssrdv 3449 . . . 4  |-  ( A. a  e.  D  a  e.  dom  F  ->  D  C_ 
dom  F )
7 funrel 5617 . . . . . . . 8  |-  ( Fun  ( F  |`  { a } )  ->  Rel  ( F  |`  { a } ) )
87ralimi 2792 . . . . . . 7  |-  ( A. a  e.  D  Fun  ( F  |`  { a } )  ->  A. a  e.  D  Rel  ( F  |`  { a } ) )
9 reliun 4972 . . . . . . 7  |-  ( Rel  U_ a  e.  D  ( F  |`  { a } )  <->  A. a  e.  D  Rel  ( F  |`  { a } ) )
108, 9sylibr 217 . . . . . 6  |-  ( A. a  e.  D  Fun  ( F  |`  { a } )  ->  Rel  U_ a  e.  D  ( F  |`  { a } ) )
11 sneq 3989 . . . . . . . . . . . . . 14  |-  ( a  =  x  ->  { a }  =  { x } )
1211reseq2d 5123 . . . . . . . . . . . . 13  |-  ( a  =  x  ->  ( F  |`  { a } )  =  ( F  |`  { x } ) )
1312funeqd 5621 . . . . . . . . . . . 12  |-  ( a  =  x  ->  ( Fun  ( F  |`  { a } )  <->  Fun  ( F  |`  { x } ) ) )
1413rspcva 3159 . . . . . . . . . . 11  |-  ( ( x  e.  D  /\  A. a  e.  D  Fun  ( F  |`  { a } ) )  ->  Fun  ( F  |`  { x } ) )
15 dffun5 5613 . . . . . . . . . . . 12  |-  ( Fun  ( F  |`  { x } )  <->  ( Rel  ( F  |`  { x } )  /\  A. w E. y A. z
( <. w ,  z
>.  e.  ( F  |`  { x } )  ->  z  =  y ) ) )
16 vex 3059 . . . . . . . . . . . . . . . . . . 19  |-  x  e. 
_V
1716elsnres 5159 . . . . . . . . . . . . . . . . . 18  |-  ( <.
w ,  z >.  e.  ( F  |`  { x } )  <->  E. a
( <. w ,  z
>.  =  <. x ,  a >.  /\  <. x ,  a >.  e.  F
) )
1817imbi1i 331 . . . . . . . . . . . . . . . . 17  |-  ( (
<. w ,  z >.  e.  ( F  |`  { x } )  ->  z  =  y )  <->  ( E. a ( <. w ,  z >.  =  <. x ,  a >.  /\  <. x ,  a >.  e.  F
)  ->  z  =  y ) )
1918albii 1701 . . . . . . . . . . . . . . . 16  |-  ( A. z ( <. w ,  z >.  e.  ( F  |`  { x } )  ->  z  =  y )  <->  A. z
( E. a (
<. w ,  z >.  =  <. x ,  a
>.  /\  <. x ,  a
>.  e.  F )  -> 
z  =  y ) )
2019exbii 1728 . . . . . . . . . . . . . . 15  |-  ( E. y A. z (
<. w ,  z >.  e.  ( F  |`  { x } )  ->  z  =  y )  <->  E. y A. z ( E. a
( <. w ,  z
>.  =  <. x ,  a >.  /\  <. x ,  a >.  e.  F
)  ->  z  =  y ) )
2120albii 1701 . . . . . . . . . . . . . 14  |-  ( A. w E. y A. z
( <. w ,  z
>.  e.  ( F  |`  { x } )  ->  z  =  y )  <->  A. w E. y A. z ( E. a
( <. w ,  z
>.  =  <. x ,  a >.  /\  <. x ,  a >.  e.  F
)  ->  z  =  y ) )
22 equcom 1872 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  z  <->  z  =  a )
23 opeq12 4181 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( w  =  x  /\  z  =  a )  -> 
<. w ,  z >.  =  <. x ,  a
>. )
2423ex 440 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  x  ->  (
z  =  a  ->  <. w ,  z >.  =  <. x ,  a
>. ) )
2522, 24syl5bi 225 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  =  x  ->  (
a  =  z  ->  <. w ,  z >.  =  <. x ,  a
>. ) )
2625adantr 471 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( w  =  x  /\  <.
x ,  z >.  e.  F )  ->  (
a  =  z  ->  <. w ,  z >.  =  <. x ,  a
>. ) )
2726impcom 436 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  =  z  /\  ( w  =  x  /\  <. x ,  z
>.  e.  F ) )  ->  <. w ,  z
>.  =  <. x ,  a >. )
28 opeq2 4180 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  a  ->  <. x ,  z >.  =  <. x ,  a >. )
2928equcoms 1874 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  z  ->  <. x ,  z >.  =  <. x ,  a >. )
3029eleq1d 2523 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  z  ->  ( <. x ,  z >.  e.  F  <->  <. x ,  a
>.  e.  F ) )
3130biimpcd 232 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
x ,  z >.  e.  F  ->  ( a  =  z  ->  <. x ,  a >.  e.  F
) )
3231adantl 472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( w  =  x  /\  <.
x ,  z >.  e.  F )  ->  (
a  =  z  ->  <. x ,  a >.  e.  F ) )
3332impcom 436 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  =  z  /\  ( w  =  x  /\  <. x ,  z
>.  e.  F ) )  ->  <. x ,  a
>.  e.  F )
3427, 33jca 539 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( a  =  z  /\  ( w  =  x  /\  <. x ,  z
>.  e.  F ) )  ->  ( <. w ,  z >.  =  <. x ,  a >.  /\  <. x ,  a >.  e.  F
) )
3534ex 440 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  z  ->  (
( w  =  x  /\  <. x ,  z
>.  e.  F )  -> 
( <. w ,  z
>.  =  <. x ,  a >.  /\  <. x ,  a >.  e.  F
) ) )
3635spimev 2113 . . . . . . . . . . . . . . . . . . 19  |-  ( ( w  =  x  /\  <.
x ,  z >.  e.  F )  ->  E. a
( <. w ,  z
>.  =  <. x ,  a >.  /\  <. x ,  a >.  e.  F
) )
3736ex 440 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  x  ->  ( <. x ,  z >.  e.  F  ->  E. a
( <. w ,  z
>.  =  <. x ,  a >.  /\  <. x ,  a >.  e.  F
) ) )
3837imim1d 78 . . . . . . . . . . . . . . . . 17  |-  ( w  =  x  ->  (
( E. a (
<. w ,  z >.  =  <. x ,  a
>.  /\  <. x ,  a
>.  e.  F )  -> 
z  =  y )  ->  ( <. x ,  z >.  e.  F  ->  z  =  y ) ) )
3938alimdv 1773 . . . . . . . . . . . . . . . 16  |-  ( w  =  x  ->  ( A. z ( E. a
( <. w ,  z
>.  =  <. x ,  a >.  /\  <. x ,  a >.  e.  F
)  ->  z  =  y )  ->  A. z
( <. x ,  z
>.  e.  F  ->  z  =  y ) ) )
4039eximdv 1774 . . . . . . . . . . . . . . 15  |-  ( w  =  x  ->  ( E. y A. z ( E. a ( <.
w ,  z >.  =  <. x ,  a
>.  /\  <. x ,  a
>.  e.  F )  -> 
z  =  y )  ->  E. y A. z
( <. x ,  z
>.  e.  F  ->  z  =  y ) ) )
4140spimvw 1853 . . . . . . . . . . . . . 14  |-  ( A. w E. y A. z
( E. a (
<. w ,  z >.  =  <. x ,  a
>.  /\  <. x ,  a
>.  e.  F )  -> 
z  =  y )  ->  E. y A. z
( <. x ,  z
>.  e.  F  ->  z  =  y ) )
4221, 41sylbi 200 . . . . . . . . . . . . 13  |-  ( A. w E. y A. z
( <. w ,  z
>.  e.  ( F  |`  { x } )  ->  z  =  y )  ->  E. y A. z ( <. x ,  z >.  e.  F  ->  z  =  y ) )
4342adantl 472 . . . . . . . . . . . 12  |-  ( ( Rel  ( F  |`  { x } )  /\  A. w E. y A. z ( <.
w ,  z >.  e.  ( F  |`  { x } )  ->  z  =  y ) )  ->  E. y A. z
( <. x ,  z
>.  e.  F  ->  z  =  y ) )
4415, 43sylbi 200 . . . . . . . . . . 11  |-  ( Fun  ( F  |`  { x } )  ->  E. y A. z ( <. x ,  z >.  e.  F  ->  z  =  y ) )
4514, 44syl 17 . . . . . . . . . 10  |-  ( ( x  e.  D  /\  A. a  e.  D  Fun  ( F  |`  { a } ) )  ->  E. y A. z (
<. x ,  z >.  e.  F  ->  z  =  y ) )
4645expcom 441 . . . . . . . . 9  |-  ( A. a  e.  D  Fun  ( F  |`  { a } )  ->  (
x  e.  D  ->  E. y A. z (
<. x ,  z >.  e.  F  ->  z  =  y ) ) )
47 ancomst 458 . . . . . . . . . . . . 13  |-  ( ( ( <. x ,  z
>.  e.  F  /\  x  e.  D )  ->  z  =  y )  <->  ( (
x  e.  D  /\  <.
x ,  z >.  e.  F )  ->  z  =  y ) )
48 impexp 452 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  D  /\  <. x ,  z
>.  e.  F )  -> 
z  =  y )  <-> 
( x  e.  D  ->  ( <. x ,  z
>.  e.  F  ->  z  =  y ) ) )
4947, 48bitri 257 . . . . . . . . . . . 12  |-  ( ( ( <. x ,  z
>.  e.  F  /\  x  e.  D )  ->  z  =  y )  <->  ( x  e.  D  ->  ( <.
x ,  z >.  e.  F  ->  z  =  y ) ) )
5049albii 1701 . . . . . . . . . . 11  |-  ( A. z ( ( <.
x ,  z >.  e.  F  /\  x  e.  D )  ->  z  =  y )  <->  A. z
( x  e.  D  ->  ( <. x ,  z
>.  e.  F  ->  z  =  y ) ) )
5150exbii 1728 . . . . . . . . . 10  |-  ( E. y A. z ( ( <. x ,  z
>.  e.  F  /\  x  e.  D )  ->  z  =  y )  <->  E. y A. z ( x  e.  D  ->  ( <. x ,  z >.  e.  F  ->  z  =  y ) ) )
52 19.21v 1796 . . . . . . . . . . 11  |-  ( A. z ( x  e.  D  ->  ( <. x ,  z >.  e.  F  ->  z  =  y ) )  <->  ( x  e.  D  ->  A. z
( <. x ,  z
>.  e.  F  ->  z  =  y ) ) )
5352exbii 1728 . . . . . . . . . 10  |-  ( E. y A. z ( x  e.  D  -> 
( <. x ,  z
>.  e.  F  ->  z  =  y ) )  <->  E. y ( x  e.  D  ->  A. z
( <. x ,  z
>.  e.  F  ->  z  =  y ) ) )
54 19.37v 1836 . . . . . . . . . 10  |-  ( E. y ( x  e.  D  ->  A. z
( <. x ,  z
>.  e.  F  ->  z  =  y ) )  <-> 
( x  e.  D  ->  E. y A. z
( <. x ,  z
>.  e.  F  ->  z  =  y ) ) )
5551, 53, 543bitri 279 . . . . . . . . 9  |-  ( E. y A. z ( ( <. x ,  z
>.  e.  F  /\  x  e.  D )  ->  z  =  y )  <->  ( x  e.  D  ->  E. y A. z ( <. x ,  z >.  e.  F  ->  z  =  y ) ) )
5646, 55sylibr 217 . . . . . . . 8  |-  ( A. a  e.  D  Fun  ( F  |`  { a } )  ->  E. y A. z ( ( <.
x ,  z >.  e.  F  /\  x  e.  D )  ->  z  =  y ) )
5756alrimiv 1783 . . . . . . 7  |-  ( A. a  e.  D  Fun  ( F  |`  { a } )  ->  A. x E. y A. z ( ( <. x ,  z
>.  e.  F  /\  x  e.  D )  ->  z  =  y ) )
58 resiun2 5142 . . . . . . . . . . . . . 14  |-  ( F  |`  U_ a  e.  D  { a } )  =  U_ a  e.  D  ( F  |`  { a } )
5958eqcomi 2470 . . . . . . . . . . . . 13  |-  U_ a  e.  D  ( F  |` 
{ a } )  =  ( F  |`  U_ a  e.  D  {
a } )
6059eleq2i 2531 . . . . . . . . . . . 12  |-  ( <.
x ,  z >.  e.  U_ a  e.  D  ( F  |`  { a } )  <->  <. x ,  z >.  e.  ( F  |`  U_ a  e.  D  { a } ) )
61 iunid 4346 . . . . . . . . . . . . . 14  |-  U_ a  e.  D  { a }  =  D
6261reseq2i 5120 . . . . . . . . . . . . 13  |-  ( F  |`  U_ a  e.  D  { a } )  =  ( F  |`  D )
6362eleq2i 2531 . . . . . . . . . . . 12  |-  ( <.
x ,  z >.  e.  ( F  |`  U_ a  e.  D  { a } )  <->  <. x ,  z >.  e.  ( F  |`  D ) )
64 vex 3059 . . . . . . . . . . . . 13  |-  z  e. 
_V
6564opelres 5128 . . . . . . . . . . . 12  |-  ( <.
x ,  z >.  e.  ( F  |`  D )  <-> 
( <. x ,  z
>.  e.  F  /\  x  e.  D ) )
6660, 63, 653bitri 279 . . . . . . . . . . 11  |-  ( <.
x ,  z >.  e.  U_ a  e.  D  ( F  |`  { a } )  <->  ( <. x ,  z >.  e.  F  /\  x  e.  D
) )
6766imbi1i 331 . . . . . . . . . 10  |-  ( (
<. x ,  z >.  e.  U_ a  e.  D  ( F  |`  { a } )  ->  z  =  y )  <->  ( ( <. x ,  z >.  e.  F  /\  x  e.  D )  ->  z  =  y ) )
6867albii 1701 . . . . . . . . 9  |-  ( A. z ( <. x ,  z >.  e.  U_ a  e.  D  ( F  |`  { a } )  ->  z  =  y )  <->  A. z
( ( <. x ,  z >.  e.  F  /\  x  e.  D
)  ->  z  =  y ) )
6968exbii 1728 . . . . . . . 8  |-  ( E. y A. z (
<. x ,  z >.  e.  U_ a  e.  D  ( F  |`  { a } )  ->  z  =  y )  <->  E. y A. z ( ( <.
x ,  z >.  e.  F  /\  x  e.  D )  ->  z  =  y ) )
7069albii 1701 . . . . . . 7  |-  ( A. x E. y A. z
( <. x ,  z
>.  e.  U_ a  e.  D  ( F  |`  { a } )  ->  z  =  y )  <->  A. x E. y A. z ( ( <.
x ,  z >.  e.  F  /\  x  e.  D )  ->  z  =  y ) )
7157, 70sylibr 217 . . . . . 6  |-  ( A. a  e.  D  Fun  ( F  |`  { a } )  ->  A. x E. y A. z (
<. x ,  z >.  e.  U_ a  e.  D  ( F  |`  { a } )  ->  z  =  y ) )
72 dffun5 5613 . . . . . 6  |-  ( Fun  U_ a  e.  D  ( F  |`  { a } )  <->  ( Rel  U_ a  e.  D  ( F  |`  { a } )  /\  A. x E. y A. z
( <. x ,  z
>.  e.  U_ a  e.  D  ( F  |`  { a } )  ->  z  =  y ) ) )
7310, 71, 72sylanbrc 675 . . . . 5  |-  ( A. a  e.  D  Fun  ( F  |`  { a } )  ->  Fun  U_ a  e.  D  ( F  |`  { a } ) )
7461eqcomi 2470 . . . . . . . 8  |-  D  = 
U_ a  e.  D  { a }
7574reseq2i 5120 . . . . . . 7  |-  ( F  |`  D )  =  ( F  |`  U_ a  e.  D  { a } )
7675funeqi 5620 . . . . . 6  |-  ( Fun  ( F  |`  D )  <->  Fun  ( F  |`  U_ a  e.  D  { a } ) )
7758funeqi 5620 . . . . . 6  |-  ( Fun  ( F  |`  U_ a  e.  D  { a } )  <->  Fun  U_ a  e.  D  ( F  |` 
{ a } ) )
7876, 77bitri 257 . . . . 5  |-  ( Fun  ( F  |`  D )  <->  Fun  U_ a  e.  D  ( F  |`  { a } ) )
7973, 78sylibr 217 . . . 4  |-  ( A. a  e.  D  Fun  ( F  |`  { a } )  ->  Fun  ( F  |`  D ) )
806, 79anim12i 574 . . 3  |-  ( ( A. a  e.  D  a  e.  dom  F  /\  A. a  e.  D  Fun  ( F  |`  { a } ) )  -> 
( D  C_  dom  F  /\  Fun  ( F  |`  D ) ) )
813, 80sylbi 200 . 2  |-  ( A. a  e.  D  (
a  e.  dom  F  /\  Fun  ( F  |`  { a } ) )  ->  ( D  C_ 
dom  F  /\  Fun  ( F  |`  D ) ) )
822, 81syl 17 1  |-  ( A. a  e.  D  ( F `  a )  =/=  (/)  ->  ( D  C_ 
dom  F  /\  Fun  ( F  |`  D ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375   A.wal 1452    = wceq 1454   E.wex 1673    e. wcel 1897    =/= wne 2632   A.wral 2748    C_ wss 3415   (/)c0 3742   {csn 3979   <.cop 3985   U_ciun 4291   dom cdm 4852    |` cres 4854   Rel wrel 4857   Fun wfun 5594   ` cfv 5600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-sbc 3279  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-iun 4293  df-br 4416  df-opab 4475  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-res 4864  df-iota 5564  df-fun 5602  df-fv 5608
This theorem is referenced by:  fveqressseq  6040  ovn0ssdmfun  40039
  Copyright terms: Public domain W3C validator