Theorem itunifn

Description: Functionality of the iterated union. (Contributed by Stefan O'Rear, 11-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ituni.u	⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) )
2		frfnom	⊢ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) Fn ω
3	1	itunifval	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑈 ‘ 𝐴 ) = ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) )
4	3	fneq1d	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑈 ‘ 𝐴 ) Fn ω ↔ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) Fn ω ) )
5	2 4	mpbiri	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑈 ‘ 𝐴 ) Fn ω )