Metamath Proof Explorer


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 ( 𝐴𝑉 → ( ( 𝑈𝐴 ) ‘ ∅ ) = 𝐴 )