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

Theorem fvn0ssdmfun 5998
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 5880. (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 5880 . . 3  |-  ( ( F `  a )  =/=  (/)  ->  ( a  e.  dom  F  /\  Fun  ( F  |`  { a } ) ) )
21ralimi 2847 . 2  |-  ( A. a  e.  D  ( F `  a )  =/=  (/)  ->  A. a  e.  D  ( a  e.  dom  F  /\  Fun  ( F  |`  { a } ) ) )
3 r19.26 2981 . . 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 2526 . . . . . 6  |-  ( a  =  p  ->  (
a  e.  dom  F  <->  p  e.  dom  F ) )
54rspccv 3204 . . . . 5  |-  ( A. a  e.  D  a  e.  dom  F  ->  (
p  e.  D  ->  p  e.  dom  F ) )
65ssrdv 3495 . . . 4  |-  ( A. a  e.  D  a  e.  dom  F  ->  D  C_ 
dom  F )
7 funrel 5587 . . . . . . . 8  |-  ( Fun  ( F  |`  { a } )  ->  Rel  ( F  |`  { a } ) )
87ralimi 2847 . . . . . . 7  |-  ( A. a  e.  D  Fun  ( F  |`  { a } )  ->  A. a  e.  D  Rel  ( F  |`  { a } ) )
9 reliun 5111 . . . . . . 7  |-  ( Rel  U_ a  e.  D  ( F  |`  { a } )  <->  A. a  e.  D  Rel  ( F  |`  { a } ) )
108, 9sylibr 212 . . . . . 6  |-  ( A. a  e.  D  Fun  ( F  |`  { a } )  ->  Rel  U_ a  e.  D  ( F  |`  { a } ) )
11 sneq 4026 . . . . . . . . . . . . . 14  |-  ( a  =  x  ->  { a }  =  { x } )
1211reseq2d 5262 . . . . . . . . . . . . 13  |-  ( a  =  x  ->  ( F  |`  { a } )  =  ( F  |`  { x } ) )
1312funeqd 5591 . . . . . . . . . . . 12  |-  ( a  =  x  ->  ( Fun  ( F  |`  { a } )  <->  Fun  ( F  |`  { x } ) ) )
1413rspcva 3205 . . . . . . . . . . 11  |-  ( ( x  e.  D  /\  A. a  e.  D  Fun  ( F  |`  { a } ) )  ->  Fun  ( F  |`  { x } ) )
15 dffun5 5583 . . . . . . . . . . . 12  |-  ( Fun  ( F  |`  { x } )  <->  ( Rel  ( F  |`  { x } )  /\  A. w E. y A. z
( <. w ,  z
>.  e.  ( F  |`  { x } )  ->  z  =  y ) ) )
16 vex 3109 . . . . . . . . . . . . . . . . . . 19  |-  x  e. 
_V
1716elsnres 5298 . . . . . . . . . . . . . . . . . 18  |-  ( <.
w ,  z >.  e.  ( F  |`  { x } )  <->  E. a
( <. w ,  z
>.  =  <. x ,  a >.  /\  <. x ,  a >.  e.  F
) )
1817imbi1i 323 . . . . . . . . . . . . . . . . 17  |-  ( (
<. w ,  z >.  e.  ( F  |`  { x } )  ->  z  =  y )  <->  ( E. a ( <. w ,  z >.  =  <. x ,  a >.  /\  <. x ,  a >.  e.  F
)  ->  z  =  y ) )
1918albii 1645 . . . . . . . . . . . . . . . 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 1672 . . . . . . . . . . . . . . 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 1645 . . . . . . . . . . . . . 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 1799 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  z  <->  z  =  a )
23 opeq12 4205 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( w  =  x  /\  z  =  a )  -> 
<. w ,  z >.  =  <. x ,  a
>. )
2423ex 432 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  x  ->  (
z  =  a  ->  <. w ,  z >.  =  <. x ,  a
>. ) )
2522, 24syl5bi 217 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  =  x  ->  (
a  =  z  ->  <. w ,  z >.  =  <. x ,  a
>. ) )
2625adantr 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( w  =  x  /\  <.
x ,  z >.  e.  F )  ->  (
a  =  z  ->  <. w ,  z >.  =  <. x ,  a
>. ) )
2726impcom 428 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  =  z  /\  ( w  =  x  /\  <. x ,  z
>.  e.  F ) )  ->  <. w ,  z
>.  =  <. x ,  a >. )
28 opeq2 4204 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  a  ->  <. x ,  z >.  =  <. x ,  a >. )
2928equcoms 1800 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  z  ->  <. x ,  z >.  =  <. x ,  a >. )
3029eleq1d 2523 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  z  ->  ( <. x ,  z >.  e.  F  <->  <. x ,  a
>.  e.  F ) )
3130biimpcd 224 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( <.
x ,  z >.  e.  F  ->  ( a  =  z  ->  <. x ,  a >.  e.  F
) )
3231adantl 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( w  =  x  /\  <.
x ,  z >.  e.  F )  ->  (
a  =  z  ->  <. x ,  a >.  e.  F ) )
3332impcom 428 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  =  z  /\  ( w  =  x  /\  <. x ,  z
>.  e.  F ) )  ->  <. x ,  a
>.  e.  F )
3427, 33jca 530 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( a  =  z  /\  ( w  =  x  /\  <. x ,  z
>.  e.  F ) )  ->  ( <. w ,  z >.  =  <. x ,  a >.  /\  <. x ,  a >.  e.  F
) )
3534ex 432 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  z  ->  (
( w  =  x  /\  <. x ,  z
>.  e.  F )  -> 
( <. w ,  z
>.  =  <. x ,  a >.  /\  <. x ,  a >.  e.  F
) ) )
3635spimev 2015 . . . . . . . . . . . . . . . . . . 19  |-  ( ( w  =  x  /\  <.
x ,  z >.  e.  F )  ->  E. a
( <. w ,  z
>.  =  <. x ,  a >.  /\  <. x ,  a >.  e.  F
) )
3736ex 432 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  x  ->  ( <. x ,  z >.  e.  F  ->  E. a
( <. w ,  z
>.  =  <. x ,  a >.  /\  <. x ,  a >.  e.  F
) ) )
3837imim1d 75 . . . . . . . . . . . . . . . . 17  |-  ( w  =  x  ->  (
( E. a (
<. w ,  z >.  =  <. x ,  a
>.  /\  <. x ,  a
>.  e.  F )  -> 
z  =  y )  ->  ( <. x ,  z >.  e.  F  ->  z  =  y ) ) )
3938alimdv 1714 . . . . . . . . . . . . . . . 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 1715 . . . . . . . . . . . . . . 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 1789 . . . . . . . . . . . . . 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 195 . . . . . . . . . . . . 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 464 . . . . . . . . . . . 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 195 . . . . . . . . . . 11  |-  ( Fun  ( F  |`  { x } )  ->  E. y A. z ( <. x ,  z >.  e.  F  ->  z  =  y ) )
4514, 44syl 16 . . . . . . . . . 10  |-  ( ( x  e.  D  /\  A. a  e.  D  Fun  ( F  |`  { a } ) )  ->  E. y A. z (
<. x ,  z >.  e.  F  ->  z  =  y ) )
4645expcom 433 . . . . . . . . 9  |-  ( A. a  e.  D  Fun  ( F  |`  { a } )  ->  (
x  e.  D  ->  E. y A. z (
<. x ,  z >.  e.  F  ->  z  =  y ) ) )
47 ancomst 450 . . . . . . . . . . . . 13  |-  ( ( ( <. x ,  z
>.  e.  F  /\  x  e.  D )  ->  z  =  y )  <->  ( (
x  e.  D  /\  <.
x ,  z >.  e.  F )  ->  z  =  y ) )
48 impexp 444 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  D  /\  <. x ,  z
>.  e.  F )  -> 
z  =  y )  <-> 
( x  e.  D  ->  ( <. x ,  z
>.  e.  F  ->  z  =  y ) ) )
4947, 48bitri 249 . . . . . . . . . . . 12  |-  ( ( ( <. x ,  z
>.  e.  F  /\  x  e.  D )  ->  z  =  y )  <->  ( x  e.  D  ->  ( <.
x ,  z >.  e.  F  ->  z  =  y ) ) )
5049albii 1645 . . . . . . . . . . 11  |-  ( A. z ( ( <.
x ,  z >.  e.  F  /\  x  e.  D )  ->  z  =  y )  <->  A. z
( x  e.  D  ->  ( <. x ,  z
>.  e.  F  ->  z  =  y ) ) )
5150exbii 1672 . . . . . . . . . 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 1734 . . . . . . . . . . 11  |-  ( A. z ( x  e.  D  ->  ( <. x ,  z >.  e.  F  ->  z  =  y ) )  <->  ( x  e.  D  ->  A. z
( <. x ,  z
>.  e.  F  ->  z  =  y ) ) )
5352exbii 1672 . . . . . . . . . 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 1773 . . . . . . . . . 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 271 . . . . . . . . 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 212 . . . . . . . 8  |-  ( A. a  e.  D  Fun  ( F  |`  { a } )  ->  E. y A. z ( ( <.
x ,  z >.  e.  F  /\  x  e.  D )  ->  z  =  y ) )
5756alrimiv 1724 . . . . . . 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 5281 . . . . . . . . . . . . . 14  |-  ( F  |`  U_ a  e.  D  { a } )  =  U_ a  e.  D  ( F  |`  { a } )
5958eqcomi 2467 . . . . . . . . . . . . 13  |-  U_ a  e.  D  ( F  |` 
{ a } )  =  ( F  |`  U_ a  e.  D  {
a } )
6059eleq2i 2532 . . . . . . . . . . . 12  |-  ( <.
x ,  z >.  e.  U_ a  e.  D  ( F  |`  { a } )  <->  <. x ,  z >.  e.  ( F  |`  U_ a  e.  D  { a } ) )
61 iunid 4370 . . . . . . . . . . . . . 14  |-  U_ a  e.  D  { a }  =  D
6261reseq2i 5259 . . . . . . . . . . . . 13  |-  ( F  |`  U_ a  e.  D  { a } )  =  ( F  |`  D )
6362eleq2i 2532 . . . . . . . . . . . 12  |-  ( <.
x ,  z >.  e.  ( F  |`  U_ a  e.  D  { a } )  <->  <. x ,  z >.  e.  ( F  |`  D ) )
64 vex 3109 . . . . . . . . . . . . 13  |-  z  e. 
_V
6564opelres 5267 . . . . . . . . . . . 12  |-  ( <.
x ,  z >.  e.  ( F  |`  D )  <-> 
( <. x ,  z
>.  e.  F  /\  x  e.  D ) )
6660, 63, 653bitri 271 . . . . . . . . . . 11  |-  ( <.
x ,  z >.  e.  U_ a  e.  D  ( F  |`  { a } )  <->  ( <. x ,  z >.  e.  F  /\  x  e.  D
) )
6766imbi1i 323 . . . . . . . . . 10  |-  ( (
<. x ,  z >.  e.  U_ a  e.  D  ( F  |`  { a } )  ->  z  =  y )  <->  ( ( <. x ,  z >.  e.  F  /\  x  e.  D )  ->  z  =  y ) )
6867albii 1645 . . . . . . . . 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 1672 . . . . . . . 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 1645 . . . . . . 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 212 . . . . . 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 5583 . . . . . 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 662 . . . . 5  |-  ( A. a  e.  D  Fun  ( F  |`  { a } )  ->  Fun  U_ a  e.  D  ( F  |`  { a } ) )
7461eqcomi 2467 . . . . . . . 8  |-  D  = 
U_ a  e.  D  { a }
7574reseq2i 5259 . . . . . . 7  |-  ( F  |`  D )  =  ( F  |`  U_ a  e.  D  { a } )
7675funeqi 5590 . . . . . 6  |-  ( Fun  ( F  |`  D )  <->  Fun  ( F  |`  U_ a  e.  D  { a } ) )
7758funeqi 5590 . . . . . 6  |-  ( Fun  ( F  |`  U_ a  e.  D  { a } )  <->  Fun  U_ a  e.  D  ( F  |` 
{ a } ) )
7876, 77bitri 249 . . . . 5  |-  ( Fun  ( F  |`  D )  <->  Fun  U_ a  e.  D  ( F  |`  { a } ) )
7973, 78sylibr 212 . . . 4  |-  ( A. a  e.  D  Fun  ( F  |`  { a } )  ->  Fun  ( F  |`  D ) )
806, 79anim12i 564 . . 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 195 . 2  |-  ( A. a  e.  D  (
a  e.  dom  F  /\  Fun  ( F  |`  { a } ) )  ->  ( D  C_ 
dom  F  /\  Fun  ( F  |`  D ) ) )
822, 81syl 16 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 367   A.wal 1396    = wceq 1398   E.wex 1617    e. wcel 1823    =/= wne 2649   A.wral 2804    C_ wss 3461   (/)c0 3783   {csn 4016   <.cop 4022   U_ciun 4315   dom cdm 4988    |` cres 4990   Rel wrel 4993   Fun wfun 5564   ` cfv 5570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-res 5000  df-iota 5534  df-fun 5572  df-fv 5578
This theorem is referenced by:  fveqressseq  6003  ovn0ssdmfun  32846
  Copyright terms: Public domain W3C validator