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

Metamath Proof Explorer

Theorem brdomg

Description: Dominance relation. (Contributed by NM, 15-Jun-1998) Extract brdom2g as an intermediate result. (Revised by BTernaryTau, 29-Nov-2024)

		Ref	Expression
	Assertion	brdomg	$⊢ B \in C \to (A ≼ B \leftrightarrow \exists f f : A \underset{1-1}{⟶} B)$

Proof

Step	Hyp	Ref	Expression
1		brdom2g	$⊢ (A \in V \land B \in C) \to (A ≼ B \leftrightarrow \exists f f : A \underset{1-1}{⟶} B)$
2	1	ex	$⊢ A \in V \to (B \in C \to (A ≼ B \leftrightarrow \exists f f : A \underset{1-1}{⟶} B))$
3		reldom	$⊢ Rel ≼$
4	3	brrelex1i	$⊢ A ≼ B \to A \in V$
5		f1f	$⊢ f : A \underset{1-1}{⟶} B \to f : A ⟶ B$
6		fdm	$⊢ f : A ⟶ B \to dom f = A$
7		vex	$⊢ f \in V$
8	7	dmex	$⊢ dom f \in V$
9	6 8	eqeltrrdi	$⊢ f : A ⟶ B \to A \in V$
10	5 9	syl	$⊢ f : A \underset{1-1}{⟶} B \to A \in V$
11	10	exlimiv	$⊢ \exists f f : A \underset{1-1}{⟶} B \to A \in V$
12	4 11	pm5.21ni	$⊢ \neg A \in V \to (A ≼ B \leftrightarrow \exists f f : A \underset{1-1}{⟶} B)$
13	12	a1d	$⊢ \neg A \in V \to (B \in C \to (A ≼ B \leftrightarrow \exists f f : A \underset{1-1}{⟶} B))$
14	2 13	pm2.61i	$⊢ B \in C \to (A ≼ B \leftrightarrow \exists f f : A \underset{1-1}{⟶} B)$