Metamath Proof Explorer

Theorem trpredlem1

Description: Technical lemma for transitive predecessors properties. All values of the transitive predecessors' underlying function are subclasses of the base class. (Contributed by Scott Fenton, 28-Apr-2012)

Ref Expression
Assertion trpredlem1 
|- ( Pred ( R , A , X ) e. B -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A )

Proof

Step Hyp Ref Expression
1 nn0suc 
 |-  ( i e. _om -> ( i = (/) \/ E. j e. _om i = suc j ) )
2 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 ) )
3 predss 
 |-  Pred ( R , A , X ) C_ A
4 2 3 eqsstrdi 
 |-  ( Pred ( R , A , X ) e. B -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` (/) ) C_ A )
5 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 ) ` (/) ) )
6 5 sseq1d 
 |-  ( i = (/) -> ( ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A <-> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` (/) ) C_ A ) )
7 4 6 syl5ibr 
 |-  ( i = (/) -> ( Pred ( R , A , X ) e. B -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A ) )
8 nfcv 
 |-  F/_ a Pred ( R , A , X )
9 nfcv 
 |-  F/_ a j
10 nfmpt1 
 |-  F/_ a ( a e. _V |-> U_ y e. a Pred ( R , A , y ) )
11 10 8 nfrdg 
 |-  F/_ a rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) )
12 nfcv 
 |-  F/_ a _om
13 11 12 nfres 
 |-  F/_ a ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om )
14 13 9 nffv 
 |-  F/_ a ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j )
15 nfcv 
 |-  F/_ a Pred ( R , A , e )
16 14 15 nfiun 
 |-  F/_ a U_ e e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , e )
17 predeq3 
 |-  ( y = e -> Pred ( R , A , y ) = Pred ( R , A , e ) )
18 17 cbviunv 
 |-  U_ y e. a Pred ( R , A , y ) = U_ e e. a Pred ( R , A , e )
19 18 mpteq2i 
 |-  ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) = ( a e. _V |-> U_ e e. a Pred ( R , A , e ) )
20 rdgeq1 
 |-  ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) = ( a e. _V |-> U_ e e. a Pred ( R , A , e ) ) -> rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) = rec ( ( a e. _V |-> U_ e e. a Pred ( R , A , e ) ) , Pred ( R , A , X ) ) )
21 reseq1 
 |-  ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) = rec ( ( a e. _V |-> U_ e e. a Pred ( R , A , e ) ) , Pred ( R , A , X ) ) -> ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) = ( rec ( ( a e. _V |-> U_ e e. a Pred ( R , A , e ) ) , Pred ( R , A , X ) ) |` _om ) )
22 19 20 21 mp2b 
 |-  ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) = ( rec ( ( a e. _V |-> U_ e e. a Pred ( R , A , e ) ) , Pred ( R , A , X ) ) |` _om )
23 iuneq1 
 |-  ( a = ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) -> U_ e e. a Pred ( R , A , e ) = U_ e e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , e ) )
24 8 9 16 22 23 frsucmpt 
 |-  ( ( j e. _om /\ U_ e e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , e ) e. _V ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) = U_ e e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , e ) )
25 iunss 
 |-  ( U_ e e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , e ) C_ A <-> A. e e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , e ) C_ A )
26 predss 
 |-  Pred ( R , A , e ) C_ A
27 26 a1i 
 |-  ( e e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) -> Pred ( R , A , e ) C_ A )
28 25 27 mprgbir 
 |-  U_ e e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , e ) C_ A
29 24 28 eqsstrdi 
 |-  ( ( j e. _om /\ U_ e e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , e ) e. _V ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) C_ A )
30 8 9 16 22 23 frsucmptn 
 |-  ( -. U_ e e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , e ) e. _V -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) = (/) )
31 30 adantl 
 |-  ( ( j e. _om /\ -. U_ e e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , e ) e. _V ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) = (/) )
32 0ss 
 |-  (/) C_ A
33 31 32 eqsstrdi 
 |-  ( ( j e. _om /\ -. U_ e e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` j ) Pred ( R , A , e ) e. _V ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) C_ A )
34 29 33 pm2.61dan 
 |-  ( j e. _om -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) C_ A )
35 34 adantr 
 |-  ( ( j e. _om /\ i = suc j ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) C_ A )
36 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 ) )
37 36 sseq1d 
 |-  ( i = suc j -> ( ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A <-> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) C_ A ) )
38 37 adantl 
 |-  ( ( j e. _om /\ i = suc j ) -> ( ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A <-> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` suc j ) C_ A ) )
39 35 38 mpbird 
 |-  ( ( j e. _om /\ i = suc j ) -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A )
40 39 rexlimiva 
 |-  ( E. j e. _om i = suc j -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A )
41 40 a1d 
 |-  ( E. j e. _om i = suc j -> ( Pred ( R , A , X ) e. B -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A ) )
42 7 41 jaoi 
 |-  ( ( i = (/) \/ E. j e. _om i = suc j ) -> ( Pred ( R , A , X ) e. B -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A ) )
43 1 42 syl 
 |-  ( i e. _om -> ( Pred ( R , A , X ) e. B -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A ) )
44 nfvres 
 |-  ( -. i e. _om -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) = (/) )
45 44 32 eqsstrdi 
 |-  ( -. i e. _om -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A )
46 45 a1d 
 |-  ( -. i e. _om -> ( Pred ( R , A , X ) e. B -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A ) )
47 43 46 pm2.61i 
 |-  ( Pred ( R , A , X ) e. B -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A )