Metamath Proof Explorer

Theorem trpred0

Description: The class of transitive predecessors is empty when A is empty. (Contributed by Scott Fenton, 30-Apr-2012)

Ref Expression
Assertion trpred0 
|- TrPred ( R , (/) , X ) = (/)

Proof

Step Hyp Ref Expression
1 dftrpred2 
 |-  TrPred ( R , (/) , X ) = U_ i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , (/) , y ) ) , Pred ( R , (/) , X ) ) |` _om ) ` i )
2 pred0 
 |-  Pred ( R , (/) , y ) = (/)
3 2 a1i 
 |-  ( y e. a -> Pred ( R , (/) , y ) = (/) )
4 3 iuneq2i 
 |-  U_ y e. a Pred ( R , (/) , y ) = U_ y e. a (/)
5 iun0 
 |-  U_ y e. a (/) = (/)
6 4 5 eqtri 
 |-  U_ y e. a Pred ( R , (/) , y ) = (/)
7 6 mpteq2i 
 |-  ( a e. _V |-> U_ y e. a Pred ( R , (/) , y ) ) = ( a e. _V |-> (/) )
8 pred0 
 |-  Pred ( R , (/) , X ) = (/)
9 rdgeq12 
 |-  ( ( ( a e. _V |-> U_ y e. a Pred ( R , (/) , y ) ) = ( a e. _V |-> (/) ) /\ Pred ( R , (/) , X ) = (/) ) -> rec ( ( a e. _V |-> U_ y e. a Pred ( R , (/) , y ) ) , Pred ( R , (/) , X ) ) = rec ( ( a e. _V |-> (/) ) , (/) ) )
10 7 8 9 mp2an 
 |-  rec ( ( a e. _V |-> U_ y e. a Pred ( R , (/) , y ) ) , Pred ( R , (/) , X ) ) = rec ( ( a e. _V |-> (/) ) , (/) )
11 10 reseq1i 
 |-  ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , (/) , y ) ) , Pred ( R , (/) , X ) ) |` _om ) = ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om )
12 11 fveq1i 
 |-  ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , (/) , y ) ) , Pred ( R , (/) , X ) ) |` _om ) ` i ) = ( ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om ) ` i )
13 nn0suc 
 |-  ( i e. _om -> ( i = (/) \/ E. j e. _om i = suc j ) )
14 fveq2 
 |-  ( i = (/) -> ( ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om ) ` i ) = ( ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om ) ` (/) ) )
15 0ex 
 |-  (/) e. _V
16 fr0g 
 |-  ( (/) e. _V -> ( ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om ) ` (/) ) = (/) )
17 15 16 ax-mp 
 |-  ( ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om ) ` (/) ) = (/)
18 14 17 eqtrdi 
 |-  ( i = (/) -> ( ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om ) ` i ) = (/) )
19 nfcv 
 |-  F/_ a (/)
20 nfcv 
 |-  F/_ a j
21 eqid 
 |-  ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om ) = ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om )
22 eqidd 
 |-  ( a = ( ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om ) ` j ) -> (/) = (/) )
23 19 20 19 21 22 frsucmpt 
 |-  ( ( j e. _om /\ (/) e. _V ) -> ( ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om ) ` suc j ) = (/) )
24 15 23 mpan2 
 |-  ( j e. _om -> ( ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om ) ` suc j ) = (/) )
25 fveqeq2 
 |-  ( i = suc j -> ( ( ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om ) ` i ) = (/) <-> ( ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om ) ` suc j ) = (/) ) )
26 24 25 syl5ibrcom 
 |-  ( j e. _om -> ( i = suc j -> ( ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om ) ` i ) = (/) ) )
27 26 rexlimiv 
 |-  ( E. j e. _om i = suc j -> ( ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om ) ` i ) = (/) )
28 18 27 jaoi 
 |-  ( ( i = (/) \/ E. j e. _om i = suc j ) -> ( ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om ) ` i ) = (/) )
29 13 28 syl 
 |-  ( i e. _om -> ( ( rec ( ( a e. _V |-> (/) ) , (/) ) |` _om ) ` i ) = (/) )
30 12 29 syl5eq 
 |-  ( i e. _om -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , (/) , y ) ) , Pred ( R , (/) , X ) ) |` _om ) ` i ) = (/) )
31 30 iuneq2i 
 |-  U_ i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , (/) , y ) ) , Pred ( R , (/) , X ) ) |` _om ) ` i ) = U_ i e. _om (/)
32 iun0 
 |-  U_ i e. _om (/) = (/)
33 1 31 32 3eqtri 
 |-  TrPred ( R , (/) , X ) = (/)