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 𝐴 → ( ∪ 𝐴 / ∼ ) = ( 𝐴 ∖ { ∅ } ) )