tgjustf

Description: Given any function F , equality of the image by F is an equivalence relation. (Contributed by Thierry Arnoux, 25-Jan-2023)

		Ref	Expression
	Assertion	tgjustf	$⊢ A \in V \to \exists r (r Er A \land \forall x \in A \forall y \in A (x r y \leftrightarrow F (x) = F (y)))$

Proof

Step	Hyp	Ref	Expression
1		relopabv	$⊢ Rel \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\}$
2		ancom	$⊢ (x \in A \land y \in A) \leftrightarrow (y \in A \land x \in A)$
3		eqcom	$⊢ F (x) = F (y) \leftrightarrow F (y) = F (x)$
4	2 3	anbi12i	$⊢ ((x \in A \land y \in A) \land F (x) = F (y)) \leftrightarrow ((y \in A \land x \in A) \land F (y) = F (x))$
5		simpl	$⊢ (u = x \land v = y) \to u = x$
6	5	fveq2d	$⊢ (u = x \land v = y) \to F (u) = F (x)$
7		simpr	$⊢ (u = x \land v = y) \to v = y$
8	7	fveq2d	$⊢ (u = x \land v = y) \to F (v) = F (y)$
9	6 8	eqeq12d	$⊢ (u = x \land v = y) \to (F (u) = F (v) \leftrightarrow F (x) = F (y))$
10		eqid	$⊢ \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} = \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\}$
11	9 10	brab2a	$⊢ x \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} y \leftrightarrow ((x \in A \land y \in A) \land F (x) = F (y))$
12		simpl	$⊢ (u = y \land v = x) \to u = y$
13	12	fveq2d	$⊢ (u = y \land v = x) \to F (u) = F (y)$
14		simpr	$⊢ (u = y \land v = x) \to v = x$
15	14	fveq2d	$⊢ (u = y \land v = x) \to F (v) = F (x)$
16	13 15	eqeq12d	$⊢ (u = y \land v = x) \to (F (u) = F (v) \leftrightarrow F (y) = F (x))$
17	16 10	brab2a	$⊢ y \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} x \leftrightarrow ((y \in A \land x \in A) \land F (y) = F (x))$
18	4 11 17	3bitr4i	$⊢ x \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} y \leftrightarrow y \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} x$
19	18	biimpi	$⊢ x \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} y \to y \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} x$
20		simplll	$⊢ (((x \in A \land y \in A) \land F (x) = F (y)) \land ((y \in A \land z \in A) \land F (y) = F (z))) \to x \in A$
21		simprlr	$⊢ (((x \in A \land y \in A) \land F (x) = F (y)) \land ((y \in A \land z \in A) \land F (y) = F (z))) \to z \in A$
22		simplr	$⊢ (((x \in A \land y \in A) \land F (x) = F (y)) \land ((y \in A \land z \in A) \land F (y) = F (z))) \to F (x) = F (y)$
23		simprr	$⊢ (((x \in A \land y \in A) \land F (x) = F (y)) \land ((y \in A \land z \in A) \land F (y) = F (z))) \to F (y) = F (z)$
24	22 23	eqtrd	$⊢ (((x \in A \land y \in A) \land F (x) = F (y)) \land ((y \in A \land z \in A) \land F (y) = F (z))) \to F (x) = F (z)$
25	20 21 24	jca31	$⊢ (((x \in A \land y \in A) \land F (x) = F (y)) \land ((y \in A \land z \in A) \land F (y) = F (z))) \to ((x \in A \land z \in A) \land F (x) = F (z))$
26		simpl	$⊢ (u = y \land v = z) \to u = y$
27	26	fveq2d	$⊢ (u = y \land v = z) \to F (u) = F (y)$
28		simpr	$⊢ (u = y \land v = z) \to v = z$
29	28	fveq2d	$⊢ (u = y \land v = z) \to F (v) = F (z)$
30	27 29	eqeq12d	$⊢ (u = y \land v = z) \to (F (u) = F (v) \leftrightarrow F (y) = F (z))$
31	30 10	brab2a	$⊢ y \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} z \leftrightarrow ((y \in A \land z \in A) \land F (y) = F (z))$
32	11 31	anbi12i	$⊢ (x \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} y \land y \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} z) \leftrightarrow (((x \in A \land y \in A) \land F (x) = F (y)) \land ((y \in A \land z \in A) \land F (y) = F (z)))$
33		simpl	$⊢ (u = x \land v = z) \to u = x$
34	33	fveq2d	$⊢ (u = x \land v = z) \to F (u) = F (x)$
35		simpr	$⊢ (u = x \land v = z) \to v = z$
36	35	fveq2d	$⊢ (u = x \land v = z) \to F (v) = F (z)$
37	34 36	eqeq12d	$⊢ (u = x \land v = z) \to (F (u) = F (v) \leftrightarrow F (x) = F (z))$
38	37 10	brab2a	$⊢ x \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} z \leftrightarrow ((x \in A \land z \in A) \land F (x) = F (z))$
39	25 32 38	3imtr4i	$⊢ (x \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} y \land y \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} z) \to x \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} z$
40		eqid	$⊢ F (x) = F (x)$
41	40	biantru	$⊢ (x \in A \land x \in A) \leftrightarrow ((x \in A \land x \in A) \land F (x) = F (x))$
42		pm4.24	$⊢ x \in A \leftrightarrow (x \in A \land x \in A)$
43		simpl	$⊢ (u = x \land v = x) \to u = x$
44	43	fveq2d	$⊢ (u = x \land v = x) \to F (u) = F (x)$
45		simpr	$⊢ (u = x \land v = x) \to v = x$
46	45	fveq2d	$⊢ (u = x \land v = x) \to F (v) = F (x)$
47	44 46	eqeq12d	$⊢ (u = x \land v = x) \to (F (u) = F (v) \leftrightarrow F (x) = F (x))$
48	47 10	brab2a	$⊢ x \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} x \leftrightarrow ((x \in A \land x \in A) \land F (x) = F (x))$
49	41 42 48	3bitr4i	$⊢ x \in A \leftrightarrow x \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} x$
50	1 19 39 49	iseri	$⊢ \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} Er A$
51	11	baib	$⊢ (x \in A \land y \in A) \to (x \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} y \leftrightarrow F (x) = F (y))$
52	51	rgen2	$⊢ \forall x \in A \forall y \in A (x \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} y \leftrightarrow F (x) = F (y))$
53		id	$⊢ A \in V \to A \in V$
54		simprll	$⊢ (A \in V \land ((u \in A \land v \in A) \land F (u) = F (v))) \to u \in A$
55		simprlr	$⊢ (A \in V \land ((u \in A \land v \in A) \land F (u) = F (v))) \to v \in A$
56	53 53 54 55	opabex2	$⊢ A \in V \to \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} \in V$
57		ereq1	$⊢ r = \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} \to (r Er A \leftrightarrow \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} Er A)$
58		simpl	$⊢ (r = \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} \land (x \in A \land y \in A)) \to r = \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\}$
59	58	breqd	$⊢ (r = \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} \land (x \in A \land y \in A)) \to (x r y \leftrightarrow x \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} y)$
60	59	bibi1d	$⊢ (r = \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} \land (x \in A \land y \in A)) \to ((x r y \leftrightarrow F (x) = F (y)) \leftrightarrow (x \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} y \leftrightarrow F (x) = F (y)))$
61	60	2ralbidva	$⊢ r = \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} \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 \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} y \leftrightarrow F (x) = F (y)))$
62	57 61	anbi12d	$⊢ r = \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} \to ((r Er A \land \forall x \in A \forall y \in A (x r y \leftrightarrow F (x) = F (y))) \leftrightarrow (\{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} Er A \land \forall x \in A \forall y \in A (x \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} y \leftrightarrow F (x) = F (y))))$
63	62	spcegv	$⊢ \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} \in V \to ((\{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} Er A \land \forall x \in A \forall y \in A (x \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} y \leftrightarrow F (x) = F (y))) \to \exists r (r Er A \land \forall x \in A \forall y \in A (x r y \leftrightarrow F (x) = F (y))))$
64	56 63	syl	$⊢ A \in V \to ((\{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} Er A \land \forall x \in A \forall y \in A (x \{⟨u, v⟩ \| ((u \in A \land v \in A) \land F (u) = F (v))\} y \leftrightarrow F (x) = F (y))) \to \exists r (r Er A \land \forall x \in A \forall y \in A (x r y \leftrightarrow F (x) = F (y))))$
65	50 52 64	mp2ani	$⊢ A \in V \to \exists r (r Er A \land \forall x \in A \forall y \in A (x r y \leftrightarrow F (x) = F (y)))$

Metamath Proof Explorer

Theorem tgjustf

Proof