Metamath Proof Explorer

Theorem fnoprabg

Description: Functionality and domain of an operation class abstraction. (Contributed by NM, 28-Aug-2007)

Ref Expression
Assertion fnoprabg ⊢ ∀ x ∀ y φ → ∃! z ψ → x y z | φ ∧ ψ Fn x y | φ

Proof

Step Hyp Ref Expression
1 eumo ⊢ ∃! z ψ → ∃* z ψ
2 1 imim2i ⊢ φ → ∃! z ψ → φ → ∃* z ψ
3 moanimv ⊢ ∃* z φ ∧ ψ ↔ φ → ∃* z ψ
4 2 3 sylibr ⊢ φ → ∃! z ψ → ∃* z φ ∧ ψ
5 4 2alimi ⊢ ∀ x ∀ y φ → ∃! z ψ → ∀ x ∀ y ∃* z φ ∧ ψ
6 funoprabg ⊢ ∀ x ∀ y ∃* z φ ∧ ψ → Fun ⁡ x y z | φ ∧ ψ
7 5 6 syl ⊢ ∀ x ∀ y φ → ∃! z ψ → Fun ⁡ x y z | φ ∧ ψ
8 dmoprab ⊢ dom ⁡ x y z | φ ∧ ψ = x y | ∃ z φ ∧ ψ
9 nfa1 ⊢ Ⅎ x ∀ x ∀ y φ → ∃! z ψ
10 nfa2 ⊢ Ⅎ y ∀ x ∀ y φ → ∃! z ψ
11 simpl ⊢ φ ∧ ψ → φ
12 11 exlimiv ⊢ ∃ z φ ∧ ψ → φ
13 euex ⊢ ∃! z ψ → ∃ z ψ
14 13 imim2i ⊢ φ → ∃! z ψ → φ → ∃ z ψ
15 14 ancld ⊢ φ → ∃! z ψ → φ → φ ∧ ∃ z ψ
16 19.42v ⊢ ∃ z φ ∧ ψ ↔ φ ∧ ∃ z ψ
17 15 16 imbitrrdi ⊢ φ → ∃! z ψ → φ → ∃ z φ ∧ ψ
18 12 17 impbid2 ⊢ φ → ∃! z ψ → ∃ z φ ∧ ψ ↔ φ
19 18 sps ⊢ ∀ y φ → ∃! z ψ → ∃ z φ ∧ ψ ↔ φ
20 19 sps ⊢ ∀ x ∀ y φ → ∃! z ψ → ∃ z φ ∧ ψ ↔ φ
21 9 10 20 opabbid ⊢ ∀ x ∀ y φ → ∃! z ψ → x y | ∃ z φ ∧ ψ = x y | φ
22 8 21 eqtrid ⊢ ∀ x ∀ y φ → ∃! z ψ → dom ⁡ x y z | φ ∧ ψ = x y | φ
23 df-fn ⊢ x y z | φ ∧ ψ Fn x y | φ ↔ Fun ⁡ x y z | φ ∧ ψ ∧ dom ⁡ x y z | φ ∧ ψ = x y | φ
24 7 22 23 sylanbrc ⊢ ∀ x ∀ y φ → ∃! z ψ → x y z | φ ∧ ψ Fn x y | φ