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

Metamath Proof Explorer

Theorem 2elresin

Description: Membership in two functions restricted by each other's domain. (Contributed by NM, 8-Aug-1994)

Ref Expression
Assertion 2elresin 
|- ( ( F Fn A /\ G Fn B ) -> ( ( <. x , y >. e. F /\ <. x , z >. e. G ) <-> ( <. x , y >. e. ( F |` ( A i^i B ) ) /\ <. x , z >. e. ( G |` ( A i^i B ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fnop 
 |-  ( ( F Fn A /\ <. x , y >. e. F ) -> x e. A )
2 fnop 
 |-  ( ( G Fn B /\ <. x , z >. e. G ) -> x e. B )
3 1 2 anim12i 
 |-  ( ( ( F Fn A /\ <. x , y >. e. F ) /\ ( G Fn B /\ <. x , z >. e. G ) ) -> ( x e. A /\ x e. B ) )
4 3 an4s 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( <. x , y >. e. F /\ <. x , z >. e. G ) ) -> ( x e. A /\ x e. B ) )
5 elin 
 |-  ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
6 4 5 sylibr 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( <. x , y >. e. F /\ <. x , z >. e. G ) ) -> x e. ( A i^i B ) )
7 vex 
 |-  y e. _V
8 7 opres 
 |-  ( x e. ( A i^i B ) -> ( <. x , y >. e. ( F |` ( A i^i B ) ) <-> <. x , y >. e. F ) )
9 vex 
 |-  z e. _V
10 9 opres 
 |-  ( x e. ( A i^i B ) -> ( <. x , z >. e. ( G |` ( A i^i B ) ) <-> <. x , z >. e. G ) )
11 8 10 anbi12d 
 |-  ( x e. ( A i^i B ) -> ( ( <. x , y >. e. ( F |` ( A i^i B ) ) /\ <. x , z >. e. ( G |` ( A i^i B ) ) ) <-> ( <. x , y >. e. F /\ <. x , z >. e. G ) ) )
12 11 biimprd 
 |-  ( x e. ( A i^i B ) -> ( ( <. x , y >. e. F /\ <. x , z >. e. G ) -> ( <. x , y >. e. ( F |` ( A i^i B ) ) /\ <. x , z >. e. ( G |` ( A i^i B ) ) ) ) )
13 6 12 syl 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( <. x , y >. e. F /\ <. x , z >. e. G ) ) -> ( ( <. x , y >. e. F /\ <. x , z >. e. G ) -> ( <. x , y >. e. ( F |` ( A i^i B ) ) /\ <. x , z >. e. ( G |` ( A i^i B ) ) ) ) )
14 13 ex 
 |-  ( ( F Fn A /\ G Fn B ) -> ( ( <. x , y >. e. F /\ <. x , z >. e. G ) -> ( ( <. x , y >. e. F /\ <. x , z >. e. G ) -> ( <. x , y >. e. ( F |` ( A i^i B ) ) /\ <. x , z >. e. ( G |` ( A i^i B ) ) ) ) ) )
15 14 pm2.43d 
 |-  ( ( F Fn A /\ G Fn B ) -> ( ( <. x , y >. e. F /\ <. x , z >. e. G ) -> ( <. x , y >. e. ( F |` ( A i^i B ) ) /\ <. x , z >. e. ( G |` ( A i^i B ) ) ) ) )
16 resss 
 |-  ( F |` ( A i^i B ) ) C_ F
17 16 sseli 
 |-  ( <. x , y >. e. ( F |` ( A i^i B ) ) -> <. x , y >. e. F )
18 resss 
 |-  ( G |` ( A i^i B ) ) C_ G
19 18 sseli 
 |-  ( <. x , z >. e. ( G |` ( A i^i B ) ) -> <. x , z >. e. G )
20 17 19 anim12i 
 |-  ( ( <. x , y >. e. ( F |` ( A i^i B ) ) /\ <. x , z >. e. ( G |` ( A i^i B ) ) ) -> ( <. x , y >. e. F /\ <. x , z >. e. G ) )
21 15 20 impbid1 
 |-  ( ( F Fn A /\ G Fn B ) -> ( ( <. x , y >. e. F /\ <. x , z >. e. G ) <-> ( <. x , y >. e. ( F |` ( A i^i B ) ) /\ <. x , z >. e. ( G |` ( A i^i B ) ) ) ) )