Metamath Proof Explorer

Theorem brparts2

Description: Binary partitions relation. (Contributed by Peter Mazsa, 30-Dec-2021)

Ref Expression
Assertion brparts2 ⊢ A ∈ V ∧ R ∈ W → R Parts A ↔ R ∈ Disjs ∧ dom ⁡ R / R = A

Proof

Step Hyp Ref Expression
1 brparts ⊢ A ∈ V → R Parts A ↔ R ∈ Disjs ∧ R DomainQss A
2 1 adantr ⊢ A ∈ V ∧ R ∈ W → R Parts A ↔ R ∈ Disjs ∧ R DomainQss A
3 brdmqss ⊢ A ∈ V ∧ R ∈ W → R DomainQss A ↔ dom ⁡ R / R = A
4 3 anbi2d ⊢ A ∈ V ∧ R ∈ W → R ∈ Disjs ∧ R DomainQss A ↔ R ∈ Disjs ∧ dom ⁡ R / R = A
5 2 4 bitrd ⊢ A ∈ V ∧ R ∈ W → R Parts A ↔ R ∈ Disjs ∧ dom ⁡ R / R = A