opidonOLD

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) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		opidonOLD.1	$⊢ X = dom dom G$
2		inss1	$⊢ Magma \cap ExId \subseteq Magma$
3	2	sseli	$⊢ G \in (Magma \cap ExId) \to G \in Magma$
4	1	ismgmOLD	$⊢ G \in Magma \to (G \in Magma \leftrightarrow G : X \times X ⟶ X)$
5	4	ibi	$⊢ G \in Magma \to G : X \times X ⟶ X$
6	3 5	syl	$⊢ G \in (Magma \cap ExId) \to G : X \times X ⟶ X$
7		inss2	$⊢ Magma \cap ExId \subseteq ExId$
8	7	sseli	$⊢ G \in (Magma \cap ExId) \to G \in ExId$
9	1	isexid	$⊢ G \in ExId \to (G \in ExId \leftrightarrow \exists u \in X \forall x \in X (u G x = x \land x G u = x))$
10	9	biimpd	$⊢ G \in ExId \to (G \in ExId \to \exists u \in X \forall x \in X (u G x = x \land x G u = x))$
11	8 8 10	sylc	$⊢ G \in (Magma \cap ExId) \to \exists u \in X \forall x \in X (u G x = x \land x G u = x)$
12		simpl	$⊢ (u G x = x \land x G u = x) \to u G x = x$
13	12	ralimi	$⊢ \forall x \in X (u G x = x \land x G u = x) \to \forall x \in X u G x = x$
14		oveq2	$⊢ x = y \to u G x = u G y$
15		id	$⊢ x = y \to x = y$
16	14 15	eqeq12d	$⊢ x = y \to (u G x = x \leftrightarrow u G y = y)$
17	16	rspcv	$⊢ y \in X \to (\forall x \in X u G x = x \to u G y = y)$
18		eqcom	$⊢ y = u G x \leftrightarrow u G x = y$
19	14	eqeq1d	$⊢ x = y \to (u G x = y \leftrightarrow u G y = y)$
20	18 19	syl5bb	$⊢ x = y \to (y = u G x \leftrightarrow u G y = y)$
21	20	rspcev	$⊢ (y \in X \land u G y = y) \to \exists x \in X y = u G x$
22	21	ex	$⊢ y \in X \to (u G y = y \to \exists x \in X y = u G x)$
23	17 22	syld	$⊢ y \in X \to (\forall x \in X u G x = x \to \exists x \in X y = u G x)$
24	13 23	syl5	$⊢ y \in X \to (\forall x \in X (u G x = x \land x G u = x) \to \exists x \in X y = u G x)$
25	24	reximdv	$⊢ y \in X \to (\exists u \in X \forall x \in X (u G x = x \land x G u = x) \to \exists u \in X \exists x \in X y = u G x)$
26	25	impcom	$⊢ (\exists u \in X \forall x \in X (u G x = x \land x G u = x) \land y \in X) \to \exists u \in X \exists x \in X y = u G x$
27	26	ralrimiva	$⊢ \exists u \in X \forall x \in X (u G x = x \land x G u = x) \to \forall y \in X \exists u \in X \exists x \in X y = u G x$
28	11 27	syl	$⊢ G \in (Magma \cap ExId) \to \forall y \in X \exists u \in X \exists x \in X y = u G x$
29		foov	$⊢ G : X \times X \underset{onto}{⟶} X \leftrightarrow (G : X \times X ⟶ X \land \forall y \in X \exists u \in X \exists x \in X y = u G x)$
30	6 28 29	sylanbrc	$⊢ G \in (Magma \cap ExId) \to G : X \times X \underset{onto}{⟶} X$

Metamath Proof Explorer

Theorem opidonOLD

Proof