Theorem 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	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }
Assertion	prter3	⊢ ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) → ∼ = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		prtlem18.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }
2		errel	⊢ ( 𝑆 Er ∪ 𝐴 → Rel 𝑆 )
3	2	adantr	⊢ ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) → Rel 𝑆 )
4	1	relopabiv	⊢ Rel ∼
5	1	prtlem13	⊢ ( 𝑧 ∼ 𝑤 ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) )
6		simpll	⊢ ( ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) ) → 𝑆 Er ∪ 𝐴 )
7		simprl	⊢ ( ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) ) → 𝑣 ∈ 𝐴 )
8		ne0i	⊢ ( 𝑧 ∈ 𝑣 → 𝑣 ≠ ∅ )
9	8	ad2antll	⊢ ( ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) ) → 𝑣 ≠ ∅ )
10		eldifsn	⊢ ( 𝑣 ∈ ( 𝐴 ∖ { ∅ } ) ↔ ( 𝑣 ∈ 𝐴 ∧ 𝑣 ≠ ∅ ) )
11	7 9 10	sylanbrc	⊢ ( ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) ) → 𝑣 ∈ ( 𝐴 ∖ { ∅ } ) )
12		simplr	⊢ ( ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) ) → ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) )
13	11 12	eleqtrrd	⊢ ( ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) ) → 𝑣 ∈ ( ∪ 𝐴 / 𝑆 ) )
14		simprr	⊢ ( ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) ) → 𝑧 ∈ 𝑣 )
15		qsel	⊢ ( ( 𝑆 Er ∪ 𝐴 ∧ 𝑣 ∈ ( ∪ 𝐴 / 𝑆 ) ∧ 𝑧 ∈ 𝑣 ) → 𝑣 = [ 𝑧 ] 𝑆 )
16	6 13 14 15	syl3anc	⊢ ( ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) ) → 𝑣 = [ 𝑧 ] 𝑆 )
17	16	eleq2d	⊢ ( ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) ) → ( 𝑤 ∈ 𝑣 ↔ 𝑤 ∈ [ 𝑧 ] 𝑆 ) )
18		vex	⊢ 𝑤 ∈ V
19		vex	⊢ 𝑧 ∈ V
20	18 19	elec	⊢ ( 𝑤 ∈ [ 𝑧 ] 𝑆 ↔ 𝑧 𝑆 𝑤 )
21	17 20	bitrdi	⊢ ( ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) ) → ( 𝑤 ∈ 𝑣 ↔ 𝑧 𝑆 𝑤 ) )
22	21	anassrs	⊢ ( ( ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝑣 ) → ( 𝑤 ∈ 𝑣 ↔ 𝑧 𝑆 𝑤 ) )
23	22	pm5.32da	⊢ ( ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ( 𝑧 ∈ 𝑣 ∧ 𝑧 𝑆 𝑤 ) ) )
24	23	rexbidva	⊢ ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) → ( ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑧 𝑆 𝑤 ) ) )
25		simpll	⊢ ( ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ∧ 𝑧 𝑆 𝑤 ) → 𝑆 Er ∪ 𝐴 )
26		simpr	⊢ ( ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ∧ 𝑧 𝑆 𝑤 ) → 𝑧 𝑆 𝑤 )
27	25 26	ercl	⊢ ( ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ∧ 𝑧 𝑆 𝑤 ) → 𝑧 ∈ ∪ 𝐴 )
28		eluni2	⊢ ( 𝑧 ∈ ∪ 𝐴 ↔ ∃ 𝑣 ∈ 𝐴 𝑧 ∈ 𝑣 )
29	27 28	sylib	⊢ ( ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ∧ 𝑧 𝑆 𝑤 ) → ∃ 𝑣 ∈ 𝐴 𝑧 ∈ 𝑣 )
30	29	ex	⊢ ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) → ( 𝑧 𝑆 𝑤 → ∃ 𝑣 ∈ 𝐴 𝑧 ∈ 𝑣 ) )
31	30	pm4.71rd	⊢ ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) → ( 𝑧 𝑆 𝑤 ↔ ( ∃ 𝑣 ∈ 𝐴 𝑧 ∈ 𝑣 ∧ 𝑧 𝑆 𝑤 ) ) )
32		r19.41v	⊢ ( ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑧 𝑆 𝑤 ) ↔ ( ∃ 𝑣 ∈ 𝐴 𝑧 ∈ 𝑣 ∧ 𝑧 𝑆 𝑤 ) )
33	31 32	bitr4di	⊢ ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) → ( 𝑧 𝑆 𝑤 ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑧 𝑆 𝑤 ) ) )
34	24 33	bitr4d	⊢ ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) → ( ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ 𝑧 𝑆 𝑤 ) )
35	5 34	syl5bb	⊢ ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) → ( 𝑧 ∼ 𝑤 ↔ 𝑧 𝑆 𝑤 ) )
36	35	adantl	⊢ ( ( ( Rel ∼ ∧ Rel 𝑆 ) ∧ ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ) → ( 𝑧 ∼ 𝑤 ↔ 𝑧 𝑆 𝑤 ) )
37	36	eqbrrdv2	⊢ ( ( ( Rel ∼ ∧ Rel 𝑆 ) ∧ ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ) → ∼ = 𝑆 )
38	4 37	mpanl1	⊢ ( ( Rel 𝑆 ∧ ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ) → ∼ = 𝑆 )
39	3 38	mpancom	⊢ ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) → ∼ = 𝑆 )