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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 prtlem18.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }
2 rexcom4 ⊢ ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑧 ( 𝑧 ∈ 𝑣 ∧ 𝑝 = [ 𝑧 ] ∼ ) ↔ ∃ 𝑧 ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑝 = [ 𝑧 ] ∼ ) )
3 r19.41v ⊢ ( ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑝 = [ 𝑧 ] ∼ ) ↔ ( ∃ 𝑣 ∈ 𝐴 𝑧 ∈ 𝑣 ∧ 𝑝 = [ 𝑧 ] ∼ ) )
4 3 exbii ⊢ ( ∃ 𝑧 ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑝 = [ 𝑧 ] ∼ ) ↔ ∃ 𝑧 ( ∃ 𝑣 ∈ 𝐴 𝑧 ∈ 𝑣 ∧ 𝑝 = [ 𝑧 ] ∼ ) )
5 2 4 bitri ⊢ ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑧 ( 𝑧 ∈ 𝑣 ∧ 𝑝 = [ 𝑧 ] ∼ ) ↔ ∃ 𝑧 ( ∃ 𝑣 ∈ 𝐴 𝑧 ∈ 𝑣 ∧ 𝑝 = [ 𝑧 ] ∼ ) )
6 df-rex ⊢ ( ∃ 𝑧 ∈ 𝑣 𝑝 = [ 𝑧 ] ∼ ↔ ∃ 𝑧 ( 𝑧 ∈ 𝑣 ∧ 𝑝 = [ 𝑧 ] ∼ ) )
7 6 rexbii ⊢ ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑧 ∈ 𝑣 𝑝 = [ 𝑧 ] ∼ ↔ ∃ 𝑣 ∈ 𝐴 ∃ 𝑧 ( 𝑧 ∈ 𝑣 ∧ 𝑝 = [ 𝑧 ] ∼ ) )
8 vex ⊢ 𝑝 ∈ V
9 8 elqs ⊢ ( 𝑝 ∈ ( ∪ 𝐴 / ∼ ) ↔ ∃ 𝑧 ∈ ∪ 𝐴 𝑝 = [ 𝑧 ] ∼ )
10 df-rex ⊢ ( ∃ 𝑧 ∈ ∪ 𝐴 𝑝 = [ 𝑧 ] ∼ ↔ ∃ 𝑧 ( 𝑧 ∈ ∪ 𝐴 ∧ 𝑝 = [ 𝑧 ] ∼ ) )
11 eluni2 ⊢ ( 𝑧 ∈ ∪ 𝐴 ↔ ∃ 𝑣 ∈ 𝐴 𝑧 ∈ 𝑣 )
12 11 anbi1i ⊢ ( ( 𝑧 ∈ ∪ 𝐴 ∧ 𝑝 = [ 𝑧 ] ∼ ) ↔ ( ∃ 𝑣 ∈ 𝐴 𝑧 ∈ 𝑣 ∧ 𝑝 = [ 𝑧 ] ∼ ) )
13 12 exbii ⊢ ( ∃ 𝑧 ( 𝑧 ∈ ∪ 𝐴 ∧ 𝑝 = [ 𝑧 ] ∼ ) ↔ ∃ 𝑧 ( ∃ 𝑣 ∈ 𝐴 𝑧 ∈ 𝑣 ∧ 𝑝 = [ 𝑧 ] ∼ ) )
14 10 13 bitri ⊢ ( ∃ 𝑧 ∈ ∪ 𝐴 𝑝 = [ 𝑧 ] ∼ ↔ ∃ 𝑧 ( ∃ 𝑣 ∈ 𝐴 𝑧 ∈ 𝑣 ∧ 𝑝 = [ 𝑧 ] ∼ ) )
15 9 14 bitri ⊢ ( 𝑝 ∈ ( ∪ 𝐴 / ∼ ) ↔ ∃ 𝑧 ( ∃ 𝑣 ∈ 𝐴 𝑧 ∈ 𝑣 ∧ 𝑝 = [ 𝑧 ] ∼ ) )
16 5 7 15 3bitr4ri ⊢ ( 𝑝 ∈ ( ∪ 𝐴 / ∼ ) ↔ ∃ 𝑣 ∈ 𝐴 ∃ 𝑧 ∈ 𝑣 𝑝 = [ 𝑧 ] ∼ )
17 1 prtlem19 ⊢ ( Prt 𝐴 → ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → 𝑣 = [ 𝑧 ] ∼ ) )
18 17 ralrimivv ⊢ ( Prt 𝐴 → ∀ 𝑣 ∈ 𝐴 ∀ 𝑧 ∈ 𝑣 𝑣 = [ 𝑧 ] ∼ )
19 2r19.29 ⊢ ( ( ∀ 𝑣 ∈ 𝐴 ∀ 𝑧 ∈ 𝑣 𝑣 = [ 𝑧 ] ∼ ∧ ∃ 𝑣 ∈ 𝐴 ∃ 𝑧 ∈ 𝑣 𝑝 = [ 𝑧 ] ∼ ) → ∃ 𝑣 ∈ 𝐴 ∃ 𝑧 ∈ 𝑣 ( 𝑣 = [ 𝑧 ] ∼ ∧ 𝑝 = [ 𝑧 ] ∼ ) )
20 19 ex ⊢ ( ∀ 𝑣 ∈ 𝐴 ∀ 𝑧 ∈ 𝑣 𝑣 = [ 𝑧 ] ∼ → ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑧 ∈ 𝑣 𝑝 = [ 𝑧 ] ∼ → ∃ 𝑣 ∈ 𝐴 ∃ 𝑧 ∈ 𝑣 ( 𝑣 = [ 𝑧 ] ∼ ∧ 𝑝 = [ 𝑧 ] ∼ ) ) )
21 18 20 syl ⊢ ( Prt 𝐴 → ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑧 ∈ 𝑣 𝑝 = [ 𝑧 ] ∼ → ∃ 𝑣 ∈ 𝐴 ∃ 𝑧 ∈ 𝑣 ( 𝑣 = [ 𝑧 ] ∼ ∧ 𝑝 = [ 𝑧 ] ∼ ) ) )
22 16 21 biimtrid ⊢ ( Prt 𝐴 → ( 𝑝 ∈ ( ∪ 𝐴 / ∼ ) → ∃ 𝑣 ∈ 𝐴 ∃ 𝑧 ∈ 𝑣 ( 𝑣 = [ 𝑧 ] ∼ ∧ 𝑝 = [ 𝑧 ] ∼ ) ) )
23 eqtr3 ⊢ ( ( 𝑣 = [ 𝑧 ] ∼ ∧ 𝑝 = [ 𝑧 ] ∼ ) → 𝑣 = 𝑝 )
24 23 reximi ⊢ ( ∃ 𝑧 ∈ 𝑣 ( 𝑣 = [ 𝑧 ] ∼ ∧ 𝑝 = [ 𝑧 ] ∼ ) → ∃ 𝑧 ∈ 𝑣 𝑣 = 𝑝 )
25 24 reximi ⊢ ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑧 ∈ 𝑣 ( 𝑣 = [ 𝑧 ] ∼ ∧ 𝑝 = [ 𝑧 ] ∼ ) → ∃ 𝑣 ∈ 𝐴 ∃ 𝑧 ∈ 𝑣 𝑣 = 𝑝 )
26 22 25 syl6 ⊢ ( Prt 𝐴 → ( 𝑝 ∈ ( ∪ 𝐴 / ∼ ) → ∃ 𝑣 ∈ 𝐴 ∃ 𝑧 ∈ 𝑣 𝑣 = 𝑝 ) )
27 df-rex ⊢ ( ∃ 𝑧 ∈ 𝑣 𝑣 = 𝑝 ↔ ∃ 𝑧 ( 𝑧 ∈ 𝑣 ∧ 𝑣 = 𝑝 ) )
28 19.41v ⊢ ( ∃ 𝑧 ( 𝑧 ∈ 𝑣 ∧ 𝑣 = 𝑝 ) ↔ ( ∃ 𝑧 𝑧 ∈ 𝑣 ∧ 𝑣 = 𝑝 ) )
29 27 28 bitri ⊢ ( ∃ 𝑧 ∈ 𝑣 𝑣 = 𝑝 ↔ ( ∃ 𝑧 𝑧 ∈ 𝑣 ∧ 𝑣 = 𝑝 ) )
30 29 simprbi ⊢ ( ∃ 𝑧 ∈ 𝑣 𝑣 = 𝑝 → 𝑣 = 𝑝 )
31 30 reximi ⊢ ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑧 ∈ 𝑣 𝑣 = 𝑝 → ∃ 𝑣 ∈ 𝐴 𝑣 = 𝑝 )
32 26 31 syl6 ⊢ ( Prt 𝐴 → ( 𝑝 ∈ ( ∪ 𝐴 / ∼ ) → ∃ 𝑣 ∈ 𝐴 𝑣 = 𝑝 ) )
33 risset ⊢ ( 𝑝 ∈ 𝐴 ↔ ∃ 𝑣 ∈ 𝐴 𝑣 = 𝑝 )
34 32 33 imbitrrdi ⊢ ( Prt 𝐴 → ( 𝑝 ∈ ( ∪ 𝐴 / ∼ ) → 𝑝 ∈ 𝐴 ) )
35 1 prtlem400 ⊢ ¬ ∅ ∈ ( ∪ 𝐴 / ∼ )
36 nelelne ⊢ ( ¬ ∅ ∈ ( ∪ 𝐴 / ∼ ) → ( 𝑝 ∈ ( ∪ 𝐴 / ∼ ) → 𝑝 ≠ ∅ ) )
37 35 36 mp1i ⊢ ( Prt 𝐴 → ( 𝑝 ∈ ( ∪ 𝐴 / ∼ ) → 𝑝 ≠ ∅ ) )
38 34 37 jcad ⊢ ( Prt 𝐴 → ( 𝑝 ∈ ( ∪ 𝐴 / ∼ ) → ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≠ ∅ ) ) )
39 eldifsn ⊢ ( 𝑝 ∈ ( 𝐴 ∖ { ∅ } ) ↔ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≠ ∅ ) )
40 38 39 imbitrrdi ⊢ ( Prt 𝐴 → ( 𝑝 ∈ ( ∪ 𝐴 / ∼ ) → 𝑝 ∈ ( 𝐴 ∖ { ∅ } ) ) )
41 neldifsn ⊢ ¬ ∅ ∈ ( 𝐴 ∖ { ∅ } )
42 n0el ⊢ ( ¬ ∅ ∈ ( 𝐴 ∖ { ∅ } ) ↔ ∀ 𝑝 ∈ ( 𝐴 ∖ { ∅ } ) ∃ 𝑧 𝑧 ∈ 𝑝 )
43 41 42 mpbi ⊢ ∀ 𝑝 ∈ ( 𝐴 ∖ { ∅ } ) ∃ 𝑧 𝑧 ∈ 𝑝
44 43 rspec ⊢ ( 𝑝 ∈ ( 𝐴 ∖ { ∅ } ) → ∃ 𝑧 𝑧 ∈ 𝑝 )
45 eldifi ⊢ ( 𝑝 ∈ ( 𝐴 ∖ { ∅ } ) → 𝑝 ∈ 𝐴 )
46 44 45 jca ⊢ ( 𝑝 ∈ ( 𝐴 ∖ { ∅ } ) → ( ∃ 𝑧 𝑧 ∈ 𝑝 ∧ 𝑝 ∈ 𝐴 ) )
47 1 prtlem19 ⊢ ( Prt 𝐴 → ( ( 𝑝 ∈ 𝐴 ∧ 𝑧 ∈ 𝑝 ) → 𝑝 = [ 𝑧 ] ∼ ) )
48 47 ancomsd ⊢ ( Prt 𝐴 → ( ( 𝑧 ∈ 𝑝 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 = [ 𝑧 ] ∼ ) )
49 elunii ⊢ ( ( 𝑧 ∈ 𝑝 ∧ 𝑝 ∈ 𝐴 ) → 𝑧 ∈ ∪ 𝐴 )
50 48 49 jca2r ⊢ ( Prt 𝐴 → ( ( 𝑧 ∈ 𝑝 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑧 ∈ ∪ 𝐴 ∧ 𝑝 = [ 𝑧 ] ∼ ) ) )
51 prtlem11 ⊢ ( 𝑝 ∈ V → ( 𝑧 ∈ ∪ 𝐴 → ( 𝑝 = [ 𝑧 ] ∼ → 𝑝 ∈ ( ∪ 𝐴 / ∼ ) ) ) )
52 51 elv ⊢ ( 𝑧 ∈ ∪ 𝐴 → ( 𝑝 = [ 𝑧 ] ∼ → 𝑝 ∈ ( ∪ 𝐴 / ∼ ) ) )
53 52 imp ⊢ ( ( 𝑧 ∈ ∪ 𝐴 ∧ 𝑝 = [ 𝑧 ] ∼ ) → 𝑝 ∈ ( ∪ 𝐴 / ∼ ) )
54 50 53 syl6 ⊢ ( Prt 𝐴 → ( ( 𝑧 ∈ 𝑝 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ ( ∪ 𝐴 / ∼ ) ) )
55 54 eximdv ⊢ ( Prt 𝐴 → ( ∃ 𝑧 ( 𝑧 ∈ 𝑝 ∧ 𝑝 ∈ 𝐴 ) → ∃ 𝑧 𝑝 ∈ ( ∪ 𝐴 / ∼ ) ) )
56 19.41v ⊢ ( ∃ 𝑧 ( 𝑧 ∈ 𝑝 ∧ 𝑝 ∈ 𝐴 ) ↔ ( ∃ 𝑧 𝑧 ∈ 𝑝 ∧ 𝑝 ∈ 𝐴 ) )
57 19.9v ⊢ ( ∃ 𝑧 𝑝 ∈ ( ∪ 𝐴 / ∼ ) ↔ 𝑝 ∈ ( ∪ 𝐴 / ∼ ) )
58 55 56 57 3imtr3g ⊢ ( Prt 𝐴 → ( ( ∃ 𝑧 𝑧 ∈ 𝑝 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ ( ∪ 𝐴 / ∼ ) ) )
59 46 58 syl5 ⊢ ( Prt 𝐴 → ( 𝑝 ∈ ( 𝐴 ∖ { ∅ } ) → 𝑝 ∈ ( ∪ 𝐴 / ∼ ) ) )
60 40 59 impbid ⊢ ( Prt 𝐴 → ( 𝑝 ∈ ( ∪ 𝐴 / ∼ ) ↔ 𝑝 ∈ ( 𝐴 ∖ { ∅ } ) ) )
61 60 eqrdv ⊢ ( Prt 𝐴 → ( ∪ 𝐴 / ∼ ) = ( 𝐴 ∖ { ∅ } ) )