Metamath Proof Explorer

Theorem opidon2OLD

Description: Obsolete version of mndpfo as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Hypothesis	opidon2OLD.1	$⊢ X = ran G$
	Assertion	opidon2OLD	$⊢ G \in (Magma \cap ExId) \to G : X \times X \underset{onto}{⟶} X$

Proof

Step	Hyp	Ref	Expression
1		opidon2OLD.1	$⊢ X = ran G$
2		eqid	$⊢ dom dom G = dom dom G$
3	2	opidonOLD	$⊢ G \in (Magma \cap ExId) \to G : dom dom G \times dom dom G \underset{onto}{⟶} dom dom G$
4		forn	$⊢ G : dom dom G \times dom dom G \underset{onto}{⟶} dom dom G \to ran G = dom dom G$
5	1 4	eqtr2id	$⊢ G : dom dom G \times dom dom G \underset{onto}{⟶} dom dom G \to dom dom G = X$
6		xpeq12	$⊢ (dom dom G = X \land dom dom G = X) \to dom dom G \times dom dom G = X \times X$
7	6	anidms	$⊢ dom dom G = X \to dom dom G \times dom dom G = X \times X$
8		foeq2	$⊢ dom dom G \times dom dom G = X \times X \to (G : dom dom G \times dom dom G \underset{onto}{⟶} dom dom G \leftrightarrow G : X \times X \underset{onto}{⟶} dom dom G)$
9	7 8	syl	$⊢ dom dom G = X \to (G : dom dom G \times dom dom G \underset{onto}{⟶} dom dom G \leftrightarrow G : X \times X \underset{onto}{⟶} dom dom G)$
10		foeq3	$⊢ dom dom G = X \to (G : X \times X \underset{onto}{⟶} dom dom G \leftrightarrow G : X \times X \underset{onto}{⟶} X)$
11	9 10	bitrd	$⊢ dom dom G = X \to (G : dom dom G \times dom dom G \underset{onto}{⟶} dom dom G \leftrightarrow G : X \times X \underset{onto}{⟶} X)$
12	11	biimpd	$⊢ dom dom G = X \to (G : dom dom G \times dom dom G \underset{onto}{⟶} dom dom G \to G : X \times X \underset{onto}{⟶} X)$
13	5 12	mpcom	$⊢ G : dom dom G \times dom dom G \underset{onto}{⟶} dom dom G \to G : X \times X \underset{onto}{⟶} X$
14	3 13	syl	$⊢ G \in (Magma \cap ExId) \to G : X \times X \underset{onto}{⟶} X$