This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )