Metamath Proof Explorer


Theorem ercpbllem

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 ( 𝜑 → ( ( 𝐹𝐴 ) = ( 𝐹𝐵 ) ↔ 𝐴 𝐵 ) )

Proof

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 ( 𝜑 → ( ( 𝐹𝐴 ) = ( 𝐹𝐵 ) ↔ 𝐴 𝐵 ) )