Theorem ov2ssiunov2

Description: Any particular operator value is the subset of the index union over a set of operator values. Generalized from rtrclreclem1 and rtrclreclem2 . (Contributed by RP, 4-Jun-2020)

	Ref	Expression
Hypothesis	ov2ssiunov2.def	⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) )
Assertion	ov2ssiunov2	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ∧ 𝑀 ∈ 𝑁 ) → ( 𝑅 ↑ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		ov2ssiunov2.def	⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) )
2		simp3	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ∧ 𝑀 ∈ 𝑁 ) → 𝑀 ∈ 𝑁 )
3		simpr	⊢ ( ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ∧ 𝑀 ∈ 𝑁 ) ∧ 𝑛 = 𝑀 ) → 𝑛 = 𝑀 )
4	3	oveq2d	⊢ ( ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ∧ 𝑀 ∈ 𝑁 ) ∧ 𝑛 = 𝑀 ) → ( 𝑅 ↑ 𝑛 ) = ( 𝑅 ↑ 𝑀 ) )
5	4	eleq2d	⊢ ( ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ∧ 𝑀 ∈ 𝑁 ) ∧ 𝑛 = 𝑀 ) → ( 𝑥 ∈ ( 𝑅 ↑ 𝑛 ) ↔ 𝑥 ∈ ( 𝑅 ↑ 𝑀 ) ) )
6	2 5	rspcedv	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ∧ 𝑀 ∈ 𝑁 ) → ( 𝑥 ∈ ( 𝑅 ↑ 𝑀 ) → ∃ 𝑛 ∈ 𝑁 𝑥 ∈ ( 𝑅 ↑ 𝑛 ) ) )
7	1	eliunov2	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑥 ∈ ( 𝐶 ‘ 𝑅 ) ↔ ∃ 𝑛 ∈ 𝑁 𝑥 ∈ ( 𝑅 ↑ 𝑛 ) ) )
8	7	biimprd	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ) → ( ∃ 𝑛 ∈ 𝑁 𝑥 ∈ ( 𝑅 ↑ 𝑛 ) → 𝑥 ∈ ( 𝐶 ‘ 𝑅 ) ) )
9	8	3adant3	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ∧ 𝑀 ∈ 𝑁 ) → ( ∃ 𝑛 ∈ 𝑁 𝑥 ∈ ( 𝑅 ↑ 𝑛 ) → 𝑥 ∈ ( 𝐶 ‘ 𝑅 ) ) )
10	6 9	syld	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ∧ 𝑀 ∈ 𝑁 ) → ( 𝑥 ∈ ( 𝑅 ↑ 𝑀 ) → 𝑥 ∈ ( 𝐶 ‘ 𝑅 ) ) )
11	10	ssrdv	⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ∧ 𝑀 ∈ 𝑁 ) → ( 𝑅 ↑ 𝑀 ) ⊆ ( 𝐶 ‘ 𝑅 ) )