This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 bitrid ⊢ ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) → ( 𝑧 ∼ 𝑤 ↔ 𝑧 𝑆 𝑤 ) )
36 35 adantl ⊢ ( ( ( Rel ∼ ∧ Rel 𝑆 ) ∧ ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ) → ( 𝑧 ∼ 𝑤 ↔ 𝑧 𝑆 𝑤 ) )
37 36 eqbrrdv2 ⊢ ( ( ( Rel ∼ ∧ Rel 𝑆 ) ∧ ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ) → ∼ = 𝑆 )
38 4 37 mpanl1 ⊢ ( ( Rel 𝑆 ∧ ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) ) → ∼ = 𝑆 )
39 3 38 mpancom ⊢ ( ( 𝑆 Er ∪ 𝐴 ∧ ( ∪ 𝐴 / 𝑆 ) = ( 𝐴 ∖ { ∅ } ) ) → ∼ = 𝑆 )