prter2

Description: The quotient set of the equivalence relation generated by a partition equals the partition itself. (Contributed by Rodolfo Medina, 17-Oct-2010)

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

Proof

Step	Hyp	Ref	Expression
1		prtlem18.1	$⊢ \underset{˙}{\sim} = \{⟨x, y⟩ \| \exists u \in A (x \in u \land y \in u)\}$
2		rexcom4	$⊢ \exists v \in A \exists z (z \in v \land p = [z] \underset{˙}{\sim}) \leftrightarrow \exists z \exists v \in A (z \in v \land p = [z] \underset{˙}{\sim})$
3		r19.41v	$⊢ \exists v \in A (z \in v \land p = [z] \underset{˙}{\sim}) \leftrightarrow (\exists v \in A z \in v \land p = [z] \underset{˙}{\sim})$
4	3	exbii	$⊢ \exists z \exists v \in A (z \in v \land p = [z] \underset{˙}{\sim}) \leftrightarrow \exists z (\exists v \in A z \in v \land p = [z] \underset{˙}{\sim})$
5	2 4	bitri	$⊢ \exists v \in A \exists z (z \in v \land p = [z] \underset{˙}{\sim}) \leftrightarrow \exists z (\exists v \in A z \in v \land p = [z] \underset{˙}{\sim})$
6		df-rex	$⊢ \exists z \in v p = [z] \underset{˙}{\sim} \leftrightarrow \exists z (z \in v \land p = [z] \underset{˙}{\sim})$
7	6	rexbii	$⊢ \exists v \in A \exists z \in v p = [z] \underset{˙}{\sim} \leftrightarrow \exists v \in A \exists z (z \in v \land p = [z] \underset{˙}{\sim})$
8		vex	$⊢ p \in V$
9	8	elqs	$⊢ p \in (⋃ A / \underset{˙}{\sim}) \leftrightarrow \exists z \in ⋃ A p = [z] \underset{˙}{\sim}$
10		df-rex	$⊢ \exists z \in ⋃ A p = [z] \underset{˙}{\sim} \leftrightarrow \exists z (z \in ⋃ A \land p = [z] \underset{˙}{\sim})$
11		eluni2	$⊢ z \in ⋃ A \leftrightarrow \exists v \in A z \in v$
12	11	anbi1i	$⊢ (z \in ⋃ A \land p = [z] \underset{˙}{\sim}) \leftrightarrow (\exists v \in A z \in v \land p = [z] \underset{˙}{\sim})$
13	12	exbii	$⊢ \exists z (z \in ⋃ A \land p = [z] \underset{˙}{\sim}) \leftrightarrow \exists z (\exists v \in A z \in v \land p = [z] \underset{˙}{\sim})$
14	10 13	bitri	$⊢ \exists z \in ⋃ A p = [z] \underset{˙}{\sim} \leftrightarrow \exists z (\exists v \in A z \in v \land p = [z] \underset{˙}{\sim})$
15	9 14	bitri	$⊢ p \in (⋃ A / \underset{˙}{\sim}) \leftrightarrow \exists z (\exists v \in A z \in v \land p = [z] \underset{˙}{\sim})$
16	5 7 15	3bitr4ri	$⊢ p \in (⋃ A / \underset{˙}{\sim}) \leftrightarrow \exists v \in A \exists z \in v p = [z] \underset{˙}{\sim}$
17	1	prtlem19	$⊢ Prt A \to ((v \in A \land z \in v) \to v = [z] \underset{˙}{\sim})$
18	17	ralrimivv	$⊢ Prt A \to \forall v \in A \forall z \in v v = [z] \underset{˙}{\sim}$
19		2r19.29	$⊢ (\forall v \in A \forall z \in v v = [z] \underset{˙}{\sim} \land \exists v \in A \exists z \in v p = [z] \underset{˙}{\sim}) \to \exists v \in A \exists z \in v (v = [z] \underset{˙}{\sim} \land p = [z] \underset{˙}{\sim})$
20	19	ex	$⊢ \forall v \in A \forall z \in v v = [z] \underset{˙}{\sim} \to (\exists v \in A \exists z \in v p = [z] \underset{˙}{\sim} \to \exists v \in A \exists z \in v (v = [z] \underset{˙}{\sim} \land p = [z] \underset{˙}{\sim}))$
21	18 20	syl	$⊢ Prt A \to (\exists v \in A \exists z \in v p = [z] \underset{˙}{\sim} \to \exists v \in A \exists z \in v (v = [z] \underset{˙}{\sim} \land p = [z] \underset{˙}{\sim}))$
22	16 21	biimtrid	$⊢ Prt A \to (p \in (⋃ A / \underset{˙}{\sim}) \to \exists v \in A \exists z \in v (v = [z] \underset{˙}{\sim} \land p = [z] \underset{˙}{\sim}))$
23		eqtr3	$⊢ (v = [z] \underset{˙}{\sim} \land p = [z] \underset{˙}{\sim}) \to v = p$
24	23	reximi	$⊢ \exists z \in v (v = [z] \underset{˙}{\sim} \land p = [z] \underset{˙}{\sim}) \to \exists z \in v v = p$
25	24	reximi	$⊢ \exists v \in A \exists z \in v (v = [z] \underset{˙}{\sim} \land p = [z] \underset{˙}{\sim}) \to \exists v \in A \exists z \in v v = p$
26	22 25	syl6	$⊢ Prt A \to (p \in (⋃ A / \underset{˙}{\sim}) \to \exists v \in A \exists z \in v v = p)$
27		df-rex	$⊢ \exists z \in v v = p \leftrightarrow \exists z (z \in v \land v = p)$
28		19.41v	$⊢ \exists z (z \in v \land v = p) \leftrightarrow (\exists z z \in v \land v = p)$
29	27 28	bitri	$⊢ \exists z \in v v = p \leftrightarrow (\exists z z \in v \land v = p)$
30	29	simprbi	$⊢ \exists z \in v v = p \to v = p$
31	30	reximi	$⊢ \exists v \in A \exists z \in v v = p \to \exists v \in A v = p$
32	26 31	syl6	$⊢ Prt A \to (p \in (⋃ A / \underset{˙}{\sim}) \to \exists v \in A v = p)$
33		risset	$⊢ p \in A \leftrightarrow \exists v \in A v = p$
34	32 33	imbitrrdi	$⊢ Prt A \to (p \in (⋃ A / \underset{˙}{\sim}) \to p \in A)$
35	1	prtlem400	$⊢ \neg \emptyset \in (⋃ A / \underset{˙}{\sim})$
36		nelelne	$⊢ \neg \emptyset \in (⋃ A / \underset{˙}{\sim}) \to (p \in (⋃ A / \underset{˙}{\sim}) \to p \neq \emptyset)$
37	35 36	mp1i	$⊢ Prt A \to (p \in (⋃ A / \underset{˙}{\sim}) \to p \neq \emptyset)$
38	34 37	jcad	$⊢ Prt A \to (p \in (⋃ A / \underset{˙}{\sim}) \to (p \in A \land p \neq \emptyset))$
39		eldifsn	$⊢ p \in (A ∖ \{\emptyset\}) \leftrightarrow (p \in A \land p \neq \emptyset)$
40	38 39	imbitrrdi	$⊢ Prt A \to (p \in (⋃ A / \underset{˙}{\sim}) \to p \in (A ∖ \{\emptyset\}))$
41		neldifsn	$⊢ \neg \emptyset \in (A ∖ \{\emptyset\})$
42		n0el	$⊢ \neg \emptyset \in (A ∖ \{\emptyset\}) \leftrightarrow \forall p \in (A ∖ \{\emptyset\}) \exists z z \in p$
43	41 42	mpbi	$⊢ \forall p \in (A ∖ \{\emptyset\}) \exists z z \in p$
44	43	rspec	$⊢ p \in (A ∖ \{\emptyset\}) \to \exists z z \in p$
45		eldifi	$⊢ p \in (A ∖ \{\emptyset\}) \to p \in A$
46	44 45	jca	$⊢ p \in (A ∖ \{\emptyset\}) \to (\exists z z \in p \land p \in A)$
47	1	prtlem19	$⊢ Prt A \to ((p \in A \land z \in p) \to p = [z] \underset{˙}{\sim})$
48	47	ancomsd	$⊢ Prt A \to ((z \in p \land p \in A) \to p = [z] \underset{˙}{\sim})$
49		elunii	$⊢ (z \in p \land p \in A) \to z \in ⋃ A$
50	48 49	jca2r	$⊢ Prt A \to ((z \in p \land p \in A) \to (z \in ⋃ A \land p = [z] \underset{˙}{\sim}))$
51		prtlem11	$⊢ p \in V \to (z \in ⋃ A \to (p = [z] \underset{˙}{\sim} \to p \in (⋃ A / \underset{˙}{\sim})))$
52	51	elv	$⊢ z \in ⋃ A \to (p = [z] \underset{˙}{\sim} \to p \in (⋃ A / \underset{˙}{\sim}))$
53	52	imp	$⊢ (z \in ⋃ A \land p = [z] \underset{˙}{\sim}) \to p \in (⋃ A / \underset{˙}{\sim})$
54	50 53	syl6	$⊢ Prt A \to ((z \in p \land p \in A) \to p \in (⋃ A / \underset{˙}{\sim}))$
55	54	eximdv	$⊢ Prt A \to (\exists z (z \in p \land p \in A) \to \exists z p \in (⋃ A / \underset{˙}{\sim}))$
56		19.41v	$⊢ \exists z (z \in p \land p \in A) \leftrightarrow (\exists z z \in p \land p \in A)$
57		19.9v	$⊢ \exists z p \in (⋃ A / \underset{˙}{\sim}) \leftrightarrow p \in (⋃ A / \underset{˙}{\sim})$
58	55 56 57	3imtr3g	$⊢ Prt A \to ((\exists z z \in p \land p \in A) \to p \in (⋃ A / \underset{˙}{\sim}))$
59	46 58	syl5	$⊢ Prt A \to (p \in (A ∖ \{\emptyset\}) \to p \in (⋃ A / \underset{˙}{\sim}))$
60	40 59	impbid	$⊢ Prt A \to (p \in (⋃ A / \underset{˙}{\sim}) \leftrightarrow p \in (A ∖ \{\emptyset\}))$
61	60	eqrdv	$⊢ Prt A \to ⋃ A / \underset{˙}{\sim} = A ∖ \{\emptyset\}$

Metamath Proof Explorer

Theorem prter2

Proof