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

Metamath Proof Explorer

Theorem releldm2

Description: Two ways of expressing membership in the domain of a relation. (Contributed by NM, 22-Sep-2013)

Ref Expression
Assertion releldm2 
|- ( Rel A -> ( B e. dom A <-> E. x e. A ( 1st ` x ) = B ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( B e. dom A -> B e. _V )
2 1 anim2i 
 |-  ( ( Rel A /\ B e. dom A ) -> ( Rel A /\ B e. _V ) )
3 id 
 |-  ( ( 1st ` x ) = B -> ( 1st ` x ) = B )
4 fvex 
 |-  ( 1st ` x ) e. _V
5 3 4 eqeltrrdi 
 |-  ( ( 1st ` x ) = B -> B e. _V )
6 5 rexlimivw 
 |-  ( E. x e. A ( 1st ` x ) = B -> B e. _V )
7 6 anim2i 
 |-  ( ( Rel A /\ E. x e. A ( 1st ` x ) = B ) -> ( Rel A /\ B e. _V ) )
8 eldm2g 
 |-  ( B e. _V -> ( B e. dom A <-> E. y <. B , y >. e. A ) )
9 8 adantl 
 |-  ( ( Rel A /\ B e. _V ) -> ( B e. dom A <-> E. y <. B , y >. e. A ) )
10 df-rel 
 |-  ( Rel A <-> A C_ ( _V X. _V ) )
11 ssel 
 |-  ( A C_ ( _V X. _V ) -> ( x e. A -> x e. ( _V X. _V ) ) )
12 10 11 sylbi 
 |-  ( Rel A -> ( x e. A -> x e. ( _V X. _V ) ) )
13 12 imp 
 |-  ( ( Rel A /\ x e. A ) -> x e. ( _V X. _V ) )
14 op1steq 
 |-  ( x e. ( _V X. _V ) -> ( ( 1st ` x ) = B <-> E. y x = <. B , y >. ) )
15 13 14 syl 
 |-  ( ( Rel A /\ x e. A ) -> ( ( 1st ` x ) = B <-> E. y x = <. B , y >. ) )
16 15 rexbidva 
 |-  ( Rel A -> ( E. x e. A ( 1st ` x ) = B <-> E. x e. A E. y x = <. B , y >. ) )
17 16 adantr 
 |-  ( ( Rel A /\ B e. _V ) -> ( E. x e. A ( 1st ` x ) = B <-> E. x e. A E. y x = <. B , y >. ) )
18 rexcom4 
 |-  ( E. x e. A E. y x = <. B , y >. <-> E. y E. x e. A x = <. B , y >. )
19 risset 
 |-  ( <. B , y >. e. A <-> E. x e. A x = <. B , y >. )
20 19 exbii 
 |-  ( E. y <. B , y >. e. A <-> E. y E. x e. A x = <. B , y >. )
21 18 20 bitr4i 
 |-  ( E. x e. A E. y x = <. B , y >. <-> E. y <. B , y >. e. A )
22 17 21 bitrdi 
 |-  ( ( Rel A /\ B e. _V ) -> ( E. x e. A ( 1st ` x ) = B <-> E. y <. B , y >. e. A ) )
23 9 22 bitr4d 
 |-  ( ( Rel A /\ B e. _V ) -> ( B e. dom A <-> E. x e. A ( 1st ` x ) = B ) )
24 2 7 23 pm5.21nd 
 |-  ( Rel A -> ( B e. dom A <-> E. x e. A ( 1st ` x ) = B ) )