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

Metamath Proof Explorer

Theorem enssdomOLD

Description: Obsolete version of enssdom as of 10-Feb-2026. (Contributed by NM, 31-Mar-1998) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	enssdomOLD	$⊢ \approx \subseteq ≼$

Proof

Step	Hyp	Ref	Expression
1		relen	$⊢ Rel \approx$
2		f1of1	$⊢ f : x \underset{1-1 onto}{⟶} y \to f : x \underset{1-1}{⟶} y$
3	2	eximi	$⊢ \exists f f : x \underset{1-1 onto}{⟶} y \to \exists f f : x \underset{1-1}{⟶} y$
4		opabidw	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| \exists f f : x \underset{1-1 onto}{⟶} y\} \leftrightarrow \exists f f : x \underset{1-1 onto}{⟶} y$
5		opabidw	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| \exists f f : x \underset{1-1}{⟶} y\} \leftrightarrow \exists f f : x \underset{1-1}{⟶} y$
6	3 4 5	3imtr4i	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| \exists f f : x \underset{1-1 onto}{⟶} y\} \to ⟨x, y⟩ \in \{⟨x, y⟩ \| \exists f f : x \underset{1-1}{⟶} y\}$
7		df-en	$⊢ \approx = \{⟨x, y⟩ \| \exists f f : x \underset{1-1 onto}{⟶} y\}$
8	7	eleq2i	$⊢ ⟨x, y⟩ \in \approx \leftrightarrow ⟨x, y⟩ \in \{⟨x, y⟩ \| \exists f f : x \underset{1-1 onto}{⟶} y\}$
9		df-dom	$⊢ ≼ = \{⟨x, y⟩ \| \exists f f : x \underset{1-1}{⟶} y\}$
10	9	eleq2i	$⊢ ⟨x, y⟩ \in ≼ \leftrightarrow ⟨x, y⟩ \in \{⟨x, y⟩ \| \exists f f : x \underset{1-1}{⟶} y\}$
11	6 8 10	3imtr4i	$⊢ ⟨x, y⟩ \in \approx \to ⟨x, y⟩ \in ≼$
12	1 11	relssi	$⊢ \approx \subseteq ≼$