Theorem fvn0ssdmfun 6350

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 6226. (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.

Step	Hyp	Ref	Expression
1		fvfundmfvn0 6226	. . 3 |- ( ( F ` a ) =/= (/) -> ( a e. dom F /\ Fun ( F |` { a } ) ) )
2	1	ralimi 2952	. 2 |- ( A. a e. D ( F ` a ) =/= (/) -> A. a e. D ( a e. dom F /\ Fun ( F |` { a } ) ) )
3		r19.26 3064	. . 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 2689	. . . . . 6 |- ( a = p -> ( a e. dom F <-> p e. dom F ) )
5	4	rspccv 3306	. . . . 5 |- ( A. a e. D a e. dom F -> ( p e. D -> p e. dom F ) )
6	5	ssrdv 3609	. . . 4 |- ( A. a e. D a e. dom F -> D C_ dom F )
7		funrel 5905	. . . . . . . 8 |- ( Fun ( F |` { a } ) -> Rel ( F |` { a } ) )
8	7	ralimi 2952	. . . . . . 7 |- ( A. a e. D Fun ( F |` { a } ) -> A. a e. D Rel ( F |` { a } ) )
9		reliun 5239	. . . . . . 7 |- ( Rel U_ a e. D ( F |` { a } ) <-> A. a e. D Rel ( F |` { a } ) )
10	8, 9	sylibr 224	. . . . . 6 |- ( A. a e. D Fun ( F |` { a } ) -> Rel U_ a e. D ( F |` { a } ) )
11		sneq 4187	. . . . . . . . . . . . . 14 |- ( a = x -> { a } = { x } )
12	11	reseq2d 5396	. . . . . . . . . . . . 13 |- ( a = x -> ( F |` { a } ) = ( F |` { x } ) )
13	12	funeqd 5910	. . . . . . . . . . . 12 |- ( a = x -> ( Fun ( F |` { a } ) <-> Fun ( F |` { x } ) ) )
14	13	rspcva 3307	. . . . . . . . . . 11 |- ( ( x e. D /\ A. a e. D Fun ( F |` { a } ) ) -> Fun ( F |` { x } ) )
15		dffun5 5901	. . . . . . . . . . . 12 |- ( Fun ( F |` { x } ) <-> ( Rel ( F |` { x } ) /\ A. w E. y A. z ( <. w , z >. e. ( F |` { x } ) -> z = y ) ) )
16		vex 3203	. . . . . . . . . . . . . . . . . . 19 |- x e. _V
17	16	elsnres 5436	. . . . . . . . . . . . . . . . . 18 |- ( <. w , z >. e. ( F |` { x } ) <-> E. a ( <. w , z >. = <. x , a >. /\ <. x , a >. e. F ) )
18	17	imbi1i 339	. . . . . . . . . . . . . . . . 17 |- ( ( <. w , z >. e. ( F |` { x } ) -> z = y ) <-> ( E. a ( <. w , z >. = <. x , a >. /\ <. x , a >. e. F ) -> z = y ) )
19	18	albii 1747	. . . . . . . . . . . . . . . 16 |- ( 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 1774	. . . . . . . . . . . . . . 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 ) )
21	20	albii 1747	. . . . . . . . . . . . . 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 1945	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( a = z <-> z = a )
23		opeq12 4404	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( w = x /\ z = a ) -> <. w , z >. = <. x , a >. )
24	23	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( w = x -> ( z = a -> <. w , z >. = <. x , a >. ) )
25	22, 24	syl5bi 232	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( w = x -> ( a = z -> <. w , z >. = <. x , a >. ) )
26	25	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( w = x /\ <. x , z >. e. F ) -> ( a = z -> <. w , z >. = <. x , a >. ) )
27	26	impcom 446	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( a = z /\ ( w = x /\ <. x , z >. e. F ) ) -> <. w , z >. = <. x , a >. )
28		opeq2 4403	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( z = a -> <. x , z >. = <. x , a >. )
29	28	equcoms 1947	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( a = z -> <. x , z >. = <. x , a >. )
30	29	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( a = z -> ( <. x , z >. e. F <-> <. x , a >. e. F ) )
31	30	biimpcd 239	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( <. x , z >. e. F -> ( a = z -> <. x , a >. e. F ) )
32	31	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( w = x /\ <. x , z >. e. F ) -> ( a = z -> <. x , a >. e. F ) )
33	32	impcom 446	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( a = z /\ ( w = x /\ <. x , z >. e. F ) ) -> <. x , a >. e. F )
34	27, 33	jca 554	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( a = z /\ ( w = x /\ <. x , z >. e. F ) ) -> ( <. w , z >. = <. x , a >. /\ <. x , a >. e. F ) )
35	34	ex 450	. . . . . . . . . . . . . . . . . . . 20 |- ( a = z -> ( ( w = x /\ <. x , z >. e. F ) -> ( <. w , z >. = <. x , a >. /\ <. x , a >. e. F ) ) )
36	35	spimev 2259	. . . . . . . . . . . . . . . . . . 19 |- ( ( w = x /\ <. x , z >. e. F ) -> E. a ( <. w , z >. = <. x , a >. /\ <. x , a >. e. F ) )
37	36	ex 450	. . . . . . . . . . . . . . . . . 18 |- ( w = x -> ( <. x , z >. e. F -> E. a ( <. w , z >. = <. x , a >. /\ <. x , a >. e. F ) ) )
38	37	imim1d 82	. . . . . . . . . . . . . . . . 17 |- ( w = x -> ( ( E. a ( <. w , z >. = <. x , a >. /\ <. x , a >. e. F ) -> z = y ) -> ( <. x , z >. e. F -> z = y ) ) )
39	38	alimdv 1845	. . . . . . . . . . . . . . . 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 ) ) )
40	39	eximdv 1846	. . . . . . . . . . . . . . 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 ) ) )
41	40	spimvw 1927	. . . . . . . . . . . . . 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 ) )
42	21, 41	sylbi 207	. . . . . . . . . . . . 13 |- ( A. w E. y A. z ( <. w , z >. e. ( F |` { x } ) -> z = y ) -> E. y A. z ( <. x , z >. e. F -> z = y ) )
43	42	adantl 482	. . . . . . . . . . . 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 ) )
44	15, 43	sylbi 207	. . . . . . . . . . 11 |- ( Fun ( F |` { x } ) -> E. y A. z ( <. x , z >. e. F -> z = y ) )
45	14, 44	syl 17	. . . . . . . . . 10 |- ( ( x e. D /\ A. a e. D Fun ( F |` { a } ) ) -> E. y A. z ( <. x , z >. e. F -> z = y ) )
46	45	expcom 451	. . . . . . . . 9 |- ( A. a e. D Fun ( F |` { a } ) -> ( x e. D -> E. y A. z ( <. x , z >. e. F -> z = y ) ) )
47		ancomst 468	. . . . . . . . . . . . 13 |- ( ( ( <. x , z >. e. F /\ x e. D ) -> z = y ) <-> ( ( x e. D /\ <. x , z >. e. F ) -> z = y ) )
48		impexp 462	. . . . . . . . . . . . 13 |- ( ( ( x e. D /\ <. x , z >. e. F ) -> z = y ) <-> ( x e. D -> ( <. x , z >. e. F -> z = y ) ) )
49	47, 48	bitri 264	. . . . . . . . . . . 12 |- ( ( ( <. x , z >. e. F /\ x e. D ) -> z = y ) <-> ( x e. D -> ( <. x , z >. e. F -> z = y ) ) )
50	49	albii 1747	. . . . . . . . . . 11 |- ( A. z ( ( <. x , z >. e. F /\ x e. D ) -> z = y ) <-> A. z ( x e. D -> ( <. x , z >. e. F -> z = y ) ) )
51	50	exbii 1774	. . . . . . . . . 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 1868	. . . . . . . . . . 11 |- ( A. z ( x e. D -> ( <. x , z >. e. F -> z = y ) ) <-> ( x e. D -> A. z ( <. x , z >. e. F -> z = y ) ) )
53	52	exbii 1774	. . . . . . . . . 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 1910	. . . . . . . . . 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 ) ) )
55	51, 53, 54	3bitri 286	. . . . . . . . 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 ) ) )
56	46, 55	sylibr 224	. . . . . . . 8 |- ( A. a e. D Fun ( F |` { a } ) -> E. y A. z ( ( <. x , z >. e. F /\ x e. D ) -> z = y ) )
57	56	alrimiv 1855	. . . . . . 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 5418	. . . . . . . . . . . . . 14 |- ( F |` U_ a e. D { a } ) = U_ a e. D ( F |` { a } )
59	58	eqcomi 2631	. . . . . . . . . . . . 13 |- U_ a e. D ( F |` { a } ) = ( F |` U_ a e. D { a } )
60	59	eleq2i 2693	. . . . . . . . . . . 12 |- ( <. x , z >. e. U_ a e. D ( F |` { a } ) <-> <. x , z >. e. ( F |` U_ a e. D { a } ) )
61		iunid 4575	. . . . . . . . . . . . . 14 |- U_ a e. D { a } = D
62	61	reseq2i 5393	. . . . . . . . . . . . 13 |- ( F |` U_ a e. D { a } ) = ( F |` D )
63	62	eleq2i 2693	. . . . . . . . . . . 12 |- ( <. x , z >. e. ( F |` U_ a e. D { a } ) <-> <. x , z >. e. ( F |` D ) )
64		vex 3203	. . . . . . . . . . . . 13 |- z e. _V
65	64	opelres 5401	. . . . . . . . . . . 12 |- ( <. x , z >. e. ( F |` D ) <-> ( <. x , z >. e. F /\ x e. D ) )
66	60, 63, 65	3bitri 286	. . . . . . . . . . 11 |- ( <. x , z >. e. U_ a e. D ( F |` { a } ) <-> ( <. x , z >. e. F /\ x e. D ) )
67	66	imbi1i 339	. . . . . . . . . 10 |- ( ( <. x , z >. e. U_ a e. D ( F |` { a } ) -> z = y ) <-> ( ( <. x , z >. e. F /\ x e. D ) -> z = y ) )
68	67	albii 1747	. . . . . . . . 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 ) )
69	68	exbii 1774	. . . . . . . 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 ) )
70	69	albii 1747	. . . . . . 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 ) )
71	57, 70	sylibr 224	. . . . . 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 5901	. . . . . 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 ) ) )
73	10, 71, 72	sylanbrc 698	. . . . 5 |- ( A. a e. D Fun ( F |` { a } ) -> Fun U_ a e. D ( F |` { a } ) )
74	61	eqcomi 2631	. . . . . . . 8 |- D = U_ a e. D { a }
75	74	reseq2i 5393	. . . . . . 7 |- ( F |` D ) = ( F |` U_ a e. D { a } )
76	75	funeqi 5909	. . . . . 6 |- ( Fun ( F |` D ) <-> Fun ( F |` U_ a e. D { a } ) )
77	58	funeqi 5909	. . . . . 6 |- ( Fun ( F |` U_ a e. D { a } ) <-> Fun U_ a e. D ( F |` { a } ) )
78	76, 77	bitri 264	. . . . 5 |- ( Fun ( F |` D ) <-> Fun U_ a e. D ( F |` { a } ) )
79	73, 78	sylibr 224	. . . 4 |- ( A. a e. D Fun ( F |` { a } ) -> Fun ( F |` D ) )
80	6, 79	anim12i 590	. . 3 |- ( ( A. a e. D a e. dom F /\ A. a e. D Fun ( F |` { a } ) ) -> ( D C_ dom F /\ Fun ( F |` D ) ) )
81	3, 80	sylbi 207	. 2 |- ( A. a e. D ( a e. dom F /\ Fun ( F |` { a } ) ) -> ( D C_ dom F /\ Fun ( F |` D ) ) )
82	2, 81	syl 17	1 |- ( A. a e. D ( F ` a ) =/= (/) -> ( D C_ dom F /\ Fun ( F |` D ) ) )

Syntax hints:   -> wi 4   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   C_ wss 3574   (/)c0 3915   {csn 4177   <.cop 4183   U_ciun 4520   dom cdm 5114   |` cres 5116   Rel wrel 5119   Fun wfun 5882   ` cfv 5888

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-8 1992  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-pow 4843  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-sbc 3436  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-uni 4437  df-iun 4522  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-res 5126  df-iota 5851  df-fun 5890  df-fv 5896

This theorem is referenced by:  fveqressseq  6355  ovn0ssdmfun  41767