Metamath Proof Explorer


Theorem trpredex

Description: The transitive predecessors under a relation form a set.

This is the first theorem in the transitive predecessor series that requires the axiom of infinity. (Contributed by Scott Fenton, 18-Feb-2011)

Ref Expression
Assertion trpredex TrPred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V

Proof

Step Hyp Ref Expression
1 df-trpred TrPred ( 𝑅 , 𝐴 , 𝑋 ) = ran ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω )
2 frfnom ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Fn ω
3 omex ω ∈ V
4 fnex ( ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Fn ω ∧ ω ∈ V ) → ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ∈ V )
5 2 3 4 mp2an ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ∈ V
6 5 rnex ran ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ∈ V
7 6 uniex ran ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ∈ V
8 1 7 eqeltri TrPred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V