This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ F = x ∈ X ⟼ y ∈ J | x ∈ y
Assertion kqfeq ⊢ J ∈ V ∧ A ∈ X ∧ B ∈ X → F ⁡ A = F ⁡ B ↔ ∀ y ∈ J A ∈ y ↔ B ∈ y

Proof

Step Hyp Ref Expression
1 kqval.2 ⊢ F = x ∈ X ⟼ y ∈ J | x ∈ y
2 1 kqfval ⊢ J ∈ V ∧ A ∈ X → F ⁡ A = y ∈ J | A ∈ y
3 2 3adant3 ⊢ J ∈ V ∧ A ∈ X ∧ B ∈ X → F ⁡ A = y ∈ J | A ∈ y
4 1 kqfval ⊢ J ∈ V ∧ B ∈ X → F ⁡ B = y ∈ J | B ∈ y
5 4 3adant2 ⊢ J ∈ V ∧ A ∈ X ∧ B ∈ X → F ⁡ B = y ∈ J | B ∈ y
6 3 5 eqeq12d ⊢ J ∈ V ∧ A ∈ X ∧ B ∈ X → F ⁡ A = F ⁡ B ↔ y ∈ J | A ∈ y = y ∈ J | B ∈ y
7 rabbi ⊢ ∀ y ∈ J A ∈ y ↔ B ∈ y ↔ y ∈ J | A ∈ y = y ∈ J | B ∈ y
8 6 7 bitr4di ⊢ J ∈ V ∧ A ∈ X ∧ B ∈ X → F ⁡ A = F ⁡ B ↔ ∀ y ∈ J A ∈ y ↔ B ∈ y