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

Metamath Proof Explorer

Theorem brdom2g

Description: Dominance relation. This variation of brdomg does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998) Extract from a subproof of brdomg . (Revised by BTernaryTau, 29-Nov-2024)

		Ref	Expression
	Assertion	brdom2g	$⊢ (A \in V \land B \in W) \to (A ≼ B \leftrightarrow \exists f f : A \underset{1-1}{⟶} B)$

Proof

Step	Hyp	Ref	Expression
1		f1eq2	$⊢ x = A \to (f : x \underset{1-1}{⟶} y \leftrightarrow f : A \underset{1-1}{⟶} y)$
2	1	exbidv	$⊢ x = A \to (\exists f f : x \underset{1-1}{⟶} y \leftrightarrow \exists f f : A \underset{1-1}{⟶} y)$
3		f1eq3	$⊢ y = B \to (f : A \underset{1-1}{⟶} y \leftrightarrow f : A \underset{1-1}{⟶} B)$
4	3	exbidv	$⊢ y = B \to (\exists f f : A \underset{1-1}{⟶} y \leftrightarrow \exists f f : A \underset{1-1}{⟶} B)$
5		df-dom	$⊢ ≼ = \{⟨x, y⟩ \| \exists f f : x \underset{1-1}{⟶} y\}$
6	2 4 5	brabg	$⊢ (A \in V \land B \in W) \to (A ≼ B \leftrightarrow \exists f f : A \underset{1-1}{⟶} B)$