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 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )