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

Metamath Proof Explorer

Theorem f1ocpbllem

Description: Lemma for f1ocpbl . (Contributed by Mario Carneiro, 24-Feb-2015)

		Ref	Expression
	Hypothesis	f1ocpbl.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝑋 )
	Assertion	f1ocpbllem	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) ∧ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐷 ) ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		f1ocpbl.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1-onto→ 𝑋 )
2		f1of1	⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑋 → 𝐹 : 𝑉 –1-1→ 𝑋 )
3	1 2	syl	⊢ ( 𝜑 → 𝐹 : 𝑉 –1-1→ 𝑋 )
4	3	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐹 : 𝑉 –1-1→ 𝑋 )
5		simp2l	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑉 )
6		simp3l	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐶 ∈ 𝑉 )
7		f1fveq	⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑋 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) ↔ 𝐴 = 𝐶 ) )
8	4 5 6 7	syl12anc	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) ↔ 𝐴 = 𝐶 ) )
9		simp2r	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
10		simp3r	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐷 ∈ 𝑉 )
11		f1fveq	⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑋 ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐷 ) ↔ 𝐵 = 𝐷 ) )
12	4 9 10 11	syl12anc	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐷 ) ↔ 𝐵 = 𝐷 ) )
13	8 12	anbi12d	⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) ∧ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐷 ) ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )