Metamath Proof Explorer

Theorem erlecpbl

Description: Translate the relation compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015) (Revised by Mario Carneiro, 12-Aug-2015) (Revised by AV, 12-Jul-2024)

Ref Expression
Hypotheses ercpbl.r ⊢φ→∼˙ErV
ercpbl.v ⊢φ→V∈W
ercpbl.f ⊢F=x∈V⟼x∼˙
erlecpbl.e ⊢φ→A∼˙C∧B∼˙D→ANB↔CND
Assertion erlecpbl ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→F⁡A=F⁡C∧F⁡B=F⁡D→ANB↔CND

Proof

Step Hyp Ref Expression
1 ercpbl.r ⊢φ→∼˙ErV
2 ercpbl.v ⊢φ→V∈W
3 ercpbl.f ⊢F=x∈V⟼x∼˙
4 erlecpbl.e ⊢φ→A∼˙C∧B∼˙D→ANB↔CND
5 1 3ad2ant1 ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→∼˙ErV
6 2 3ad2ant1 ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→V∈W
7 simp2l ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→A∈V
8 5 6 3 7 ercpbllem ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→F⁡A=F⁡C↔A∼˙C
9 simp2r ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→B∈V
10 5 6 3 9 ercpbllem ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→F⁡B=F⁡D↔B∼˙D
11 8 10 anbi12d ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→F⁡A=F⁡C∧F⁡B=F⁡D↔A∼˙C∧B∼˙D
12 4 3ad2ant1 ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→A∼˙C∧B∼˙D→ANB↔CND
13 11 12 sylbid ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→F⁡A=F⁡C∧F⁡B=F⁡D→ANB↔CND