Metamath Proof Explorer


Theorem kqfeq

Description: Two points in the Kolmogorov quotient are equal iff the original points are topologically indistinguishable. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis kqval.2 𝐹 = ( 𝑥𝑋 ↦ { 𝑦𝐽𝑥𝑦 } )
Assertion kqfeq ( ( 𝐽𝑉𝐴𝑋𝐵𝑋 ) → ( ( 𝐹𝐴 ) = ( 𝐹𝐵 ) ↔ ∀ 𝑦𝐽 ( 𝐴𝑦𝐵𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 kqval.2 𝐹 = ( 𝑥𝑋 ↦ { 𝑦𝐽𝑥𝑦 } )
2 1 kqfval ( ( 𝐽𝑉𝐴𝑋 ) → ( 𝐹𝐴 ) = { 𝑦𝐽𝐴𝑦 } )
3 2 3adant3 ( ( 𝐽𝑉𝐴𝑋𝐵𝑋 ) → ( 𝐹𝐴 ) = { 𝑦𝐽𝐴𝑦 } )
4 1 kqfval ( ( 𝐽𝑉𝐵𝑋 ) → ( 𝐹𝐵 ) = { 𝑦𝐽𝐵𝑦 } )
5 4 3adant2 ( ( 𝐽𝑉𝐴𝑋𝐵𝑋 ) → ( 𝐹𝐵 ) = { 𝑦𝐽𝐵𝑦 } )
6 3 5 eqeq12d ( ( 𝐽𝑉𝐴𝑋𝐵𝑋 ) → ( ( 𝐹𝐴 ) = ( 𝐹𝐵 ) ↔ { 𝑦𝐽𝐴𝑦 } = { 𝑦𝐽𝐵𝑦 } ) )
7 rabbi ( ∀ 𝑦𝐽 ( 𝐴𝑦𝐵𝑦 ) ↔ { 𝑦𝐽𝐴𝑦 } = { 𝑦𝐽𝐵𝑦 } )
8 6 7 bitr4di ( ( 𝐽𝑉𝐴𝑋𝐵𝑋 ) → ( ( 𝐹𝐴 ) = ( 𝐹𝐵 ) ↔ ∀ 𝑦𝐽 ( 𝐴𝑦𝐵𝑦 ) ) )