Metamath Proof Explorer

Theorem fvn0ssdmfun

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 . (Contributed by AV, 27-Jan-2020) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion fvn0ssdmfun 
|- ( A. a e. D ( F ` a ) =/= (/) -> ( D C_ dom F /\ Fun ( F |` D ) ) )

Proof

Step Hyp Ref Expression
1 fvfundmfvn0 
 |-  ( ( F ` a ) =/= (/) -> ( a e. dom F /\ Fun ( F |` { a } ) ) )
2 1 ralimi 
 |-  ( A. a e. D ( F ` a ) =/= (/) -> A. a e. D ( a e. dom F /\ Fun ( F |` { a } ) ) )
3 r19.26 
 |-  ( 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 eleq1w 
 |-  ( a = p -> ( a e. dom F <-> p e. dom F ) )
5 4 rspccv 
 |-  ( A. a e. D a e. dom F -> ( p e. D -> p e. dom F ) )
6 5 ssrdv 
 |-  ( A. a e. D a e. dom F -> D C_ dom F )
7 funrel 
 |-  ( Fun ( F |` { a } ) -> Rel ( F |` { a } ) )
8 7 ralimi 
 |-  ( A. a e. D Fun ( F |` { a } ) -> A. a e. D Rel ( F |` { a } ) )
9 reliun 
 |-  ( Rel U_ a e. D ( F |` { a } ) <-> A. a e. D Rel ( F |` { a } ) )
10 8 9 sylibr 
 |-  ( A. a e. D Fun ( F |` { a } ) -> Rel U_ a e. D ( F |` { a } ) )
11 sneq 
 |-  ( a = x -> { a } = { x } )
12 11 reseq2d 
 |-  ( a = x -> ( F |` { a } ) = ( F |` { x } ) )
13 12 funeqd 
 |-  ( a = x -> ( Fun ( F |` { a } ) <-> Fun ( F |` { x } ) ) )
14 13 rspcva 
 |-  ( ( x e. D /\ A. a e. D Fun ( F |` { a } ) ) -> Fun ( F |` { x } ) )
15 dffun5 
 |-  ( Fun ( F |` { x } ) <-> ( Rel ( F |` { x } ) /\ A. w E. y A. z ( <. w , z >. e. ( F |` { x } ) -> z = y ) ) )
16 vex 
 |-  x e. _V
17 16 elsnres 
 |-  ( <. w , z >. e. ( F |` { x } ) <-> E. a ( <. w , z >. = <. x , a >. /\ <. x , a >. e. F ) )
18 17 imbi1i 
 |-  ( ( <. w , z >. e. ( F |` { x } ) -> z = y ) <-> ( E. a ( <. w , z >. = <. x , a >. /\ <. x , a >. e. F ) -> z = y ) )
19 18 albii 
 |-  ( A. z ( <. w , z >. e. ( F |` { x } ) -> z = y ) <-> A. z ( E. a ( <. w , z >. = <. x , a >. /\ <. x , a >. e. F ) -> z = y ) )
20 19 exbii 
 |-  ( 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 ) )
21 20 albii 
 |-  ( 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 
 |-  ( a = z <-> z = a )
23 opeq12 
 |-  ( ( w = x /\ z = a ) -> <. w , z >. = <. x , a >. )
24 23 ex 
 |-  ( w = x -> ( z = a -> <. w , z >. = <. x , a >. ) )
25 22 24 biimtrid 
 |-  ( w = x -> ( a = z -> <. w , z >. = <. x , a >. ) )
26 25 adantr 
 |-  ( ( w = x /\ <. x , z >. e. F ) -> ( a = z -> <. w , z >. = <. x , a >. ) )
27 26 impcom 
 |-  ( ( a = z /\ ( w = x /\ <. x , z >. e. F ) ) -> <. w , z >. = <. x , a >. )
28 opeq2 
 |-  ( z = a -> <. x , z >. = <. x , a >. )
29 28 equcoms 
 |-  ( a = z -> <. x , z >. = <. x , a >. )
30 29 eleq1d 
 |-  ( a = z -> ( <. x , z >. e. F <-> <. x , a >. e. F ) )
31 30 biimpcd 
 |-  ( <. x , z >. e. F -> ( a = z -> <. x , a >. e. F ) )
32 31 adantl 
 |-  ( ( w = x /\ <. x , z >. e. F ) -> ( a = z -> <. x , a >. e. F ) )
33 32 impcom 
 |-  ( ( a = z /\ ( w = x /\ <. x , z >. e. F ) ) -> <. x , a >. e. F )
34 27 33 jca 
 |-  ( ( a = z /\ ( w = x /\ <. x , z >. e. F ) ) -> ( <. w , z >. = <. x , a >. /\ <. x , a >. e. F ) )
35 34 ex 
 |-  ( a = z -> ( ( w = x /\ <. x , z >. e. F ) -> ( <. w , z >. = <. x , a >. /\ <. x , a >. e. F ) ) )
36 35 spimevw 
 |-  ( ( w = x /\ <. x , z >. e. F ) -> E. a ( <. w , z >. = <. x , a >. /\ <. x , a >. e. F ) )
37 36 ex 
 |-  ( w = x -> ( <. x , z >. e. F -> E. a ( <. w , z >. = <. x , a >. /\ <. x , a >. e. F ) ) )
38 37 imim1d 
 |-  ( w = x -> ( ( E. a ( <. w , z >. = <. x , a >. /\ <. x , a >. e. F ) -> z = y ) -> ( <. x , z >. e. F -> z = y ) ) )
39 38 alimdv 
 |-  ( w = x -> ( A. z ( E. a ( <. w , z >. = <. x , a >. /\ <. x , a >. e. F ) -> z = y ) -> A. z ( <. x , z >. e. F -> z = y ) ) )
40 39 eximdv 
 |-  ( 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 ) ) )
41 40 spimvw 
 |-  ( 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 ) )
42 21 41 sylbi 
 |-  ( A. w E. y A. z ( <. w , z >. e. ( F |` { x } ) -> z = y ) -> E. y A. z ( <. x , z >. e. F -> z = y ) )
43 15 42 simplbiim 
 |-  ( Fun ( F |` { x } ) -> E. y A. z ( <. x , z >. e. F -> z = y ) )
44 14 43 syl 
 |-  ( ( x e. D /\ A. a e. D Fun ( F |` { a } ) ) -> E. y A. z ( <. x , z >. e. F -> z = y ) )
45 44 expcom 
 |-  ( A. a e. D Fun ( F |` { a } ) -> ( x e. D -> E. y A. z ( <. x , z >. e. F -> z = y ) ) )
46 impexp 
 |-  ( ( ( x e. D /\ <. x , z >. e. F ) -> z = y ) <-> ( x e. D -> ( <. x , z >. e. F -> z = y ) ) )
47 46 albii 
 |-  ( A. z ( ( x e. D /\ <. x , z >. e. F ) -> z = y ) <-> A. z ( x e. D -> ( <. x , z >. e. F -> z = y ) ) )
48 47 exbii 
 |-  ( E. y A. z ( ( x e. D /\ <. x , z >. e. F ) -> z = y ) <-> E. y A. z ( x e. D -> ( <. x , z >. e. F -> z = y ) ) )
49 19.21v 
 |-  ( A. z ( x e. D -> ( <. x , z >. e. F -> z = y ) ) <-> ( x e. D -> A. z ( <. x , z >. e. F -> z = y ) ) )
50 49 exbii 
 |-  ( 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 ) ) )
51 19.37v 
 |-  ( 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 ) ) )
52 48 50 51 3bitri 
 |-  ( E. y A. z ( ( x e. D /\ <. x , z >. e. F ) -> z = y ) <-> ( x e. D -> E. y A. z ( <. x , z >. e. F -> z = y ) ) )
53 45 52 sylibr 
 |-  ( A. a e. D Fun ( F |` { a } ) -> E. y A. z ( ( x e. D /\ <. x , z >. e. F ) -> z = y ) )
54 53 alrimiv 
 |-  ( A. a e. D Fun ( F |` { a } ) -> A. x E. y A. z ( ( x e. D /\ <. x , z >. e. F ) -> z = y ) )
55 resiun2 
 |-  ( F |` U_ a e. D { a } ) = U_ a e. D ( F |` { a } )
56 55 eqcomi 
 |-  U_ a e. D ( F |` { a } ) = ( F |` U_ a e. D { a } )
57 56 eleq2i 
 |-  ( <. x , z >. e. U_ a e. D ( F |` { a } ) <-> <. x , z >. e. ( F |` U_ a e. D { a } ) )
58 iunid 
 |-  U_ a e. D { a } = D
59 58 reseq2i 
 |-  ( F |` U_ a e. D { a } ) = ( F |` D )
60 59 eleq2i 
 |-  ( <. x , z >. e. ( F |` U_ a e. D { a } ) <-> <. x , z >. e. ( F |` D ) )
61 vex 
 |-  z e. _V
62 61 opelresi 
 |-  ( <. x , z >. e. ( F |` D ) <-> ( x e. D /\ <. x , z >. e. F ) )
63 57 60 62 3bitri 
 |-  ( <. x , z >. e. U_ a e. D ( F |` { a } ) <-> ( x e. D /\ <. x , z >. e. F ) )
64 63 imbi1i 
 |-  ( ( <. x , z >. e. U_ a e. D ( F |` { a } ) -> z = y ) <-> ( ( x e. D /\ <. x , z >. e. F ) -> z = y ) )
65 64 albii 
 |-  ( A. z ( <. x , z >. e. U_ a e. D ( F |` { a } ) -> z = y ) <-> A. z ( ( x e. D /\ <. x , z >. e. F ) -> z = y ) )
66 65 exbii 
 |-  ( E. y A. z ( <. x , z >. e. U_ a e. D ( F |` { a } ) -> z = y ) <-> E. y A. z ( ( x e. D /\ <. x , z >. e. F ) -> z = y ) )
67 66 albii 
 |-  ( A. x E. y A. z ( <. x , z >. e. U_ a e. D ( F |` { a } ) -> z = y ) <-> A. x E. y A. z ( ( x e. D /\ <. x , z >. e. F ) -> z = y ) )
68 54 67 sylibr 
 |-  ( A. a e. D Fun ( F |` { a } ) -> A. x E. y A. z ( <. x , z >. e. U_ a e. D ( F |` { a } ) -> z = y ) )
69 dffun5 
 |-  ( 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 ) ) )
70 10 68 69 sylanbrc 
 |-  ( A. a e. D Fun ( F |` { a } ) -> Fun U_ a e. D ( F |` { a } ) )
71 58 eqcomi 
 |-  D = U_ a e. D { a }
72 71 reseq2i 
 |-  ( F |` D ) = ( F |` U_ a e. D { a } )
73 72 funeqi 
 |-  ( Fun ( F |` D ) <-> Fun ( F |` U_ a e. D { a } ) )
74 55 funeqi 
 |-  ( Fun ( F |` U_ a e. D { a } ) <-> Fun U_ a e. D ( F |` { a } ) )
75 73 74 bitri 
 |-  ( Fun ( F |` D ) <-> Fun U_ a e. D ( F |` { a } ) )
76 70 75 sylibr 
 |-  ( A. a e. D Fun ( F |` { a } ) -> Fun ( F |` D ) )
77 6 76 anim12i 
 |-  ( ( A. a e. D a e. dom F /\ A. a e. D Fun ( F |` { a } ) ) -> ( D C_ dom F /\ Fun ( F |` D ) ) )
78 3 77 sylbi 
 |-  ( A. a e. D ( a e. dom F /\ Fun ( F |` { a } ) ) -> ( D C_ dom F /\ Fun ( F |` D ) ) )
79 2 78 syl 
 |-  ( A. a e. D ( F ` a ) =/= (/) -> ( D C_ dom F /\ Fun ( F |` D ) ) )