Metamath Proof Explorer


Theorem dftrpred2

Description: A definition of the transitive predecessors of a class in terms of indexed union. (Contributed by Scott Fenton, 28-Apr-2012)

Ref Expression
Assertion dftrpred2 TrPred ( 𝑅 , 𝐴 , 𝑋 ) = 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 )

Proof

Step Hyp Ref Expression
1 df-trpred TrPred ( 𝑅 , 𝐴 , 𝑋 ) = ran ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω )
2 frfnom ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Fn ω
3 fniunfv ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) Fn ω → 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) = ran ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) )
4 2 3 ax-mp 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) = ran ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω )
5 1 4 eqtr4i TrPred ( 𝑅 , 𝐴 , 𝑋 ) = 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ 𝑦𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 )