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 ⊢ φ → ∼ ˙ Er V
ercpbl.v ⊢ φ → V ∈ W
ercpbl.f ⊢ F = x ∈ V ⟼ x ∼ ˙
erlecpbl.e ⊢ φ → A ∼ ˙ C ∧ B ∼ ˙ D → A N B ↔ C N D
Assertion erlecpbl ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → F ⁡ A = F ⁡ C ∧ F ⁡ B = F ⁡ D → A N B ↔ C N D

Proof

Step Hyp Ref Expression
1 ercpbl.r ⊢ φ → ∼ ˙ Er V
2 ercpbl.v ⊢ φ → V ∈ W
3 ercpbl.f ⊢ F = x ∈ V ⟼ x ∼ ˙
4 erlecpbl.e ⊢ φ → A ∼ ˙ C ∧ B ∼ ˙ D → A N B ↔ C N D
5 1 3ad2ant1 ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ∼ ˙ Er V
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 → A N B ↔ C N D
13 11 12 sylbid ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → F ⁡ A = F ⁡ C ∧ F ⁡ B = F ⁡ D → A N B ↔ C N D