Theorem tz6.12i-afv2

Description: Corollary of Theorem 6.12(2) of TakeutiZaring p. 27. analogous to tz6.12i . (Contributed by AV, 5-Sep-2022)

	Ref	Expression
Assertion	tz6.12i-afv2	|- ( B e. ran F -> ( ( F '''' A ) = B -> A F B ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	|- ( ( F '''' A ) = y -> ( ( F '''' A ) e. ran F <-> y e. ran F ) )
2		dfatafv2rnb	|- ( F defAt A <-> ( F '''' A ) e. ran F )
3		dfdfat2	|- ( F defAt A <-> ( A e. dom F /\ E! y A F y ) )
4	3	simprbi	|- ( F defAt A -> E! y A F y )
5	2 4	sylbir	|- ( ( F '''' A ) e. ran F -> E! y A F y )
6		tz6.12c-afv2	|- ( E! y A F y -> ( ( F '''' A ) = y <-> A F y ) )
7	5 6	syl	|- ( ( F '''' A ) e. ran F -> ( ( F '''' A ) = y <-> A F y ) )
8	7	biimpcd	|- ( ( F '''' A ) = y -> ( ( F '''' A ) e. ran F -> A F y ) )
9	1 8	sylbird	|- ( ( F '''' A ) = y -> ( y e. ran F -> A F y ) )
10	9	eqcoms	|- ( y = ( F '''' A ) -> ( y e. ran F -> A F y ) )
11		eleq1	|- ( y = ( F '''' A ) -> ( y e. ran F <-> ( F '''' A ) e. ran F ) )
12		breq2	|- ( y = ( F '''' A ) -> ( A F y <-> A F ( F '''' A ) ) )
13	10 11 12	3imtr3d	|- ( y = ( F '''' A ) -> ( ( F '''' A ) e. ran F -> A F ( F '''' A ) ) )
14	13	vtocleg	|- ( ( F '''' A ) e. ran F -> ( ( F '''' A ) e. ran F -> A F ( F '''' A ) ) )
15	14	pm2.43i	|- ( ( F '''' A ) e. ran F -> A F ( F '''' A ) )
16	15	a1i	|- ( ( F '''' A ) = B -> ( ( F '''' A ) e. ran F -> A F ( F '''' A ) ) )
17		eleq1	|- ( ( F '''' A ) = B -> ( ( F '''' A ) e. ran F <-> B e. ran F ) )
18		breq2	|- ( ( F '''' A ) = B -> ( A F ( F '''' A ) <-> A F B ) )
19	16 17 18	3imtr3d	|- ( ( F '''' A ) = B -> ( B e. ran F -> A F B ) )
20	19	com12	|- ( B e. ran F -> ( ( F '''' A ) = B -> A F B ) )