Metamath Proof Explorer

Theorem dftrpred3g

Description: The transitive predecessors of X are equal to the predecessors of X together with their transitive predecessors. (Contributed by Scott Fenton, 26-Apr-2012) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion dftrpred3g 
|- ( ( X e. A /\ R Se A ) -> TrPred ( R , A , X ) = ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) )

Proof

Step Hyp Ref Expression
1 elun 
 |-  ( z e. ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) <-> ( z e. Pred ( R , A , X ) \/ z e. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) )
2 predel 
 |-  ( z e. Pred ( R , A , X ) -> z e. A )
3 setlikespec 
 |-  ( ( z e. A /\ R Se A ) -> Pred ( R , A , z ) e. _V )
4 trpredpred 
 |-  ( Pred ( R , A , z ) e. _V -> Pred ( R , A , z ) C_ TrPred ( R , A , z ) )
5 3 4 syl 
 |-  ( ( z e. A /\ R Se A ) -> Pred ( R , A , z ) C_ TrPred ( R , A , z ) )
6 5 expcom 
 |-  ( R Se A -> ( z e. A -> Pred ( R , A , z ) C_ TrPred ( R , A , z ) ) )
7 6 adantl 
 |-  ( ( X e. A /\ R Se A ) -> ( z e. A -> Pred ( R , A , z ) C_ TrPred ( R , A , z ) ) )
8 2 7 syl5 
 |-  ( ( X e. A /\ R Se A ) -> ( z e. Pred ( R , A , X ) -> Pred ( R , A , z ) C_ TrPred ( R , A , z ) ) )
9 8 ancld 
 |-  ( ( X e. A /\ R Se A ) -> ( z e. Pred ( R , A , X ) -> ( z e. Pred ( R , A , X ) /\ Pred ( R , A , z ) C_ TrPred ( R , A , z ) ) ) )
10 trpredeq3 
 |-  ( y = z -> TrPred ( R , A , y ) = TrPred ( R , A , z ) )
11 10 sseq2d 
 |-  ( y = z -> ( Pred ( R , A , z ) C_ TrPred ( R , A , y ) <-> Pred ( R , A , z ) C_ TrPred ( R , A , z ) ) )
12 11 rspcev 
 |-  ( ( z e. Pred ( R , A , X ) /\ Pred ( R , A , z ) C_ TrPred ( R , A , z ) ) -> E. y e. Pred ( R , A , X ) Pred ( R , A , z ) C_ TrPred ( R , A , y ) )
13 ssiun 
 |-  ( E. y e. Pred ( R , A , X ) Pred ( R , A , z ) C_ TrPred ( R , A , y ) -> Pred ( R , A , z ) C_ U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) )
14 12 13 syl 
 |-  ( ( z e. Pred ( R , A , X ) /\ Pred ( R , A , z ) C_ TrPred ( R , A , z ) ) -> Pred ( R , A , z ) C_ U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) )
15 9 14 syl6 
 |-  ( ( X e. A /\ R Se A ) -> ( z e. Pred ( R , A , X ) -> Pred ( R , A , z ) C_ U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) )
16 eliun 
 |-  ( z e. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) <-> E. y e. Pred ( R , A , X ) z e. TrPred ( R , A , y ) )
17 predel 
 |-  ( y e. Pred ( R , A , X ) -> y e. A )
18 setlikespec 
 |-  ( ( y e. A /\ R Se A ) -> Pred ( R , A , y ) e. _V )
19 18 ancoms 
 |-  ( ( R Se A /\ y e. A ) -> Pred ( R , A , y ) e. _V )
20 19 adantll 
 |-  ( ( ( X e. A /\ R Se A ) /\ y e. A ) -> Pred ( R , A , y ) e. _V )
21 trpredss 
 |-  ( Pred ( R , A , y ) e. _V -> TrPred ( R , A , y ) C_ A )
22 20 21 syl 
 |-  ( ( ( X e. A /\ R Se A ) /\ y e. A ) -> TrPred ( R , A , y ) C_ A )
23 22 sseld 
 |-  ( ( ( X e. A /\ R Se A ) /\ y e. A ) -> ( z e. TrPred ( R , A , y ) -> z e. A ) )
24 3 expcom 
 |-  ( R Se A -> ( z e. A -> Pred ( R , A , z ) e. _V ) )
25 24 ad2antlr 
 |-  ( ( ( X e. A /\ R Se A ) /\ y e. A ) -> ( z e. A -> Pred ( R , A , z ) e. _V ) )
26 23 25 syld 
 |-  ( ( ( X e. A /\ R Se A ) /\ y e. A ) -> ( z e. TrPred ( R , A , y ) -> Pred ( R , A , z ) e. _V ) )
27 26 imp 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ y e. A ) /\ z e. TrPred ( R , A , y ) ) -> Pred ( R , A , z ) e. _V )
28 27 4 syl 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ y e. A ) /\ z e. TrPred ( R , A , y ) ) -> Pred ( R , A , z ) C_ TrPred ( R , A , z ) )
29 simpr 
 |-  ( ( ( X e. A /\ R Se A ) /\ y e. A ) -> y e. A )
30 simplr 
 |-  ( ( ( X e. A /\ R Se A ) /\ y e. A ) -> R Se A )
31 trpredelss 
 |-  ( ( y e. A /\ R Se A ) -> ( z e. TrPred ( R , A , y ) -> TrPred ( R , A , z ) C_ TrPred ( R , A , y ) ) )
32 29 30 31 syl2anc 
 |-  ( ( ( X e. A /\ R Se A ) /\ y e. A ) -> ( z e. TrPred ( R , A , y ) -> TrPred ( R , A , z ) C_ TrPred ( R , A , y ) ) )
33 32 imp 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ y e. A ) /\ z e. TrPred ( R , A , y ) ) -> TrPred ( R , A , z ) C_ TrPred ( R , A , y ) )
34 28 33 sstrd 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ y e. A ) /\ z e. TrPred ( R , A , y ) ) -> Pred ( R , A , z ) C_ TrPred ( R , A , y ) )
35 34 exp31 
 |-  ( ( X e. A /\ R Se A ) -> ( y e. A -> ( z e. TrPred ( R , A , y ) -> Pred ( R , A , z ) C_ TrPred ( R , A , y ) ) ) )
36 17 35 syl5 
 |-  ( ( X e. A /\ R Se A ) -> ( y e. Pred ( R , A , X ) -> ( z e. TrPred ( R , A , y ) -> Pred ( R , A , z ) C_ TrPred ( R , A , y ) ) ) )
37 36 reximdvai 
 |-  ( ( X e. A /\ R Se A ) -> ( E. y e. Pred ( R , A , X ) z e. TrPred ( R , A , y ) -> E. y e. Pred ( R , A , X ) Pred ( R , A , z ) C_ TrPred ( R , A , y ) ) )
38 37 13 syl6 
 |-  ( ( X e. A /\ R Se A ) -> ( E. y e. Pred ( R , A , X ) z e. TrPred ( R , A , y ) -> Pred ( R , A , z ) C_ U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) )
39 16 38 syl5bi 
 |-  ( ( X e. A /\ R Se A ) -> ( z e. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) -> Pred ( R , A , z ) C_ U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) )
40 15 39 jaod 
 |-  ( ( X e. A /\ R Se A ) -> ( ( z e. Pred ( R , A , X ) \/ z e. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) -> Pred ( R , A , z ) C_ U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) )
41 ssun4 
 |-  ( Pred ( R , A , z ) C_ U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) -> Pred ( R , A , z ) C_ ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) )
42 40 41 syl6 
 |-  ( ( X e. A /\ R Se A ) -> ( ( z e. Pred ( R , A , X ) \/ z e. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) -> Pred ( R , A , z ) C_ ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) ) )
43 1 42 syl5bi 
 |-  ( ( X e. A /\ R Se A ) -> ( z e. ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) -> Pred ( R , A , z ) C_ ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) ) )
44 43 ralrimiv 
 |-  ( ( X e. A /\ R Se A ) -> A. z e. ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) Pred ( R , A , z ) C_ ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) )
45 ssun1 
 |-  Pred ( R , A , X ) C_ ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) )
46 44 45 jctir 
 |-  ( ( X e. A /\ R Se A ) -> ( A. z e. ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) Pred ( R , A , z ) C_ ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) /\ Pred ( R , A , X ) C_ ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) ) )
47 trpredmintr 
 |-  ( ( ( X e. A /\ R Se A ) /\ ( A. z e. ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) Pred ( R , A , z ) C_ ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) /\ Pred ( R , A , X ) C_ ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) ) ) -> TrPred ( R , A , X ) C_ ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) )
48 46 47 mpdan 
 |-  ( ( X e. A /\ R Se A ) -> TrPred ( R , A , X ) C_ ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) )
49 setlikespec 
 |-  ( ( X e. A /\ R Se A ) -> Pred ( R , A , X ) e. _V )
50 trpredpred 
 |-  ( Pred ( R , A , X ) e. _V -> Pred ( R , A , X ) C_ TrPred ( R , A , X ) )
51 49 50 syl 
 |-  ( ( X e. A /\ R Se A ) -> Pred ( R , A , X ) C_ TrPred ( R , A , X ) )
52 51 sseld 
 |-  ( ( X e. A /\ R Se A ) -> ( y e. Pred ( R , A , X ) -> y e. TrPred ( R , A , X ) ) )
53 trpredelss 
 |-  ( ( X e. A /\ R Se A ) -> ( y e. TrPred ( R , A , X ) -> TrPred ( R , A , y ) C_ TrPred ( R , A , X ) ) )
54 52 53 syld 
 |-  ( ( X e. A /\ R Se A ) -> ( y e. Pred ( R , A , X ) -> TrPred ( R , A , y ) C_ TrPred ( R , A , X ) ) )
55 54 ralrimiv 
 |-  ( ( X e. A /\ R Se A ) -> A. y e. Pred ( R , A , X ) TrPred ( R , A , y ) C_ TrPred ( R , A , X ) )
56 iunss 
 |-  ( U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) C_ TrPred ( R , A , X ) <-> A. y e. Pred ( R , A , X ) TrPred ( R , A , y ) C_ TrPred ( R , A , X ) )
57 55 56 sylibr 
 |-  ( ( X e. A /\ R Se A ) -> U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) C_ TrPred ( R , A , X ) )
58 51 57 unssd 
 |-  ( ( X e. A /\ R Se A ) -> ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) C_ TrPred ( R , A , X ) )
59 48 58 eqssd 
 |-  ( ( X e. A /\ R Se A ) -> TrPred ( R , A , X ) = ( Pred ( R , A , X ) u. U_ y e. Pred ( R , A , X ) TrPred ( R , A , y ) ) )