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

Metamath Proof Explorer

Theorem setlikespec

Description: If R is set-like in A , then all predecessor classes of elements of A exist. (Contributed by Scott Fenton, 20-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion setlikespec 
|- ( ( X e. A /\ R Se A ) -> Pred ( R , A , X ) e. _V )

Proof

Step Hyp Ref Expression
1 df-rab 
 |-  { x e. A | x R X } = { x | ( x e. A /\ x R X ) }
2 vex 
 |-  x e. _V
3 2 elpred 
 |-  ( X e. A -> ( x e. Pred ( R , A , X ) <-> ( x e. A /\ x R X ) ) )
4 3 eqabdv 
 |-  ( X e. A -> Pred ( R , A , X ) = { x | ( x e. A /\ x R X ) } )
5 1 4 eqtr4id 
 |-  ( X e. A -> { x e. A | x R X } = Pred ( R , A , X ) )
6 5 adantr 
 |-  ( ( X e. A /\ R Se A ) -> { x e. A | x R X } = Pred ( R , A , X ) )
7 seex 
 |-  ( ( R Se A /\ X e. A ) -> { x e. A | x R X } e. _V )
8 7 ancoms 
 |-  ( ( X e. A /\ R Se A ) -> { x e. A | x R X } e. _V )
9 6 8 eqeltrrd 
 |-  ( ( X e. A /\ R Se A ) -> Pred ( R , A , X ) e. _V )