Metamath Proof Explorer


Theorem trpredpred

Description: Assuming it is a set, the predecessor class is a subset of the class of transitive predecessors. (Contributed by Scott Fenton, 18-Feb-2011)

Ref Expression
Assertion trpredpred Pred R A X B Pred R A X TrPred R A X

Proof

Step Hyp Ref Expression
1 fr0g Pred R A X B rec a V y a Pred R A y Pred R A X ω = Pred R A X
2 frfnom rec a V y a Pred R A y Pred R A X ω Fn ω
3 peano1 ω
4 fnbrfvb rec a V y a Pred R A y Pred R A X ω Fn ω ω rec a V y a Pred R A y Pred R A X ω = Pred R A X rec a V y a Pred R A y Pred R A X ω Pred R A X
5 2 3 4 mp2an rec a V y a Pred R A y Pred R A X ω = Pred R A X rec a V y a Pred R A y Pred R A X ω Pred R A X
6 1 5 sylib Pred R A X B rec a V y a Pred R A y Pred R A X ω Pred R A X
7 0ex V
8 breq1 z = z rec a V y a Pred R A y Pred R A X ω Pred R A X rec a V y a Pred R A y Pred R A X ω Pred R A X
9 7 8 spcev rec a V y a Pred R A y Pred R A X ω Pred R A X z z rec a V y a Pred R A y Pred R A X ω Pred R A X
10 6 9 syl Pred R A X B z z rec a V y a Pred R A y Pred R A X ω Pred R A X
11 elrng Pred R A X B Pred R A X ran rec a V y a Pred R A y Pred R A X ω z z rec a V y a Pred R A y Pred R A X ω Pred R A X
12 10 11 mpbird Pred R A X B Pred R A X ran rec a V y a Pred R A y Pred R A X ω
13 elssuni Pred R A X ran rec a V y a Pred R A y Pred R A X ω Pred R A X ran rec a V y a Pred R A y Pred R A X ω
14 12 13 syl Pred R A X B Pred R A X ran rec a V y a Pred R A y Pred R A X ω
15 df-trpred TrPred R A X = ran rec a V y a Pred R A y Pred R A X ω
16 14 15 sseqtrrdi Pred R A X B Pred R A X TrPred R A X