Theorem fwfffunres

Description: If ps is function-like over A , then F matches its behavior over x . (Contributed by BTernaryTau, 28-Sep-2026)

	Ref	Expression
Hypotheses	fwfffunres.1	|- F/ y ps
	fwfffunres.2	|- ( ph -> A. w e. A E. y A. z e. A ( ps -> z = y ) )
	fwfffunres.3	|- F = ( { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } |` x )
Assertion	fwfffunres	|- ( ph -> ( ( z e. A /\ ( w e. A /\ w e. x /\ ps ) ) <-> ( w e. dom F /\ ( F ` w ) = z ) ) )

Proof

Step	Hyp	Ref	Expression
1		fwfffunres.1	|- F/ y ps
2		fwfffunres.2	|- ( ph -> A. w e. A E. y A. z e. A ( ps -> z = y ) )
3		fwfffunres.3	|- F = ( { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } |` x )
4		eqid	|- { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } = { <. w , z >. | ( w e. A /\ z e. A /\ ps ) }
5	1 2 4	fwfffun	|- ( ph -> ( ( w e. A /\ z e. A /\ ps ) <-> ( w e. dom { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } /\ ( { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } ` w ) = z ) ) )
6	5	adantr	|- ( ( ph /\ w e. x ) -> ( ( w e. A /\ z e. A /\ ps ) <-> ( w e. dom { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } /\ ( { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } ` w ) = z ) ) )
7	3	dmeqi	|- dom F = dom ( { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } |` x )
8		dmres	|- dom ( { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } |` x ) = ( x i^i dom { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } )
9	7 8	eqtri	|- dom F = ( x i^i dom { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } )
10	9	elin2	|- ( w e. dom F <-> ( w e. x /\ w e. dom { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } ) )
11	10	baib	|- ( w e. x -> ( w e. dom F <-> w e. dom { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } ) )
12	3	fveq1i	|- ( F ` w ) = ( ( { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } |` x ) ` w )
13		fvres	|- ( w e. x -> ( ( { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } |` x ) ` w ) = ( { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } ` w ) )
14	12 13	eqtrid	|- ( w e. x -> ( F ` w ) = ( { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } ` w ) )
15	14	eqeq1d	|- ( w e. x -> ( ( F ` w ) = z <-> ( { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } ` w ) = z ) )
16	11 15	anbi12d	|- ( w e. x -> ( ( w e. dom F /\ ( F ` w ) = z ) <-> ( w e. dom { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } /\ ( { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } ` w ) = z ) ) )
17	16	adantl	|- ( ( ph /\ w e. x ) -> ( ( w e. dom F /\ ( F ` w ) = z ) <-> ( w e. dom { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } /\ ( { <. w , z >. | ( w e. A /\ z e. A /\ ps ) } ` w ) = z ) ) )
18	6 17	bitr4d	|- ( ( ph /\ w e. x ) -> ( ( w e. A /\ z e. A /\ ps ) <-> ( w e. dom F /\ ( F ` w ) = z ) ) )
19	18	pm5.32da	|- ( ph -> ( ( w e. x /\ ( w e. A /\ z e. A /\ ps ) ) <-> ( w e. x /\ ( w e. dom F /\ ( F ` w ) = z ) ) ) )
20		an4	|- ( ( ( z e. A /\ w e. A ) /\ ( w e. x /\ ps ) ) <-> ( ( z e. A /\ w e. x ) /\ ( w e. A /\ ps ) ) )
21		ancom	|- ( ( z e. A /\ w e. x ) <-> ( w e. x /\ z e. A ) )
22	21	anbi1i	|- ( ( ( z e. A /\ w e. x ) /\ ( w e. A /\ ps ) ) <-> ( ( w e. x /\ z e. A ) /\ ( w e. A /\ ps ) ) )
23		an4	|- ( ( ( w e. x /\ z e. A ) /\ ( w e. A /\ ps ) ) <-> ( ( w e. x /\ w e. A ) /\ ( z e. A /\ ps ) ) )
24	20 22 23	3bitri	|- ( ( ( z e. A /\ w e. A ) /\ ( w e. x /\ ps ) ) <-> ( ( w e. x /\ w e. A ) /\ ( z e. A /\ ps ) ) )
25		13an22anass	|- ( ( z e. A /\ ( w e. A /\ w e. x /\ ps ) ) <-> ( ( z e. A /\ w e. A ) /\ ( w e. x /\ ps ) ) )
26		13an22anass	|- ( ( w e. x /\ ( w e. A /\ z e. A /\ ps ) ) <-> ( ( w e. x /\ w e. A ) /\ ( z e. A /\ ps ) ) )
27	24 25 26	3bitr4i	|- ( ( z e. A /\ ( w e. A /\ w e. x /\ ps ) ) <-> ( w e. x /\ ( w e. A /\ z e. A /\ ps ) ) )
28	10	simplbi	|- ( w e. dom F -> w e. x )
29	28	adantr	|- ( ( w e. dom F /\ ( F ` w ) = z ) -> w e. x )
30	29	pm4.71ri	|- ( ( w e. dom F /\ ( F ` w ) = z ) <-> ( w e. x /\ ( w e. dom F /\ ( F ` w ) = z ) ) )
31	19 27 30	3bitr4g	|- ( ph -> ( ( z e. A /\ ( w e. A /\ w e. x /\ ps ) ) <-> ( w e. dom F /\ ( F ` w ) = z ) ) )