Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Partitions: disjoints on domain quotients
partsuc2
Next ⟩
partsuc
Metamath Proof Explorer
Ascii
Unicode
Theorem
partsuc2
Description:
Property of the partition.
(Contributed by
Peter Mazsa
, 24-Jul-2024)
Ref
Expression
Assertion
partsuc2
⊢
R
↾
A
∪
A
∖
R
↾
A
Part
A
∪
A
∖
A
↔
R
↾
A
Part
A
Proof
Step
Hyp
Ref
Expression
1
ressucdifsn2
⊢
R
↾
A
∪
A
∖
R
↾
A
=
R
↾
A
2
sucdifsn2
⊢
A
∪
A
∖
A
=
A
3
parteq12
⊢
R
↾
A
∪
A
∖
R
↾
A
=
R
↾
A
∧
A
∪
A
∖
A
=
A
→
R
↾
A
∪
A
∖
R
↾
A
Part
A
∪
A
∖
A
↔
R
↾
A
Part
A
4
1
2
3
mp2an
⊢
R
↾
A
∪
A
∖
R
↾
A
Part
A
∪
A
∖
A
↔
R
↾
A
Part
A