prter3

Description: For every partition there exists a unique equivalence relation whose quotient set equals the partition. (Contributed by Rodolfo Medina, 19-Oct-2010) (Proof shortened by Mario Carneiro, 12-Aug-2015)

		Ref	Expression
	Hypothesis	prtlem18.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| \exists u \in A (x \in u \land y \in u)\}$
	Assertion	prter3	$⊢ (S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \to \underset{˙}{\sim} = S$

Proof

Step	Hyp	Ref	Expression
1		prtlem18.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| \exists u \in A (x \in u \land y \in u)\}$
2		errel	$⊢ S Er ⋃ A \to Rel S$
3	2	adantr	$⊢ (S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \to Rel S$
4	1	relopabiv	$⊢ Rel \underset{˙}{\sim}$
5	1	prtlem13	$⊢ z \underset{˙}{\sim} w \leftrightarrow \exists v \in A (z \in v \land w \in v)$
6		simpll	$⊢ ((S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \land (v \in A \land z \in v)) \to S Er ⋃ A$
7		simprl	$⊢ ((S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \land (v \in A \land z \in v)) \to v \in A$
8		ne0i	$⊢ z \in v \to v \neq \emptyset$
9	8	ad2antll	$⊢ ((S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \land (v \in A \land z \in v)) \to v \neq \emptyset$
10		eldifsn	$⊢ v \in (A ∖ \{\emptyset\}) \leftrightarrow (v \in A \land v \neq \emptyset)$
11	7 9 10	sylanbrc	$⊢ ((S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \land (v \in A \land z \in v)) \to v \in (A ∖ \{\emptyset\})$
12		simplr	$⊢ ((S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \land (v \in A \land z \in v)) \to ⋃ A / S = A ∖ \{\emptyset\}$
13	11 12	eleqtrrd	$⊢ ((S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \land (v \in A \land z \in v)) \to v \in (⋃ A / S)$
14		simprr	$⊢ ((S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \land (v \in A \land z \in v)) \to z \in v$
15		qsel	$⊢ (S Er ⋃ A \land v \in (⋃ A / S) \land z \in v) \to v = [z] S$
16	6 13 14 15	syl3anc	$⊢ ((S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \land (v \in A \land z \in v)) \to v = [z] S$
17	16	eleq2d	$⊢ ((S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \land (v \in A \land z \in v)) \to (w \in v \leftrightarrow w \in [z] S)$
18		vex	$⊢ w \in V$
19		vex	$⊢ z \in V$
20	18 19	elec	$⊢ w \in [z] S \leftrightarrow z S w$
21	17 20	bitrdi	$⊢ ((S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \land (v \in A \land z \in v)) \to (w \in v \leftrightarrow z S w)$
22	21	anassrs	$⊢ (((S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \land v \in A) \land z \in v) \to (w \in v \leftrightarrow z S w)$
23	22	pm5.32da	$⊢ ((S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \land v \in A) \to ((z \in v \land w \in v) \leftrightarrow (z \in v \land z S w))$
24	23	rexbidva	$⊢ (S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \to (\exists v \in A (z \in v \land w \in v) \leftrightarrow \exists v \in A (z \in v \land z S w))$
25		simpll	$⊢ ((S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \land z S w) \to S Er ⋃ A$
26		simpr	$⊢ ((S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \land z S w) \to z S w$
27	25 26	ercl	$⊢ ((S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \land z S w) \to z \in ⋃ A$
28		eluni2	$⊢ z \in ⋃ A \leftrightarrow \exists v \in A z \in v$
29	27 28	sylib	$⊢ ((S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \land z S w) \to \exists v \in A z \in v$
30	29	ex	$⊢ (S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \to (z S w \to \exists v \in A z \in v)$
31	30	pm4.71rd	$⊢ (S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \to (z S w \leftrightarrow (\exists v \in A z \in v \land z S w))$
32		r19.41v	$⊢ \exists v \in A (z \in v \land z S w) \leftrightarrow (\exists v \in A z \in v \land z S w)$
33	31 32	bitr4di	$⊢ (S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \to (z S w \leftrightarrow \exists v \in A (z \in v \land z S w))$
34	24 33	bitr4d	$⊢ (S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \to (\exists v \in A (z \in v \land w \in v) \leftrightarrow z S w)$
35	5 34	syl5bb	$⊢ (S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \to (z \underset{˙}{\sim} w \leftrightarrow z S w)$
36	35	adantl	$⊢ ((Rel \underset{˙}{\sim} \land Rel S) \land (S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\})) \to (z \underset{˙}{\sim} w \leftrightarrow z S w)$
37	36	eqbrrdv2	$⊢ ((Rel \underset{˙}{\sim} \land Rel S) \land (S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\})) \to \underset{˙}{\sim} = S$
38	4 37	mpanl1	$⊢ (Rel S \land (S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\})) \to \underset{˙}{\sim} = S$
39	3 38	mpancom	$⊢ (S Er ⋃ A \land ⋃ A / S = A ∖ \{\emptyset\}) \to \underset{˙}{\sim} = S$

Metamath Proof Explorer

Theorem prter3

Proof