Metamath Proof Explorer

Theorem trpredmintr

Description: The transitive predecessors form the smallest class transitive in R and A . That is, if B is another R , A transitive class containing Pred ( R , A , X ) , then TrPred ( R , A , X ) C_ B (Contributed by Scott Fenton, 25-Apr-2012) (Revised by Mario Carneiro, 26-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 dftrpred2 
 |-  TrPred ( R , A , X ) = U_ i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i )
2 fveq2 
 |-  ( j = (/) -> ( ( 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 ) ` (/) ) )
3 2 sseq1d 
 |-  ( j = (/) -> ( ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) C_ B <-> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` (/) ) C_ B ) )
4 3 imbi2d 
 |-  ( j = (/) -> ( ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) C_ B ) <-> ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` (/) ) C_ B ) ) )
5 fveq2 
 |-  ( j = k -> ( ( 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 ) ` k ) )
6 5 sseq1d 
 |-  ( j = k -> ( ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) C_ B <-> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B ) )
7 6 imbi2d 
 |-  ( j = k -> ( ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) C_ B ) <-> ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B ) ) )
8 fveq2 
 |-  ( j = suc k -> ( ( 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 k ) )
9 8 sseq1d 
 |-  ( j = suc k -> ( ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) C_ B <-> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc k ) C_ B ) )
10 9 imbi2d 
 |-  ( j = suc k -> ( ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) C_ B ) <-> ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc k ) C_ B ) ) )
11 fveq2 
 |-  ( j = 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 ) ` i ) )
12 11 sseq1d 
 |-  ( j = i -> ( ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) C_ B <-> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ B ) )
13 12 imbi2d 
 |-  ( j = i -> ( ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) C_ B ) <-> ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ B ) ) )
14 setlikespec 
 |-  ( ( X e. A /\ R Se A ) -> Pred ( R , A , X ) e. _V )
15 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 ) )
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 ) ` (/) ) = Pred ( R , A , X ) )
17 16 adantr 
 |-  ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` (/) ) = Pred ( R , A , X ) )
18 simprr 
 |-  ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> Pred ( R , A , X ) C_ B )
19 17 18 eqsstrd 
 |-  ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` (/) ) C_ B )
20 fvex 
 |-  ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) e. _V
21 trpredlem1 
 |-  ( Pred ( R , A , X ) e. _V -> ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ A )
22 14 21 syl 
 |-  ( ( X e. A /\ R Se A ) -> ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ A )
23 22 sseld 
 |-  ( ( X e. A /\ R Se A ) -> ( y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) -> y e. A ) )
24 setlikespec 
 |-  ( ( y e. A /\ R Se A ) -> Pred ( R , A , y ) e. _V )
25 24 expcom 
 |-  ( R Se A -> ( y e. A -> Pred ( R , A , y ) e. _V ) )
26 25 adantl 
 |-  ( ( X e. A /\ R Se A ) -> ( y e. A -> Pred ( R , A , y ) e. _V ) )
27 23 26 syld 
 |-  ( ( X e. A /\ R Se A ) -> ( y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) -> Pred ( R , A , y ) e. _V ) )
28 27 ralrimiv 
 |-  ( ( X e. A /\ R Se A ) -> A. y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) Pred ( R , A , y ) e. _V )
29 28 ad2antrr 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) /\ ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B ) -> A. y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) Pred ( R , A , y ) e. _V )
30 iunexg 
 |-  ( ( ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) e. _V /\ A. y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) Pred ( R , A , y ) e. _V ) -> U_ y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) Pred ( R , A , y ) e. _V )
31 20 29 30 sylancr 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) /\ ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B ) -> U_ y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) Pred ( R , A , y ) e. _V )
32 nfcv 
 |-  F/_ a Pred ( R , A , X )
33 nfcv 
 |-  F/_ a k
34 nfcv 
 |-  F/_ a U_ y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) Pred ( R , A , y )
35 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 )
36 predeq3 
 |-  ( y = d -> Pred ( R , A , y ) = Pred ( R , A , d ) )
37 36 cbviunv 
 |-  U_ y e. a Pred ( R , A , y ) = U_ d e. a Pred ( R , A , d )
38 iuneq1 
 |-  ( a = c -> U_ d e. a Pred ( R , A , d ) = U_ d e. c Pred ( R , A , d ) )
39 37 38 syl5eq 
 |-  ( a = c -> U_ y e. a Pred ( R , A , y ) = U_ d e. c Pred ( R , A , d ) )
40 39 cbvmptv 
 |-  ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) = ( c e. _V |-> U_ d e. c Pred ( R , A , d ) )
41 rdgeq1 
 |-  ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) = ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) -> rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) = rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) )
42 reseq1 
 |-  ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) = rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) -> ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) = ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) )
43 40 41 42 mp2b 
 |-  ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) = ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om )
44 43 fveq1i 
 |-  ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) = ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k )
45 44 eqeq2i 
 |-  ( a = ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) <-> a = ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) )
46 iuneq1 
 |-  ( a = ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) -> U_ y e. a Pred ( R , A , y ) = U_ y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) Pred ( R , A , y ) )
47 45 46 sylbi 
 |-  ( a = ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) -> U_ y e. a Pred ( R , A , y ) = U_ y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) Pred ( R , A , y ) )
48 32 33 34 35 47 frsucmpt 
 |-  ( ( k e. _om /\ U_ y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) Pred ( R , A , y ) e. _V ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc k ) = U_ y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) Pred ( R , A , y ) )
49 31 48 sylan2 
 |-  ( ( k e. _om /\ ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) /\ ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B ) ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc k ) = U_ y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) Pred ( R , A , y ) )
50 44 sseq1i 
 |-  ( ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B <-> ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B )
51 50 anbi2i 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) /\ ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B ) <-> ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) /\ ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B ) )
52 nfv 
 |-  F/ y ( X e. A /\ R Se A )
53 nfra1 
 |-  F/ y A. y e. B Pred ( R , A , y ) C_ B
54 nfv 
 |-  F/ y Pred ( R , A , X ) C_ B
55 53 54 nfan 
 |-  F/ y ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B )
56 52 55 nfan 
 |-  F/ y ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) )
57 nfv 
 |-  F/ y ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B
58 56 57 nfan 
 |-  F/ y ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) /\ ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B )
59 ssel 
 |-  ( ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B -> ( y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) -> y e. B ) )
60 rsp 
 |-  ( A. y e. B Pred ( R , A , y ) C_ B -> ( y e. B -> Pred ( R , A , y ) C_ B ) )
61 60 ad2antrl 
 |-  ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> ( y e. B -> Pred ( R , A , y ) C_ B ) )
62 59 61 sylan9r 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) /\ ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B ) -> ( y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) -> Pred ( R , A , y ) C_ B ) )
63 58 62 ralrimi 
 |-  ( ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) /\ ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B ) -> A. y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) Pred ( R , A , y ) C_ B )
64 63 adantl 
 |-  ( ( k e. _om /\ ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) /\ ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B ) ) -> A. y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) Pred ( R , A , y ) C_ B )
65 51 64 sylan2b 
 |-  ( ( k e. _om /\ ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) /\ ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B ) ) -> A. y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) Pred ( R , A , y ) C_ B )
66 iunss 
 |-  ( U_ y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) Pred ( R , A , y ) C_ B <-> A. y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) Pred ( R , A , y ) C_ B )
67 65 66 sylibr 
 |-  ( ( k e. _om /\ ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) /\ ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B ) ) -> U_ y e. ( ( rec ( ( c e. _V |-> U_ d e. c Pred ( R , A , d ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) Pred ( R , A , y ) C_ B )
68 49 67 eqsstrd 
 |-  ( ( k e. _om /\ ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) /\ ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B ) ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc k ) C_ B )
69 68 exp32 
 |-  ( k e. _om -> ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> ( ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc k ) C_ B ) ) )
70 69 a2d 
 |-  ( k e. _om -> ( ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` k ) C_ B ) -> ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc k ) C_ B ) ) )
71 4 7 10 13 19 70 finds 
 |-  ( i e. _om -> ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ B ) )
72 71 com12 
 |-  ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> ( i e. _om -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ B ) )
73 72 ralrimiv 
 |-  ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> A. i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ B )
74 iunss 
 |-  ( U_ i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ B <-> A. i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ B )
75 73 74 sylibr 
 |-  ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> U_ i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ B )
76 1 75 eqsstrid 
 |-  ( ( ( X e. A /\ R Se A ) /\ ( A. y e. B Pred ( R , A , y ) C_ B /\ Pred ( R , A , X ) C_ B ) ) -> TrPred ( R , A , X ) C_ B )