Metamath Proof Explorer

Theorem eliunov2

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. Generalized from dfrtrclrec2 . (Contributed by RP, 1-Jun-2020)

Ref Expression
Hypothesis mptiunov2.def ⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) )
Assertion eliunov2 ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑋 ∈ ( 𝐶 ‘ 𝑅 ) ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ∈ ( 𝑅 ↑ 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 mptiunov2.def ⊢ 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) )
2 eqid ⊢ ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) )
3 oveq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 ↑ 𝑛 ) = ( 𝑅 ↑ 𝑛 ) )
4 3 iuneq2d ⊢ ( 𝑟 = 𝑅 → ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) = ∪ 𝑛 ∈ 𝑁 ( 𝑅 ↑ 𝑛 ) )
5 elex ⊢ ( 𝑅 ∈ 𝑈 → 𝑅 ∈ V )
6 5 adantr ⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ) → 𝑅 ∈ V )
7 simpr ⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ) → 𝑁 ∈ 𝑉 )
8 ovex ⊢ ( 𝑅 ↑ 𝑛 ) ∈ V
9 8 rgenw ⊢ ∀ 𝑛 ∈ 𝑁 ( 𝑅 ↑ 𝑛 ) ∈ V
10 iunexg ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ∀ 𝑛 ∈ 𝑁 ( 𝑅 ↑ 𝑛 ) ∈ V ) → ∪ 𝑛 ∈ 𝑁 ( 𝑅 ↑ 𝑛 ) ∈ V )
11 7 9 10 sylancl ⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ) → ∪ 𝑛 ∈ 𝑁 ( 𝑅 ↑ 𝑛 ) ∈ V )
12 2 4 6 11 fvmptd3 ⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) ‘ 𝑅 ) = ∪ 𝑛 ∈ 𝑁 ( 𝑅 ↑ 𝑛 ) )
13 eleq2 ⊢ ( ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) ‘ 𝑅 ) = ∪ 𝑛 ∈ 𝑁 ( 𝑅 ↑ 𝑛 ) → ( 𝑋 ∈ ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) ‘ 𝑅 ) ↔ 𝑋 ∈ ∪ 𝑛 ∈ 𝑁 ( 𝑅 ↑ 𝑛 ) ) )
14 eliun ⊢ ( 𝑋 ∈ ∪ 𝑛 ∈ 𝑁 ( 𝑅 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ∈ ( 𝑅 ↑ 𝑛 ) )
15 14 a1i ⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑋 ∈ ∪ 𝑛 ∈ 𝑁 ( 𝑅 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ∈ ( 𝑅 ↑ 𝑛 ) ) )
16 13 15 sylan9bb ⊢ ( ( ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) ‘ 𝑅 ) = ∪ 𝑛 ∈ 𝑁 ( 𝑅 ↑ 𝑛 ) ∧ ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ) ) → ( 𝑋 ∈ ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) ‘ 𝑅 ) ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ∈ ( 𝑅 ↑ 𝑛 ) ) )
17 12 16 mpancom ⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑋 ∈ ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) ‘ 𝑅 ) ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ∈ ( 𝑅 ↑ 𝑛 ) ) )
18 fveq1 ⊢ ( 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) → ( 𝐶 ‘ 𝑅 ) = ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) ‘ 𝑅 ) )
19 18 eleq2d ⊢ ( 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) → ( 𝑋 ∈ ( 𝐶 ‘ 𝑅 ) ↔ 𝑋 ∈ ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) ‘ 𝑅 ) ) )
20 19 bibi1d ⊢ ( 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) → ( ( 𝑋 ∈ ( 𝐶 ‘ 𝑅 ) ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ∈ ( 𝑅 ↑ 𝑛 ) ) ↔ ( 𝑋 ∈ ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) ‘ 𝑅 ) ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ∈ ( 𝑅 ↑ 𝑛 ) ) ) )
21 20 imbi2d ⊢ ( 𝐶 = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) → ( ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑋 ∈ ( 𝐶 ‘ 𝑅 ) ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ∈ ( 𝑅 ↑ 𝑛 ) ) ) ↔ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑋 ∈ ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) ‘ 𝑅 ) ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ∈ ( 𝑅 ↑ 𝑛 ) ) ) ) )
22 1 21 ax-mp ⊢ ( ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑋 ∈ ( 𝐶 ‘ 𝑅 ) ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ∈ ( 𝑅 ↑ 𝑛 ) ) ) ↔ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑋 ∈ ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 ( 𝑟 ↑ 𝑛 ) ) ‘ 𝑅 ) ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ∈ ( 𝑅 ↑ 𝑛 ) ) ) )
23 17 22 mpbir ⊢ ( ( 𝑅 ∈ 𝑈 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑋 ∈ ( 𝐶 ‘ 𝑅 ) ↔ ∃ 𝑛 ∈ 𝑁 𝑋 ∈ ( 𝑅 ↑ 𝑛 ) ) )