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

Metamath Proof Explorer

Definition df-dom

Description: Define the dominance relation. For an alternate definition see dfdom2 . Compare Definition of Enderton p. 145. Typical textbook definitions are derived as brdom and domen . (Contributed by NM, 28-Mar-1998)

		Ref	Expression
	Assertion	df-dom	⊢ ≼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1→ 𝑦 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdom	⊢ ≼
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3		vf	⊢ 𝑓
4	3	cv	⊢ 𝑓
5	1	cv	⊢ 𝑥
6	2	cv	⊢ 𝑦
7	5 6 4	wf1	⊢ 𝑓 : 𝑥 –1-1→ 𝑦
8	7 3	wex	⊢ ∃ 𝑓 𝑓 : 𝑥 –1-1→ 𝑦
9	8 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1→ 𝑦 }
10	0 9	wceq	⊢ ≼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1→ 𝑦 }