Theorem r1tr2

Description: The union of a cumulative hierarchy of sets at ordinal A is a subset of the hierarchy at A . JFM CLASSES1 th. 40. (Contributed by FL, 20-Apr-2011)

	Ref	Expression
Assertion	r1tr2	⊢ ∪ ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		r1tr	⊢ Tr ( 𝑅1 ‘ 𝐴 )
2		df-tr	⊢ ( Tr ( 𝑅1 ‘ 𝐴 ) ↔ ∪ ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐴 ) )
3	1 2	mpbi	⊢ ∪ ( 𝑅1 ‘ 𝐴 ) ⊆ ( 𝑅1 ‘ 𝐴 )