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

Metamath Proof Explorer

Theorem elreldm

Description: The first member of an ordered pair in a relation belongs to the domain of the relation (see op1stb ). (Contributed by NM, 28-Jul-2004)

Ref Expression
Assertion elreldm 
|- ( ( Rel A /\ B e. A ) -> |^| |^| B e. dom A )

Proof

Step Hyp Ref Expression
1 df-rel 
 |-  ( Rel A <-> A C_ ( _V X. _V ) )
2 ssel 
 |-  ( A C_ ( _V X. _V ) -> ( B e. A -> B e. ( _V X. _V ) ) )
3 1 2 sylbi 
 |-  ( Rel A -> ( B e. A -> B e. ( _V X. _V ) ) )
4 elvv 
 |-  ( B e. ( _V X. _V ) <-> E. x E. y B = <. x , y >. )
5 3 4 imbitrdi 
 |-  ( Rel A -> ( B e. A -> E. x E. y B = <. x , y >. ) )
6 eleq1 
 |-  ( B = <. x , y >. -> ( B e. A <-> <. x , y >. e. A ) )
7 vex 
 |-  x e. _V
8 vex 
 |-  y e. _V
9 7 8 opeldm 
 |-  ( <. x , y >. e. A -> x e. dom A )
10 6 9 biimtrdi 
 |-  ( B = <. x , y >. -> ( B e. A -> x e. dom A ) )
11 inteq 
 |-  ( B = <. x , y >. -> |^| B = |^| <. x , y >. )
12 11 inteqd 
 |-  ( B = <. x , y >. -> |^| |^| B = |^| |^| <. x , y >. )
13 7 8 op1stb 
 |-  |^| |^| <. x , y >. = x
14 12 13 eqtrdi 
 |-  ( B = <. x , y >. -> |^| |^| B = x )
15 14 eleq1d 
 |-  ( B = <. x , y >. -> ( |^| |^| B e. dom A <-> x e. dom A ) )
16 10 15 sylibrd 
 |-  ( B = <. x , y >. -> ( B e. A -> |^| |^| B e. dom A ) )
17 16 exlimivv 
 |-  ( E. x E. y B = <. x , y >. -> ( B e. A -> |^| |^| B e. dom A ) )
18 5 17 syli 
 |-  ( Rel A -> ( B e. A -> |^| |^| B e. dom A ) )
19 18 imp 
 |-  ( ( Rel A /\ B e. A ) -> |^| |^| B e. dom A )