tgjustr

Description: Given any equivalence relation R , one can define a function f such that all elements of an equivalence classe of R have the same image by f . (Contributed by Thierry Arnoux, 25-Jan-2023)

		Ref	Expression
	Assertion	tgjustr	$⊢ (A \in V \land R Er A) \to \exists f (f Fn A \land \forall x \in A \forall y \in A (x R y \leftrightarrow f (x) = f (y)))$

Proof

Step	Hyp	Ref	Expression
1		erex	$⊢ R Er A \to (A \in V \to R \in V)$
2	1	impcom	$⊢ (A \in V \land R Er A) \to R \in V$
3		ecexg	$⊢ R \in V \to [u] R \in V$
4	2 3	syl	$⊢ (A \in V \land R Er A) \to [u] R \in V$
5	4	adantr	$⊢ ((A \in V \land R Er A) \land u \in A) \to [u] R \in V$
6	5	ralrimiva	$⊢ (A \in V \land R Er A) \to \forall u \in A [u] R \in V$
7		eqid	$⊢ (u \in A ⟼ [u] R) = (u \in A ⟼ [u] R)$
8	7	fnmpt	$⊢ \forall u \in A [u] R \in V \to (u \in A ⟼ [u] R) Fn A$
9	6 8	syl	$⊢ (A \in V \land R Er A) \to (u \in A ⟼ [u] R) Fn A$
10		simpllr	$⊢ (((A \in V \land R Er A) \land x \in A) \land y \in A) \to R Er A$
11		simpr	$⊢ ((A \in V \land R Er A) \land x \in A) \to x \in A$
12	11	adantr	$⊢ (((A \in V \land R Er A) \land x \in A) \land y \in A) \to x \in A$
13	10 12	erth	$⊢ (((A \in V \land R Er A) \land x \in A) \land y \in A) \to (x R y \leftrightarrow [x] R = [y] R)$
14		eceq1	$⊢ u = x \to [u] R = [x] R$
15		ecelqsg	$⊢ (R \in V \land x \in A) \to [x] R \in (A / R)$
16	2 15	sylan	$⊢ ((A \in V \land R Er A) \land x \in A) \to [x] R \in (A / R)$
17	7 14 11 16	fvmptd3	$⊢ ((A \in V \land R Er A) \land x \in A) \to (u \in A ⟼ [u] R) (x) = [x] R$
18	17	adantr	$⊢ (((A \in V \land R Er A) \land x \in A) \land y \in A) \to (u \in A ⟼ [u] R) (x) = [x] R$
19		eceq1	$⊢ u = y \to [u] R = [y] R$
20		simpr	$⊢ ((A \in V \land R Er A) \land y \in A) \to y \in A$
21		ecelqsg	$⊢ (R \in V \land y \in A) \to [y] R \in (A / R)$
22	2 21	sylan	$⊢ ((A \in V \land R Er A) \land y \in A) \to [y] R \in (A / R)$
23	7 19 20 22	fvmptd3	$⊢ ((A \in V \land R Er A) \land y \in A) \to (u \in A ⟼ [u] R) (y) = [y] R$
24	23	adantlr	$⊢ (((A \in V \land R Er A) \land x \in A) \land y \in A) \to (u \in A ⟼ [u] R) (y) = [y] R$
25	18 24	eqeq12d	$⊢ (((A \in V \land R Er A) \land x \in A) \land y \in A) \to ((u \in A ⟼ [u] R) (x) = (u \in A ⟼ [u] R) (y) \leftrightarrow [x] R = [y] R)$
26	13 25	bitr4d	$⊢ (((A \in V \land R Er A) \land x \in A) \land y \in A) \to (x R y \leftrightarrow (u \in A ⟼ [u] R) (x) = (u \in A ⟼ [u] R) (y))$
27	26	ralrimiva	$⊢ ((A \in V \land R Er A) \land x \in A) \to \forall y \in A (x R y \leftrightarrow (u \in A ⟼ [u] R) (x) = (u \in A ⟼ [u] R) (y))$
28	27	ralrimiva	$⊢ (A \in V \land R Er A) \to \forall x \in A \forall y \in A (x R y \leftrightarrow (u \in A ⟼ [u] R) (x) = (u \in A ⟼ [u] R) (y))$
29		mptexg	$⊢ A \in V \to (u \in A ⟼ [u] R) \in V$
30	29	adantr	$⊢ (A \in V \land R Er A) \to (u \in A ⟼ [u] R) \in V$
31		fneq1	$⊢ f = (u \in A ⟼ [u] R) \to (f Fn A \leftrightarrow (u \in A ⟼ [u] R) Fn A)$
32		simpl	$⊢ (f = (u \in A ⟼ [u] R) \land (x \in A \land y \in A)) \to f = (u \in A ⟼ [u] R)$
33	32	fveq1d	$⊢ (f = (u \in A ⟼ [u] R) \land (x \in A \land y \in A)) \to f (x) = (u \in A ⟼ [u] R) (x)$
34	32	fveq1d	$⊢ (f = (u \in A ⟼ [u] R) \land (x \in A \land y \in A)) \to f (y) = (u \in A ⟼ [u] R) (y)$
35	33 34	eqeq12d	$⊢ (f = (u \in A ⟼ [u] R) \land (x \in A \land y \in A)) \to (f (x) = f (y) \leftrightarrow (u \in A ⟼ [u] R) (x) = (u \in A ⟼ [u] R) (y))$
36	35	bibi2d	$⊢ (f = (u \in A ⟼ [u] R) \land (x \in A \land y \in A)) \to ((x R y \leftrightarrow f (x) = f (y)) \leftrightarrow (x R y \leftrightarrow (u \in A ⟼ [u] R) (x) = (u \in A ⟼ [u] R) (y)))$
37	36	2ralbidva	$⊢ f = (u \in A ⟼ [u] R) \to (\forall x \in A \forall y \in A (x R y \leftrightarrow f (x) = f (y)) \leftrightarrow \forall x \in A \forall y \in A (x R y \leftrightarrow (u \in A ⟼ [u] R) (x) = (u \in A ⟼ [u] R) (y)))$
38	31 37	anbi12d	$⊢ f = (u \in A ⟼ [u] R) \to ((f Fn A \land \forall x \in A \forall y \in A (x R y \leftrightarrow f (x) = f (y))) \leftrightarrow ((u \in A ⟼ [u] R) Fn A \land \forall x \in A \forall y \in A (x R y \leftrightarrow (u \in A ⟼ [u] R) (x) = (u \in A ⟼ [u] R) (y))))$
39	38	spcegv	$⊢ (u \in A ⟼ [u] R) \in V \to (((u \in A ⟼ [u] R) Fn A \land \forall x \in A \forall y \in A (x R y \leftrightarrow (u \in A ⟼ [u] R) (x) = (u \in A ⟼ [u] R) (y))) \to \exists f (f Fn A \land \forall x \in A \forall y \in A (x R y \leftrightarrow f (x) = f (y))))$
40	30 39	syl	$⊢ (A \in V \land R Er A) \to (((u \in A ⟼ [u] R) Fn A \land \forall x \in A \forall y \in A (x R y \leftrightarrow (u \in A ⟼ [u] R) (x) = (u \in A ⟼ [u] R) (y))) \to \exists f (f Fn A \land \forall x \in A \forall y \in A (x R y \leftrightarrow f (x) = f (y))))$
41	9 28 40	mp2and	$⊢ (A \in V \land R Er A) \to \exists f (f Fn A \land \forall x \in A \forall y \in A (x R y \leftrightarrow f (x) = f (y)))$

Metamath Proof Explorer

Theorem tgjustr

Proof