Metamath Proof Explorer

Theorem trpredrec

Description: A transitive predecessor of X is either an immediate predecessor of X or an immediate predecessor of a transitive predecessor of X . (Contributed by Scott Fenton, 9-May-2012) (Revised by Mario Carneiro, 26-Jun-2015)

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

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 nn0suc 
 |-  ( i e. _om -> ( i = (/) \/ E. j e. _om i = suc j ) )
3 fveq2 
 |-  ( i = (/) -> ( ( 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 ) ` (/) ) )
4 3 eleq2d 
 |-  ( i = (/) -> ( 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 ) ` (/) ) ) )
5 4 anbi2d 
 |-  ( i = (/) -> ( ( ( X e. A /\ R Se A ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) <-> ( ( X e. A /\ R Se A ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` (/) ) ) ) )
6 5 biimpd 
 |-  ( i = (/) -> ( ( ( X e. A /\ R Se A ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) -> ( ( X e. A /\ R Se A ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` (/) ) ) ) )
7 setlikespec 
 |-  ( ( X e. A /\ R Se A ) -> Pred ( R , A , X ) e. _V )
8 fr0g 
 |-  ( Pred ( R , A , X ) e. _V -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` (/) ) = Pred ( R , A , X ) )
9 7 8 syl 
 |-  ( ( X e. A /\ R Se A ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` (/) ) = Pred ( R , A , X ) )
10 9 eleq2d 
 |-  ( ( X e. A /\ R Se A ) -> ( Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` (/) ) <-> Y e. Pred ( R , A , X ) ) )
11 10 biimpa 
 |-  ( ( ( X e. A /\ R Se A ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` (/) ) ) -> Y e. Pred ( R , A , X ) )
12 6 11 syl6com 
 |-  ( ( ( X e. A /\ R Se A ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) -> ( i = (/) -> Y e. Pred ( R , A , X ) ) )
13 fveq2 
 |-  ( i = suc j -> ( ( 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 j ) )
14 13 eleq2d 
 |-  ( i = suc j -> ( 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 ) ` suc j ) ) )
15 14 anbi2d 
 |-  ( i = suc j -> ( ( ( X e. A /\ R Se A ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) <-> ( ( X e. A /\ R Se A ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) ) ) )
16 15 biimpd 
 |-  ( i = suc j -> ( ( ( X e. A /\ R Se A ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) -> ( ( X e. A /\ R Se A ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) ) ) )
17 fvex 
 |-  ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) e. _V
18 trpredlem1 
 |-  ( Pred ( R , A , X ) e. _V -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) C_ A )
19 7 18 syl 
 |-  ( ( X e. A /\ R Se A ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) C_ A )
20 19 sseld 
 |-  ( ( X e. A /\ R Se A ) -> ( z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) -> z e. A ) )
21 setlikespec 
 |-  ( ( z e. A /\ R Se A ) -> Pred ( R , A , z ) e. _V )
22 21 expcom 
 |-  ( R Se A -> ( z e. A -> Pred ( R , A , z ) e. _V ) )
23 22 adantl 
 |-  ( ( X e. A /\ R Se A ) -> ( z e. A -> Pred ( R , A , z ) e. _V ) )
24 20 23 syld 
 |-  ( ( X e. A /\ R Se A ) -> ( z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) -> Pred ( R , A , z ) e. _V ) )
25 24 ralrimiv 
 |-  ( ( X e. A /\ R Se A ) -> A. z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , z ) e. _V )
26 iunexg 
 |-  ( ( ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) e. _V /\ A. z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , z ) e. _V ) -> U_ z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , z ) e. _V )
27 17 25 26 sylancr 
 |-  ( ( X e. A /\ R Se A ) -> U_ z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , z ) e. _V )
28 nfcv 
 |-  F/_ a Pred ( R , A , X )
29 nfcv 
 |-  F/_ a j
30 nfmpt1 
 |-  F/_ a ( a e. _V |-> U_ y e. a Pred ( R , A , y ) )
31 30 28 nfrdg 
 |-  F/_ a rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) )
32 nfcv 
 |-  F/_ a _om
33 31 32 nfres 
 |-  F/_ a ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om )
34 33 29 nffv 
 |-  F/_ a ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j )
35 nfcv 
 |-  F/_ a Pred ( R , A , z )
36 34 35 nfiun 
 |-  F/_ a U_ z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , z )
37 eqid 
 |-  ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) = ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om )
38 predeq3 
 |-  ( y = z -> Pred ( R , A , y ) = Pred ( R , A , z ) )
39 38 cbviunv 
 |-  U_ y e. a Pred ( R , A , y ) = U_ z e. a Pred ( R , A , z )
40 iuneq1 
 |-  ( a = ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) -> U_ z e. a Pred ( R , A , z ) = U_ z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , z ) )
41 39 40 eqtrid 
 |-  ( a = ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) -> U_ y e. a Pred ( R , A , y ) = U_ z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , z ) )
42 28 29 36 37 41 frsucmpt 
 |-  ( ( j e. _om /\ U_ z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , z ) e. _V ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) = U_ z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , z ) )
43 27 42 sylan2 
 |-  ( ( j e. _om /\ ( X e. A /\ R Se A ) ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) = U_ z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , z ) )
44 43 eleq2d 
 |-  ( ( j e. _om /\ ( X e. A /\ R Se A ) ) -> ( Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) <-> Y e. U_ z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , z ) ) )
45 44 biimpd 
 |-  ( ( j e. _om /\ ( X e. A /\ R Se A ) ) -> ( Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) -> Y e. U_ z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , z ) ) )
46 45 expimpd 
 |-  ( j e. _om -> ( ( ( X e. A /\ R Se A ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) ) -> Y e. U_ z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , z ) ) )
47 eliun 
 |-  ( Y e. U_ z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , z ) <-> E. z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Y e. Pred ( R , A , z ) )
48 ssiun2 
 |-  ( j e. _om -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) C_ U_ j e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) )
49 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 )
50 48 49 sseqtrrdi 
 |-  ( j e. _om -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) C_ TrPred ( R , A , X ) )
51 50 sseld 
 |-  ( j e. _om -> ( z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) -> z e. TrPred ( R , A , X ) ) )
52 vex 
 |-  z e. _V
53 52 elpredim 
 |-  ( Y e. Pred ( R , A , z ) -> Y R z )
54 53 a1i 
 |-  ( j e. _om -> ( Y e. Pred ( R , A , z ) -> Y R z ) )
55 51 54 anim12d 
 |-  ( j e. _om -> ( ( z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) /\ Y e. Pred ( R , A , z ) ) -> ( z e. TrPred ( R , A , X ) /\ Y R z ) ) )
56 55 reximdv2 
 |-  ( j e. _om -> ( E. z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Y e. Pred ( R , A , z ) -> E. z e. TrPred ( R , A , X ) Y R z ) )
57 56 com12 
 |-  ( E. z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Y e. Pred ( R , A , z ) -> ( j e. _om -> E. z e. TrPred ( R , A , X ) Y R z ) )
58 47 57 sylbi 
 |-  ( Y e. U_ z e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , z ) -> ( j e. _om -> E. z e. TrPred ( R , A , X ) Y R z ) )
59 46 58 syl6com 
 |-  ( ( ( X e. A /\ R Se A ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) ) -> ( j e. _om -> ( j e. _om -> E. z e. TrPred ( R , A , X ) Y R z ) ) )
60 59 pm2.43d 
 |-  ( ( ( X e. A /\ R Se A ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) ) -> ( j e. _om -> E. z e. TrPred ( R , A , X ) Y R z ) )
61 16 60 syl6com 
 |-  ( ( ( X e. A /\ R Se A ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) -> ( i = suc j -> ( j e. _om -> E. z e. TrPred ( R , A , X ) Y R z ) ) )
62 61 com23 
 |-  ( ( ( X e. A /\ R Se A ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) -> ( j e. _om -> ( i = suc j -> E. z e. TrPred ( R , A , X ) Y R z ) ) )
63 62 rexlimdv 
 |-  ( ( ( X e. A /\ R Se A ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) -> ( E. j e. _om i = suc j -> E. z e. TrPred ( R , A , X ) Y R z ) )
64 12 63 orim12d 
 |-  ( ( ( X e. A /\ R Se A ) /\ Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) ) -> ( ( i = (/) \/ E. j e. _om i = suc j ) -> ( Y e. Pred ( R , A , X ) \/ E. z e. TrPred ( R , A , X ) Y R z ) ) )
65 64 ex 
 |-  ( ( X e. A /\ R Se A ) -> ( Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) -> ( ( i = (/) \/ E. j e. _om i = suc j ) -> ( Y e. Pred ( R , A , X ) \/ E. z e. TrPred ( R , A , X ) Y R z ) ) ) )
66 65 com23 
 |-  ( ( X e. A /\ R Se A ) -> ( ( i = (/) \/ E. j e. _om i = suc j ) -> ( Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) -> ( Y e. Pred ( R , A , X ) \/ E. z e. TrPred ( R , A , X ) Y R z ) ) ) )
67 2 66 syl5 
 |-  ( ( 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. Pred ( R , A , X ) \/ E. z e. TrPred ( R , A , X ) Y R z ) ) ) )
68 67 rexlimdv 
 |-  ( ( 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 ) -> ( Y e. Pred ( R , A , X ) \/ E. z e. TrPred ( R , A , X ) Y R z ) ) )
69 1 68 syl5bi 
 |-  ( ( X e. A /\ R Se A ) -> ( Y e. TrPred ( R , A , X ) -> ( Y e. Pred ( R , A , X ) \/ E. z e. TrPred ( R , A , X ) Y R z ) ) )