Theorem mapdcnv11N

Description: The converse of the map defined by df-mapd is one-to-one. (Contributed by NM, 13-Mar-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapdcnvord.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	mapdcnvord.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
	mapdcnvord.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	mapdcnvord.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝑀 )
	mapdcnvord.y	⊢ ( 𝜑 → 𝑌 ∈ ran 𝑀 )
Assertion	mapdcnv11N	⊢ ( 𝜑 → ( ( ◡ 𝑀 ‘ 𝑋 ) = ( ◡ 𝑀 ‘ 𝑌 ) ↔ 𝑋 = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		mapdcnvord.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		mapdcnvord.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
3		mapdcnvord.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
4		mapdcnvord.x	⊢ ( 𝜑 → 𝑋 ∈ ran 𝑀 )
5		mapdcnvord.y	⊢ ( 𝜑 → 𝑌 ∈ ran 𝑀 )
6	1 2 3 4 5	mapdcnvordN	⊢ ( 𝜑 → ( ( ◡ 𝑀 ‘ 𝑋 ) ⊆ ( ◡ 𝑀 ‘ 𝑌 ) ↔ 𝑋 ⊆ 𝑌 ) )
7	1 2 3 5 4	mapdcnvordN	⊢ ( 𝜑 → ( ( ◡ 𝑀 ‘ 𝑌 ) ⊆ ( ◡ 𝑀 ‘ 𝑋 ) ↔ 𝑌 ⊆ 𝑋 ) )
8	6 7	anbi12d	⊢ ( 𝜑 → ( ( ( ◡ 𝑀 ‘ 𝑋 ) ⊆ ( ◡ 𝑀 ‘ 𝑌 ) ∧ ( ◡ 𝑀 ‘ 𝑌 ) ⊆ ( ◡ 𝑀 ‘ 𝑋 ) ) ↔ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 ⊆ 𝑋 ) ) )
9		eqss	⊢ ( ( ◡ 𝑀 ‘ 𝑋 ) = ( ◡ 𝑀 ‘ 𝑌 ) ↔ ( ( ◡ 𝑀 ‘ 𝑋 ) ⊆ ( ◡ 𝑀 ‘ 𝑌 ) ∧ ( ◡ 𝑀 ‘ 𝑌 ) ⊆ ( ◡ 𝑀 ‘ 𝑋 ) ) )
10		eqss	⊢ ( 𝑋 = 𝑌 ↔ ( 𝑋 ⊆ 𝑌 ∧ 𝑌 ⊆ 𝑋 ) )
11	8 9 10	3bitr4g	⊢ ( 𝜑 → ( ( ◡ 𝑀 ‘ 𝑋 ) = ( ◡ 𝑀 ‘ 𝑌 ) ↔ 𝑋 = 𝑌 ) )