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	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
	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	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ↔ 𝐵 ∈ 𝑦 ) ) )