This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )