Theorem eltrpred

Description: A class is a transitive predecessor iff it is in some value of the underlying function. This theorem is not meant to be used directly; use trpredpred and trpredmintr instead. (Contributed by Scott Fenton, 28-Apr-2012)

	Ref	Expression
Assertion	eltrpred	⊢ ( 𝑌 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ∃ 𝑖 ∈ ω 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) )

Proof

Step	Hyp	Ref	Expression
1		dftrpred2	⊢ TrPred ( 𝑅 , 𝐴 , 𝑋 ) = ∪ 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 )
2	1	eleq2i	⊢ ( 𝑌 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑌 ∈ ∪ 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) )
3		eliun	⊢ ( 𝑌 ∈ ∪ 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ ω 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) )
4	2 3	bitri	⊢ ( 𝑌 ∈ TrPred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ∃ 𝑖 ∈ ω 𝑌 ∈ ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) )