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

Metamath Proof Explorer

Theorem mpets2

Description: Member Partition-Equivalence Theorem with binary relations, cf. mpet2 . (Contributed by Peter Mazsa, 24-Sep-2021)

Ref Expression
Assertion mpets2 ( 𝐴 ∈ 𝑉 → ( ( ◡ E ↾ 𝐴 ) Parts 𝐴 ↔ ≀ ( ◡ E ↾ 𝐴 ) Ers 𝐴 ) )

Proof

Step Hyp Ref Expression
1 mpet2 ⊢ ( ( ◡ E ↾ 𝐴 ) Part 𝐴 ↔ ≀ ( ◡ E ↾ 𝐴 ) ErALTV 𝐴 )
2 cnvepresex ⊢ ( 𝐴 ∈ 𝑉 → ( ◡ E ↾ 𝐴 ) ∈ V )
3 brpartspart ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ◡ E ↾ 𝐴 ) ∈ V ) → ( ( ◡ E ↾ 𝐴 ) Parts 𝐴 ↔ ( ◡ E ↾ 𝐴 ) Part 𝐴 ) )
4 2 3 mpdan ⊢ ( 𝐴 ∈ 𝑉 → ( ( ◡ E ↾ 𝐴 ) Parts 𝐴 ↔ ( ◡ E ↾ 𝐴 ) Part 𝐴 ) )
5 1cosscnvepresex ⊢ ( 𝐴 ∈ 𝑉 → ≀ ( ◡ E ↾ 𝐴 ) ∈ V )
6 brerser ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ≀ ( ◡ E ↾ 𝐴 ) ∈ V ) → ( ≀ ( ◡ E ↾ 𝐴 ) Ers 𝐴 ↔ ≀ ( ◡ E ↾ 𝐴 ) ErALTV 𝐴 ) )
7 5 6 mpdan ⊢ ( 𝐴 ∈ 𝑉 → ( ≀ ( ◡ E ↾ 𝐴 ) Ers 𝐴 ↔ ≀ ( ◡ E ↾ 𝐴 ) ErALTV 𝐴 ) )
8 4 7 bibi12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( ( ◡ E ↾ 𝐴 ) Parts 𝐴 ↔ ≀ ( ◡ E ↾ 𝐴 ) Ers 𝐴 ) ↔ ( ( ◡ E ↾ 𝐴 ) Part 𝐴 ↔ ≀ ( ◡ E ↾ 𝐴 ) ErALTV 𝐴 ) ) )
9 1 8 mpbiri ⊢ ( 𝐴 ∈ 𝑉 → ( ( ◡ E ↾ 𝐴 ) Parts 𝐴 ↔ ≀ ( ◡ E ↾ 𝐴 ) Ers 𝐴 ) )