Metamath Proof Explorer

Theorem trpredtr

Description: Predecessors of a transitive predecessor are transitive predecessors. (Contributed by Scott Fenton, 20-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion trpredtr 
|- ( ( X e. A /\ R Se A ) -> ( Y e. TrPred ( R , A , X ) -> Pred ( R , A , Y ) C_ TrPred ( R , A , X ) ) )

Proof

Step Hyp Ref Expression
1 eltrpred 
 |-  ( Y e. TrPred ( R , A , X ) <-> E. i e. _om Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) )
2 simplr 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ i e. _om ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) -> i e. _om )
3 peano2 
 |-  ( i e. _om -> suc i e. _om )
4 2 3 syl 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ i e. _om ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) -> suc i e. _om )
5 simpr 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ i e. _om ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) -> Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) )
6 ssid 
 |-  Pred ( R , A , Y ) C_ Pred ( R , A , Y )
7 predeq3 
 |-  ( t = Y -> Pred ( R , A , t ) = Pred ( R , A , Y ) )
8 7 sseq2d 
 |-  ( t = Y -> ( Pred ( R , A , Y ) C_ Pred ( R , A , t ) <-> Pred ( R , A , Y ) C_ Pred ( R , A , Y ) ) )
9 8 rspcev 
 |-  ( ( Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) /\ Pred ( R , A , Y ) C_ Pred ( R , A , Y ) ) -> E. t e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) Pred ( R , A , Y ) C_ Pred ( R , A , t ) )
10 ssiun 
 |-  ( E. t e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) Pred ( R , A , Y ) C_ Pred ( R , A , t ) -> Pred ( R , A , Y ) C_ U_ t e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) Pred ( R , A , t ) )
11 9 10 syl 
 |-  ( ( Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) /\ Pred ( R , A , Y ) C_ Pred ( R , A , Y ) ) -> Pred ( R , A , Y ) C_ U_ t e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) Pred ( R , A , t ) )
12 5 6 11 sylancl 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ i e. _om ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) -> Pred ( R , A , Y ) C_ U_ t e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) Pred ( R , A , t ) )
13 fvex 
 |-  ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) e. _V
14 setlikespec 
 |-  ( ( X e. A /\ R Se A ) -> Pred ( R , A , X ) e. _V )
15 trpredlem1 
 |-  ( Pred ( R , A , X ) e. _V -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A )
16 14 15 syl 
 |-  ( ( X e. A /\ R Se A ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A )
17 16 sseld 
 |-  ( ( X e. A /\ R Se A ) -> ( t e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) -> t e. A ) )
18 setlikespec 
 |-  ( ( t e. A /\ R Se A ) -> Pred ( R , A , t ) e. _V )
19 18 expcom 
 |-  ( R Se A -> ( t e. A -> Pred ( R , A , t ) e. _V ) )
20 19 adantl 
 |-  ( ( X e. A /\ R Se A ) -> ( t e. A -> Pred ( R , A , t ) e. _V ) )
21 17 20 syld 
 |-  ( ( X e. A /\ R Se A ) -> ( t e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) -> Pred ( R , A , t ) e. _V ) )
22 21 ralrimiv 
 |-  ( ( X e. A /\ R Se A ) -> A. t e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) Pred ( R , A , t ) e. _V )
23 22 ad2antrr 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ i e. _om ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) -> A. t e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) Pred ( R , A , t ) e. _V )
24 iunexg 
 |-  ( ( ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) e. _V /\ A. t e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) Pred ( R , A , t ) e. _V ) -> U_ t e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) Pred ( R , A , t ) e. _V )
25 13 23 24 sylancr 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ i e. _om ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) -> U_ t e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) Pred ( R , A , t ) e. _V )
26 nfcv 
 |-  F/_ f Pred ( R , A , X )
27 nfcv 
 |-  F/_ f i
28 nfcv 
 |-  F/_ f U_ t e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) Pred ( R , A , t )
29 predeq3 
 |-  ( y = t -> Pred ( R , A , y ) = Pred ( R , A , t ) )
30 29 cbviunv 
 |-  U_ y e. a Pred ( R , A , y ) = U_ t e. a Pred ( R , A , t )
31 iuneq1 
 |-  ( a = f -> U_ t e. a Pred ( R , A , t ) = U_ t e. f Pred ( R , A , t ) )
32 30 31 eqtrid 
 |-  ( a = f -> U_ y e. a Pred ( R , A , y ) = U_ t e. f Pred ( R , A , t ) )
33 32 cbvmptv 
 |-  ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) = ( f e. _V |-> U_ t e. f Pred ( R , A , t ) )
34 rdgeq1 
 |-  ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) = ( f e. _V |-> U_ t e. f Pred ( R , A , t ) ) -> rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) = rec ( ( f e. _V |-> U_ t e. f Pred ( R , A , t ) ) , Pred ( R , A , X ) ) )
35 reseq1 
 |-  ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) = rec ( ( f e. _V |-> U_ t e. f Pred ( R , A , t ) ) , Pred ( R , A , X ) ) -> ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) = ( rec ( ( f e. _V |-> U_ t e. f Pred ( R , A , t ) ) , Pred ( R , A , X ) ) |` _om ) )
36 33 34 35 mp2b 
 |-  ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) = ( rec ( ( f e. _V |-> U_ t e. f Pred ( R , A , t ) ) , Pred ( R , A , X ) ) |` _om )
37 iuneq1 
 |-  ( f = ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) -> U_ t e. f Pred ( R , A , t ) = U_ t e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) Pred ( R , A , t ) )
38 26 27 28 36 37 frsucmpt 
 |-  ( ( i e. _om /\ U_ t e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) Pred ( R , A , t ) e. _V ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc i ) = U_ t e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) Pred ( R , A , t ) )
39 2 25 38 syl2anc 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ i e. _om ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc i ) = U_ t e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) Pred ( R , A , t ) )
40 12 39 sseqtrrd 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ i e. _om ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) -> Pred ( R , A , Y ) C_ ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc i ) )
41 fveq2 
 |-  ( j = suc i -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) = ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc i ) )
42 41 sseq2d 
 |-  ( j = suc i -> ( Pred ( R , A , Y ) C_ ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) <-> Pred ( R , A , Y ) C_ ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc i ) ) )
43 42 rspcev 
 |-  ( ( suc i e. _om /\ Pred ( R , A , Y ) C_ ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc i ) ) -> E. j e. _om Pred ( R , A , Y ) C_ ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) )
44 ssiun 
 |-  ( E. j e. _om Pred ( R , A , Y ) C_ ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) -> Pred ( R , A , Y ) C_ U_ j e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) )
45 43 44 syl 
 |-  ( ( suc i e. _om /\ Pred ( R , A , Y ) C_ ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc i ) ) -> Pred ( R , A , Y ) C_ U_ j e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) )
46 dftrpred2 
 |-  TrPred ( R , A , X ) = U_ j e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j )
47 45 46 sseqtrrdi 
 |-  ( ( suc i e. _om /\ Pred ( R , A , Y ) C_ ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc i ) ) -> Pred ( R , A , Y ) C_ TrPred ( R , A , X ) )
48 4 40 47 syl2anc 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ i e. _om ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) -> Pred ( R , A , Y ) C_ TrPred ( R , A , X ) )
49 48 rexlimdva2 
 |-  ( ( X e. A /\ R Se A ) -> ( E. i e. _om Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) -> Pred ( R , A , Y ) C_ TrPred ( R , A , X ) ) )
50 1 49 syl5bi 
 |-  ( ( X e. A /\ R Se A ) -> ( Y e. TrPred ( R , A , X ) -> Pred ( R , A , Y ) C_ TrPred ( R , A , X ) ) )