Theorem ituni0

Description: A zero-fold iterated union. (Contributed by Stefan O'Rear, 11-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ituni.u	⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) )
2	1	itunifval	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑈 ‘ 𝐴 ) = ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) )
3	2	fveq1d	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑈 ‘ 𝐴 ) ‘ ∅ ) = ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ ∅ ) )
4		fr0g	⊢ ( 𝐴 ∈ 𝑉 → ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ ∅ ) = 𝐴 )
5	3 4	eqtrd	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑈 ‘ 𝐴 ) ‘ ∅ ) = 𝐴 )