Description: A zero-fold iterated union. (Contributed by Stefan O'Rear, 11-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ituni.u | ⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) ) | |
Assertion | ituni0 | ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑈 ‘ 𝐴 ) ‘ ∅ ) = 𝐴 ) |
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 | ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑈 ‘ 𝐴 ) ‘ ∅ ) = 𝐴 ) |