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

Metamath Proof Explorer

Theorem cnvresima

Description: An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009)

Ref Expression
Assertion cnvresima 
|- ( `' ( F |` A ) " B ) = ( ( `' F " B ) i^i A )

Proof

Step Hyp Ref Expression
1 19.41v 
 |-  ( E. s ( ( s e. B /\ <. s , t >. e. `' F ) /\ t e. A ) <-> ( E. s ( s e. B /\ <. s , t >. e. `' F ) /\ t e. A ) )
2 vex 
 |-  s e. _V
3 2 opelresi 
 |-  ( <. t , s >. e. ( F |` A ) <-> ( t e. A /\ <. t , s >. e. F ) )
4 vex 
 |-  t e. _V
5 2 4 opelcnv 
 |-  ( <. s , t >. e. `' ( F |` A ) <-> <. t , s >. e. ( F |` A ) )
6 2 4 opelcnv 
 |-  ( <. s , t >. e. `' F <-> <. t , s >. e. F )
7 6 anbi2ci 
 |-  ( ( <. s , t >. e. `' F /\ t e. A ) <-> ( t e. A /\ <. t , s >. e. F ) )
8 3 5 7 3bitr4i 
 |-  ( <. s , t >. e. `' ( F |` A ) <-> ( <. s , t >. e. `' F /\ t e. A ) )
9 8 bianass 
 |-  ( ( s e. B /\ <. s , t >. e. `' ( F |` A ) ) <-> ( ( s e. B /\ <. s , t >. e. `' F ) /\ t e. A ) )
10 9 exbii 
 |-  ( E. s ( s e. B /\ <. s , t >. e. `' ( F |` A ) ) <-> E. s ( ( s e. B /\ <. s , t >. e. `' F ) /\ t e. A ) )
11 4 elima3 
 |-  ( t e. ( `' F " B ) <-> E. s ( s e. B /\ <. s , t >. e. `' F ) )
12 11 anbi1i 
 |-  ( ( t e. ( `' F " B ) /\ t e. A ) <-> ( E. s ( s e. B /\ <. s , t >. e. `' F ) /\ t e. A ) )
13 1 10 12 3bitr4i 
 |-  ( E. s ( s e. B /\ <. s , t >. e. `' ( F |` A ) ) <-> ( t e. ( `' F " B ) /\ t e. A ) )
14 4 elima3 
 |-  ( t e. ( `' ( F |` A ) " B ) <-> E. s ( s e. B /\ <. s , t >. e. `' ( F |` A ) ) )
15 elin 
 |-  ( t e. ( ( `' F " B ) i^i A ) <-> ( t e. ( `' F " B ) /\ t e. A ) )
16 13 14 15 3bitr4i 
 |-  ( t e. ( `' ( F |` A ) " B ) <-> t e. ( ( `' F " B ) i^i A ) )
17 16 eqriv 
 |-  ( `' ( F |` A ) " B ) = ( ( `' F " B ) i^i A )