Theorem briunov2uz

Description: Two classes related by 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 two classes are related by that operator value. The index set N is restricted to an upper range of integers. (Contributed by RP, 2-Jun-2020)

	Ref	Expression
Hypothesis	briunov2uz.def	⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) )
Assertion	briunov2uz	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑋 ( 𝐶 ‘ 𝑅 ) 𝑌 ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ( 𝑅 ↑ 𝑛 ) 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		briunov2uz.def	⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) )
2		simpr	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 = ( ℤ≥ ‘ 𝑀 ) )
3		fvex	⊢ ( ℤ≥ ‘ 𝑀 ) ∈ V
4	2 3	eqeltrdi	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → 𝑁 ∈ V )
5	1	briunov2	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ V ) → ( 𝑋 ( 𝐶 ‘ 𝑅 ) 𝑌 ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ( 𝑅 ↑ 𝑛 ) 𝑌 ) )
6	4 5	syldan	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 = ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑋 ( 𝐶 ‘ 𝑅 ) 𝑌 ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ( 𝑅 ↑ 𝑛 ) 𝑌 ) )