Theorem brovex

Description: A binary relation of the value of an operation given by the maps-to notation. (Contributed by Alexander van der Vekens, 21-Oct-2017)

	Ref	Expression
Hypotheses	brovex.1	⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ 𝐶 )
	brovex.2	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → Rel ( 𝑉 𝑂 𝐸 ) )
Assertion	brovex	⊢ ( 𝐹 ( 𝑉 𝑂 𝐸 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )

Proof

Step	Hyp	Ref	Expression
1		brovex.1	⊢ 𝑂 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ 𝐶 )
2		brovex.2	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → Rel ( 𝑉 𝑂 𝐸 ) )
3		df-br	⊢ ( 𝐹 ( 𝑉 𝑂 𝐸 ) 𝑃 ↔ ⟨ 𝐹 , 𝑃 ⟩ ∈ ( 𝑉 𝑂 𝐸 ) )
4		ne0i	⊢ ( ⟨ 𝐹 , 𝑃 ⟩ ∈ ( 𝑉 𝑂 𝐸 ) → ( 𝑉 𝑂 𝐸 ) ≠ ∅ )
5	1	mpondm0	⊢ ( ¬ ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( 𝑉 𝑂 𝐸 ) = ∅ )
6	5	necon1ai	⊢ ( ( 𝑉 𝑂 𝐸 ) ≠ ∅ → ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) )
7		brrelex12	⊢ ( ( Rel ( 𝑉 𝑂 𝐸 ) ∧ 𝐹 ( 𝑉 𝑂 𝐸 ) 𝑃 ) → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
8	2 7	sylan	⊢ ( ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ 𝐹 ( 𝑉 𝑂 𝐸 ) 𝑃 ) → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
9		id	⊢ ( ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
10	8 9	syldan	⊢ ( ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ 𝐹 ( 𝑉 𝑂 𝐸 ) 𝑃 ) → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
11	10	ex	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( 𝐹 ( 𝑉 𝑂 𝐸 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) )
12	4 6 11	3syl	⊢ ( ⟨ 𝐹 , 𝑃 ⟩ ∈ ( 𝑉 𝑂 𝐸 ) → ( 𝐹 ( 𝑉 𝑂 𝐸 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) )
13	3 12	sylbi	⊢ ( 𝐹 ( 𝑉 𝑂 𝐸 ) 𝑃 → ( 𝐹 ( 𝑉 𝑂 𝐸 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) ) )
14	13	pm2.43i	⊢ ( 𝐹 ( 𝑉 𝑂 𝐸 ) 𝑃 → ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )