Theorem trpredss

Description: The transitive predecessors form a subset of the base class. (Contributed by Scott Fenton, 20-Feb-2011)

	Ref	Expression
Assertion	trpredss	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → TrPred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dftrpred2	⊢ TrPred ( 𝑅 , 𝐴 , 𝑋 ) = ∪ 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 )
2		trpredlem1	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 )
3	2	ralrimivw	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → ∀ 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 )
4		iunss	⊢ ( ∪ 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 ↔ ∀ 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 )
5	3 4	sylibr	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → ∪ 𝑖 ∈ ω ( ( rec ( ( 𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred ( 𝑅 , 𝐴 , 𝑦 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ↾ ω ) ‘ 𝑖 ) ⊆ 𝐴 )
6	1 5	eqsstrid	⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐵 → TrPred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐴 )