Theorem itunifval

Description: Function value of iterated unions.EDITORIAL: The iterated unions and order types of ordered sets are split out here because they could conceivably be independently useful. (Contributed by Stefan O'Rear, 11-Feb-2015)

	Ref	Expression
Hypothesis	ituni.u	⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) )
Assertion	itunifval	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑈 ‘ 𝐴 ) = ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) )

Proof

Step	Hyp	Ref	Expression
1		ituni.u	⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) )
2		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
3		rdgeq2	⊢ ( 𝑥 = 𝐴 → rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) = rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) )
4	3	reseq1d	⊢ ( 𝑥 = 𝐴 → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) = ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) )
5		rdgfun	⊢ Fun rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 )
6		omex	⊢ ω ∈ V
7		resfunexg	⊢ ( ( Fun rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ∧ ω ∈ V ) → ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ∈ V )
8	5 6 7	mp2an	⊢ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ∈ V
9	4 1 8	fvmpt	⊢ ( 𝐴 ∈ V → ( 𝑈 ‘ 𝐴 ) = ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) )
10	2 9	syl	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑈 ‘ 𝐴 ) = ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) )