Description: Lemma for ercpbl . (Contributed by Mario Carneiro, 24-Feb-2015) (Revised by AV, 12-Jul-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ercpbl.r | ⊢ ( 𝜑 → ∼ Er 𝑉 ) | |
ercpbl.v | ⊢ ( 𝜑 → 𝑉 ∈ 𝑊 ) | ||
ercpbl.f | ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) | ||
ercpbllem.1 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) | ||
Assertion | ercpbllem | ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) ↔ 𝐴 ∼ 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ercpbl.r | ⊢ ( 𝜑 → ∼ Er 𝑉 ) | |
2 | ercpbl.v | ⊢ ( 𝜑 → 𝑉 ∈ 𝑊 ) | |
3 | ercpbl.f | ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ ) | |
4 | ercpbllem.1 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) | |
5 | 1 2 3 | divsfval | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = [ 𝐴 ] ∼ ) |
6 | 1 2 3 | divsfval | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) = [ 𝐵 ] ∼ ) |
7 | 5 6 | eqeq12d | ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) ↔ [ 𝐴 ] ∼ = [ 𝐵 ] ∼ ) ) |
8 | 1 4 | erth | ⊢ ( 𝜑 → ( 𝐴 ∼ 𝐵 ↔ [ 𝐴 ] ∼ = [ 𝐵 ] ∼ ) ) |
9 | 7 8 | bitr4d | ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) ↔ 𝐴 ∼ 𝐵 ) ) |