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

Metamath Proof Explorer

Theorem eldm3

Description: Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017)

Ref Expression
Assertion eldm3 
|- ( A e. dom B <-> ( B |` { A } ) =/= (/) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. dom B -> A e. _V )
2 snprc 
 |-  ( -. A e. _V <-> { A } = (/) )
3 reseq2 
 |-  ( { A } = (/) -> ( B |` { A } ) = ( B |` (/) ) )
4 res0 
 |-  ( B |` (/) ) = (/)
5 3 4 eqtrdi 
 |-  ( { A } = (/) -> ( B |` { A } ) = (/) )
6 2 5 sylbi 
 |-  ( -. A e. _V -> ( B |` { A } ) = (/) )
7 6 necon1ai 
 |-  ( ( B |` { A } ) =/= (/) -> A e. _V )
8 eleq1 
 |-  ( x = A -> ( x e. dom B <-> A e. dom B ) )
9 sneq 
 |-  ( x = A -> { x } = { A } )
10 9 reseq2d 
 |-  ( x = A -> ( B |` { x } ) = ( B |` { A } ) )
11 10 neeq1d 
 |-  ( x = A -> ( ( B |` { x } ) =/= (/) <-> ( B |` { A } ) =/= (/) ) )
12 dfclel 
 |-  ( <. x , y >. e. B <-> E. p ( p = <. x , y >. /\ p e. B ) )
13 12 exbii 
 |-  ( E. y <. x , y >. e. B <-> E. y E. p ( p = <. x , y >. /\ p e. B ) )
14 vex 
 |-  x e. _V
15 14 eldm2 
 |-  ( x e. dom B <-> E. y <. x , y >. e. B )
16 n0 
 |-  ( ( B |` { x } ) =/= (/) <-> E. p p e. ( B |` { x } ) )
17 elres 
 |-  ( p e. ( B |` { x } ) <-> E. z e. { x } E. y ( p = <. z , y >. /\ <. z , y >. e. B ) )
18 eleq1 
 |-  ( p = <. z , y >. -> ( p e. B <-> <. z , y >. e. B ) )
19 18 pm5.32i 
 |-  ( ( p = <. z , y >. /\ p e. B ) <-> ( p = <. z , y >. /\ <. z , y >. e. B ) )
20 opeq1 
 |-  ( z = x -> <. z , y >. = <. x , y >. )
21 20 eqeq2d 
 |-  ( z = x -> ( p = <. z , y >. <-> p = <. x , y >. ) )
22 21 anbi1d 
 |-  ( z = x -> ( ( p = <. z , y >. /\ p e. B ) <-> ( p = <. x , y >. /\ p e. B ) ) )
23 19 22 bitr3id 
 |-  ( z = x -> ( ( p = <. z , y >. /\ <. z , y >. e. B ) <-> ( p = <. x , y >. /\ p e. B ) ) )
24 23 exbidv 
 |-  ( z = x -> ( E. y ( p = <. z , y >. /\ <. z , y >. e. B ) <-> E. y ( p = <. x , y >. /\ p e. B ) ) )
25 14 24 rexsn 
 |-  ( E. z e. { x } E. y ( p = <. z , y >. /\ <. z , y >. e. B ) <-> E. y ( p = <. x , y >. /\ p e. B ) )
26 17 25 bitri 
 |-  ( p e. ( B |` { x } ) <-> E. y ( p = <. x , y >. /\ p e. B ) )
27 26 exbii 
 |-  ( E. p p e. ( B |` { x } ) <-> E. p E. y ( p = <. x , y >. /\ p e. B ) )
28 excom 
 |-  ( E. p E. y ( p = <. x , y >. /\ p e. B ) <-> E. y E. p ( p = <. x , y >. /\ p e. B ) )
29 16 27 28 3bitri 
 |-  ( ( B |` { x } ) =/= (/) <-> E. y E. p ( p = <. x , y >. /\ p e. B ) )
30 13 15 29 3bitr4i 
 |-  ( x e. dom B <-> ( B |` { x } ) =/= (/) )
31 8 11 30 vtoclbg 
 |-  ( A e. _V -> ( A e. dom B <-> ( B |` { A } ) =/= (/) ) )
32 1 7 31 pm5.21nii 
 |-  ( A e. dom B <-> ( B |` { A } ) =/= (/) )