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 ( ( 𝜑 ∧ ( 𝐴𝑉𝐵𝑉 ) ∧ ( 𝐶𝑉𝐷𝑉 ) ) → ( ( ( 𝐹𝐴 ) = ( 𝐹𝐶 ) ∧ ( 𝐹𝐵 ) = ( 𝐹𝐷 ) ) ↔ ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )