Theorem mpoxopn0yelv

Description: If there is an element of the value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, then the second argument is an element of the first component of the first argument. (Contributed by Alexander van der Vekens, 10-Oct-2017)

	Ref	Expression
Hypothesis	mpoxopn0yelv.f	⊢ 𝐹 = ( 𝑥 ∈ V , 𝑦 ∈ ( 1st ‘ 𝑥 ) ↦ 𝐶 )
Assertion	mpoxopn0yelv	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑁 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) → 𝐾 ∈ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		mpoxopn0yelv.f	⊢ 𝐹 = ( 𝑥 ∈ V , 𝑦 ∈ ( 1st ‘ 𝑥 ) ↦ 𝐶 )
2	1	dmmpossx	⊢ dom 𝐹 ⊆ ∪ 𝑥 ∈ V ( { 𝑥 } × ( 1st ‘ 𝑥 ) )
3		elfvdm	⊢ ( 𝑁 ∈ ( 𝐹 ‘ ⟨ ⟨ 𝑉 , 𝑊 ⟩ , 𝐾 ⟩ ) → ⟨ ⟨ 𝑉 , 𝑊 ⟩ , 𝐾 ⟩ ∈ dom 𝐹 )
4		df-ov	⊢ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) = ( 𝐹 ‘ ⟨ ⟨ 𝑉 , 𝑊 ⟩ , 𝐾 ⟩ )
5	3 4	eleq2s	⊢ ( 𝑁 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) → ⟨ ⟨ 𝑉 , 𝑊 ⟩ , 𝐾 ⟩ ∈ dom 𝐹 )
6	2 5	sselid	⊢ ( 𝑁 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) → ⟨ ⟨ 𝑉 , 𝑊 ⟩ , 𝐾 ⟩ ∈ ∪ 𝑥 ∈ V ( { 𝑥 } × ( 1st ‘ 𝑥 ) ) )
7		fveq2	⊢ ( 𝑥 = ⟨ 𝑉 , 𝑊 ⟩ → ( 1st ‘ 𝑥 ) = ( 1st ‘ ⟨ 𝑉 , 𝑊 ⟩ ) )
8	7	opeliunxp2	⊢ ( ⟨ ⟨ 𝑉 , 𝑊 ⟩ , 𝐾 ⟩ ∈ ∪ 𝑥 ∈ V ( { 𝑥 } × ( 1st ‘ 𝑥 ) ) ↔ ( ⟨ 𝑉 , 𝑊 ⟩ ∈ V ∧ 𝐾 ∈ ( 1st ‘ ⟨ 𝑉 , 𝑊 ⟩ ) ) )
9	8	simprbi	⊢ ( ⟨ ⟨ 𝑉 , 𝑊 ⟩ , 𝐾 ⟩ ∈ ∪ 𝑥 ∈ V ( { 𝑥 } × ( 1st ‘ 𝑥 ) ) → 𝐾 ∈ ( 1st ‘ ⟨ 𝑉 , 𝑊 ⟩ ) )
10	6 9	syl	⊢ ( 𝑁 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) → 𝐾 ∈ ( 1st ‘ ⟨ 𝑉 , 𝑊 ⟩ ) )
11		op1stg	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 1st ‘ ⟨ 𝑉 , 𝑊 ⟩ ) = 𝑉 )
12	11	eleq2d	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝐾 ∈ ( 1st ‘ ⟨ 𝑉 , 𝑊 ⟩ ) ↔ 𝐾 ∈ 𝑉 ) )
13	10 12	syl5ib	⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝑁 ∈ ( ⟨ 𝑉 , 𝑊 ⟩ 𝐹 𝐾 ) → 𝐾 ∈ 𝑉 ) )