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

Metamath Proof Explorer

Theorem fnoprabg

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

Ref Expression
Assertion fnoprabg ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∃! 𝑧 𝜓 ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) } Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )

Proof

Step Hyp Ref Expression
1 eumo ⊢ ( ∃! 𝑧 𝜓 → ∃* 𝑧 𝜓 )
2 1 imim2i ⊢ ( ( 𝜑 → ∃! 𝑧 𝜓 ) → ( 𝜑 → ∃* 𝑧 𝜓 ) )
3 moanimv ⊢ ( ∃* 𝑧 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 → ∃* 𝑧 𝜓 ) )
4 2 3 sylibr ⊢ ( ( 𝜑 → ∃! 𝑧 𝜓 ) → ∃* 𝑧 ( 𝜑 ∧ 𝜓 ) )
5 4 2alimi ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∃! 𝑧 𝜓 ) → ∀ 𝑥 ∀ 𝑦 ∃* 𝑧 ( 𝜑 ∧ 𝜓 ) )
6 funoprabg ⊢ ( ∀ 𝑥 ∀ 𝑦 ∃* 𝑧 ( 𝜑 ∧ 𝜓 ) → Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) } )
7 5 6 syl ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∃! 𝑧 𝜓 ) → Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) } )
8 dmoprab ⊢ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝜑 ∧ 𝜓 ) }
9 nfa1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∃! 𝑧 𝜓 )
10 nfa2 ⊢ Ⅎ 𝑦 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∃! 𝑧 𝜓 )
11 simpl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 )
12 11 exlimiv ⊢ ( ∃ 𝑧 ( 𝜑 ∧ 𝜓 ) → 𝜑 )
13 euex ⊢ ( ∃! 𝑧 𝜓 → ∃ 𝑧 𝜓 )
14 13 imim2i ⊢ ( ( 𝜑 → ∃! 𝑧 𝜓 ) → ( 𝜑 → ∃ 𝑧 𝜓 ) )
15 14 ancld ⊢ ( ( 𝜑 → ∃! 𝑧 𝜓 ) → ( 𝜑 → ( 𝜑 ∧ ∃ 𝑧 𝜓 ) ) )
16 19.42v ⊢ ( ∃ 𝑧 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∃ 𝑧 𝜓 ) )
17 15 16 imbitrrdi ⊢ ( ( 𝜑 → ∃! 𝑧 𝜓 ) → ( 𝜑 → ∃ 𝑧 ( 𝜑 ∧ 𝜓 ) ) )
18 12 17 impbid2 ⊢ ( ( 𝜑 → ∃! 𝑧 𝜓 ) → ( ∃ 𝑧 ( 𝜑 ∧ 𝜓 ) ↔ 𝜑 ) )
19 18 sps ⊢ ( ∀ 𝑦 ( 𝜑 → ∃! 𝑧 𝜓 ) → ( ∃ 𝑧 ( 𝜑 ∧ 𝜓 ) ↔ 𝜑 ) )
20 19 sps ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∃! 𝑧 𝜓 ) → ( ∃ 𝑧 ( 𝜑 ∧ 𝜓 ) ↔ 𝜑 ) )
21 9 10 20 opabbid ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∃! 𝑧 𝜓 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝜑 ∧ 𝜓 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
22 8 21 eqtrid ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∃! 𝑧 𝜓 ) → dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
23 df-fn ⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) } Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ( Fun { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) } ∧ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) )
24 7 22 23 sylanbrc ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∃! 𝑧 𝜓 ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) } Fn { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )