Theorem fwfffun

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

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

Proof

Step	Hyp	Ref	Expression
1		fwfffun.1	|- F/ y ps
2		fwfffun.2	|- ( ph -> A. x e. A E. y A. z e. A ( ps -> z = y ) )
3		fwfffun.3	|- F = { <. x , z >. | ( x e. A /\ z e. A /\ ps ) }
4	3	eleq2i	|- ( <. x , z >. e. F <-> <. x , z >. e. { <. x , z >. | ( x e. A /\ z e. A /\ ps ) } )
5		opabidw	|- ( <. x , z >. e. { <. x , z >. | ( x e. A /\ z e. A /\ ps ) } <-> ( x e. A /\ z e. A /\ ps ) )
6	4 5	bitri	|- ( <. x , z >. e. F <-> ( x e. A /\ z e. A /\ ps ) )
7	1	rmo2	|- ( E* z e. A ps <-> E. y A. z e. A ( ps -> z = y ) )
8	7	ralbii	|- ( A. x e. A E* z e. A ps <-> A. x e. A E. y A. z e. A ( ps -> z = y ) )
9	2 8	sylibr	|- ( ph -> A. x e. A E* z e. A ps )
10		funopab	|- ( Fun { <. x , z >. | ( x e. A /\ z e. A /\ ps ) } <-> A. x E* z ( x e. A /\ z e. A /\ ps ) )
11	3	funeqi	|- ( Fun F <-> Fun { <. x , z >. | ( x e. A /\ z e. A /\ ps ) } )
12		2reu5lem2	|- ( A. x e. A E* z e. A ps <-> A. x E* z ( x e. A /\ z e. A /\ ps ) )
13	10 11 12	3bitr4i	|- ( Fun F <-> A. x e. A E* z e. A ps )
14	9 13	sylibr	|- ( ph -> Fun F )
15		df-br	|- ( x F z <-> <. x , z >. e. F )
16		funbrfv2b	|- ( Fun F -> ( x F z <-> ( x e. dom F /\ ( F ` x ) = z ) ) )
17	15 16	bitr3id	|- ( Fun F -> ( <. x , z >. e. F <-> ( x e. dom F /\ ( F ` x ) = z ) ) )
18	14 17	syl	|- ( ph -> ( <. x , z >. e. F <-> ( x e. dom F /\ ( F ` x ) = z ) ) )
19	6 18	bitr3id	|- ( ph -> ( ( x e. A /\ z e. A /\ ps ) <-> ( x e. dom F /\ ( F ` x ) = z ) ) )