Description: Membership in the indexed union over operator values where the index varies the second input is equivalent to the existence of at least one index such that the element is a member of that operator value. The index set N is restricted to an upper range of integers. (Contributed by RP, 2-Jun-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | eliunov2uz.def | ⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) | |
| Assertion | eliunov2uz | ⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑋 ∈ ( 𝐶 ‘ 𝑅 ) ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ∈ ( 𝑅 ↑ 𝑛 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eliunov2uz.def | ⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) | |
| 2 | simpr | ⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) | |
| 3 | fvex | ⊢ ( ℤ≥ ‘ 𝑀 ) ∈ V | |
| 4 | 2 3 | eqeltrdi | ⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 ∈ V ) |
| 5 | 1 | eliunov2 | ⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ V ) → ( 𝑋 ∈ ( 𝐶 ‘ 𝑅 ) ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ∈ ( 𝑅 ↑ 𝑛 ) ) ) |
| 6 | 4 5 | syldan | ⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑋 ∈ ( 𝐶 ‘ 𝑅 ) ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ∈ ( 𝑅 ↑ 𝑛 ) ) ) |