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

Metamath Proof Explorer

Theorem oprabexd

Description: Existence of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by AV, 9-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 oprabexd.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 oprabexd.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 oprabexd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑧 𝜓 )
4 oprabexd.4 ⊢ ( 𝜑 → 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) } )
5 3 ex ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃* 𝑧 𝜓 ) )
6 moanimv ⊢ ( ∃* 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃* 𝑧 𝜓 ) )
7 5 6 sylibr ⊢ ( 𝜑 → ∃* 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) )
8 7 alrimivv ⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 ∃* 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) )
9 funoprabg ⊢ ( ∀ 𝑥 ∀ 𝑦 ∃* 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) → Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) } )
10 8 9 syl ⊢ ( 𝜑 → Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) } )
11 dmoprabss ⊢ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) } ⊆ ( 𝐴 × 𝐵 )
12 1 2 xpexd ⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) ∈ V )
13 ssexg ⊢ ( ( dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) } ⊆ ( 𝐴 × 𝐵 ) ∧ ( 𝐴 × 𝐵 ) ∈ V ) → dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) } ∈ V )
14 11 12 13 sylancr ⊢ ( 𝜑 → dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) } ∈ V )
15 funex ⊢ ( ( Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) } ∧ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) } ∈ V ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) } ∈ V )
16 10 14 15 syl2anc ⊢ ( 𝜑 → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) } ∈ V )
17 4 16 eqeltrd ⊢ ( 𝜑 → 𝐹 ∈ V )