Metamath Proof Explorer

Theorem ercpbl

Description: Translate the function 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 ∼ ˙
ercpbl.c ⊢ φ ∧ a ∈ V ∧ b ∈ V → a + ˙ b ∈ V
ercpbl.e ⊢ φ → A ∼ ˙ C ∧ B ∼ ˙ D → A + ˙ B ∼ ˙ C + ˙ D
Assertion ercpbl ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → F ⁡ A = F ⁡ C ∧ F ⁡ B = F ⁡ D → F ⁡ A + ˙ B = F ⁡ C + ˙ D

Proof

Step Hyp Ref Expression
1 ercpbl.r ⊢ φ → ∼ ˙ Er V
2 ercpbl.v ⊢ φ → V ∈ W
3 ercpbl.f ⊢ F = x ∈ V ⟼ x ∼ ˙
4 ercpbl.c ⊢ φ ∧ a ∈ V ∧ b ∈ V → a + ˙ b ∈ V
5 ercpbl.e ⊢ φ → A ∼ ˙ C ∧ B ∼ ˙ D → A + ˙ B ∼ ˙ C + ˙ D
6 5 3ad2ant1 ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → A ∼ ˙ C ∧ B ∼ ˙ D → A + ˙ B ∼ ˙ C + ˙ D
7 1 3ad2ant1 ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → ∼ ˙ Er V
8 2 3ad2ant1 ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → V ∈ W
9 simp2l ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → A ∈ V
10 7 8 3 9 ercpbllem ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → F ⁡ A = F ⁡ C ↔ A ∼ ˙ C
11 simp2r ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → B ∈ V
12 7 8 3 11 ercpbllem ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → F ⁡ B = F ⁡ D ↔ B ∼ ˙ D
13 10 12 anbi12d ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → F ⁡ A = F ⁡ C ∧ F ⁡ B = F ⁡ D ↔ A ∼ ˙ C ∧ B ∼ ˙ D
14 4 caovclg ⊢ φ ∧ A ∈ V ∧ B ∈ V → A + ˙ B ∈ V
15 14 3adant3 ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → A + ˙ B ∈ V
16 7 8 3 15 ercpbllem ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → F ⁡ A + ˙ B = F ⁡ C + ˙ D ↔ A + ˙ B ∼ ˙ C + ˙ D
17 6 13 16 3imtr4d ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → F ⁡ A = F ⁡ C ∧ F ⁡ B = F ⁡ D → F ⁡ A + ˙ B = F ⁡ C + ˙ D