Theorem tz6.12i

Description: Corollary of Theorem 6.12(2) of TakeutiZaring p. 27. (Contributed by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Assertion	tz6.12i	|- ( B =/= (/) -> ( ( F ` A ) = B -> A F B ) )

Proof

Step	Hyp	Ref	Expression
1		fvex	|- ( F ` A ) e. _V
2		neeq1	|- ( ( F ` A ) = y -> ( ( F ` A ) =/= (/) <-> y =/= (/) ) )
3		tz6.12-2	|- ( -. E! y A F y -> ( F ` A ) = (/) )
4	3	necon1ai	|- ( ( F ` A ) =/= (/) -> E! y A F y )
5		tz6.12c	|- ( E! y A F y -> ( ( F ` A ) = y <-> A F y ) )
6	4 5	syl	|- ( ( F ` A ) =/= (/) -> ( ( F ` A ) = y <-> A F y ) )
7	6	biimpcd	|- ( ( F ` A ) = y -> ( ( F ` A ) =/= (/) -> A F y ) )
8	2 7	sylbird	|- ( ( F ` A ) = y -> ( y =/= (/) -> A F y ) )
9	8	eqcoms	|- ( y = ( F ` A ) -> ( y =/= (/) -> A F y ) )
10		neeq1	|- ( y = ( F ` A ) -> ( y =/= (/) <-> ( F ` A ) =/= (/) ) )
11		breq2	|- ( y = ( F ` A ) -> ( A F y <-> A F ( F ` A ) ) )
12	9 10 11	3imtr3d	|- ( y = ( F ` A ) -> ( ( F ` A ) =/= (/) -> A F ( F ` A ) ) )
13	1 12	vtocle	|- ( ( F ` A ) =/= (/) -> A F ( F ` A ) )
14	13	a1i	|- ( ( F ` A ) = B -> ( ( F ` A ) =/= (/) -> A F ( F ` A ) ) )
15		neeq1	|- ( ( F ` A ) = B -> ( ( F ` A ) =/= (/) <-> B =/= (/) ) )
16		breq2	|- ( ( F ` A ) = B -> ( A F ( F ` A ) <-> A F B ) )
17	14 15 16	3imtr3d	|- ( ( F ` A ) = B -> ( B =/= (/) -> A F B ) )
18	17	com12	|- ( B =/= (/) -> ( ( F ` A ) = B -> A F B ) )