Metamath Proof Explorer

Theorem trpredpred

Description: Assuming it exists, the predecessor class is a subset of the transitive predecessors. (Contributed by Scott Fenton, 18-Feb-2011)

Ref Expression
Assertion trpredpred 
|- ( Pred ( R , A , X ) e. B -> Pred ( R , A , X ) C_ TrPred ( R , A , X ) )

Proof

Step Hyp Ref Expression
1 fr0g 
 |-  ( Pred ( R , A , X ) e. B -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` (/) ) = Pred ( R , A , X ) )
2 frfnom 
 |-  ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) Fn _om
3 peano1 
 |-  (/) e. _om
4 fnbrfvb 
 |-  ( ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) Fn _om /\ (/) e. _om ) -> ( ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` (/) ) = Pred ( R , A , X ) <-> (/) ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) Pred ( R , A , X ) ) )
5 2 3 4 mp2an 
 |-  ( ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` (/) ) = Pred ( R , A , X ) <-> (/) ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) Pred ( R , A , X ) )
6 1 5 sylib 
 |-  ( Pred ( R , A , X ) e. B -> (/) ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) Pred ( R , A , X ) )
7 0ex 
 |-  (/) e. _V
8 breq1 
 |-  ( z = (/) -> ( z ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) Pred ( R , A , X ) <-> (/) ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) Pred ( R , A , X ) ) )
9 7 8 spcev 
 |-  ( (/) ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) Pred ( R , A , X ) -> E. z z ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) Pred ( R , A , X ) )
10 6 9 syl 
 |-  ( Pred ( R , A , X ) e. B -> E. z z ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) Pred ( R , A , X ) )
11 elrng 
 |-  ( Pred ( R , A , X ) e. B -> ( Pred ( R , A , X ) e. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) <-> E. z z ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) Pred ( R , A , X ) ) )
12 10 11 mpbird 
 |-  ( Pred ( R , A , X ) e. B -> Pred ( R , A , X ) e. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) )
13 elssuni 
 |-  ( Pred ( R , A , X ) e. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) -> Pred ( R , A , X ) C_ U. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) )
14 12 13 syl 
 |-  ( Pred ( R , A , X ) e. B -> Pred ( R , A , X ) C_ U. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) )
15 df-trpred 
 |-  TrPred ( R , A , X ) = U. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om )
16 14 15 sseqtrrdi 
 |-  ( Pred ( R , A , X ) e. B -> Pred ( R , A , X ) C_ TrPred ( R , A , X ) )