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

Metamath Proof Explorer

Theorem oprabex

Description: Existence of an operation class abstraction. (Contributed by NM, 19-Oct-2004)

Ref Expression
Hypotheses oprabex.1 ⊢ 𝐴 ∈ V
oprabex.2 ⊢ 𝐵 ∈ V
oprabex.3 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃* 𝑧 𝜑 )
oprabex.4 ⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) }
Assertion oprabex 𝐹 ∈ V

Proof

Step Hyp Ref Expression
1 oprabex.1 ⊢ 𝐴 ∈ V
2 oprabex.2 ⊢ 𝐵 ∈ V
3 oprabex.3 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃* 𝑧 𝜑 )
4 oprabex.4 ⊢ 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) }
5 moanimv ⊢ ( ∃* 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃* 𝑧 𝜑 ) )
6 3 5 mpbir ⊢ ∃* 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 )
7 6 funoprab ⊢ Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) }
8 1 2 xpex ⊢ ( 𝐴 × 𝐵 ) ∈ V
9 dmoprabss ⊢ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ⊆ ( 𝐴 × 𝐵 )
10 8 9 ssexi ⊢ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ∈ V
11 funex ⊢ ( ( Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ∧ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ∈ V ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ∈ V )
12 7 10 11 mp2an ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) } ∈ V
13 4 12 eqeltri ⊢ 𝐹 ∈ V