Metamath Proof Explorer

Theorem f1ocpbllem

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

Ref Expression
Hypothesis f1ocpbl.f ⊢φ→F:V⟶1-1 ontoX
Assertion f1ocpbllem ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→F⁡A=F⁡C∧F⁡B=F⁡D↔A=C∧B=D

Proof

Step Hyp Ref Expression
1 f1ocpbl.f ⊢φ→F:V⟶1-1 ontoX
2 f1of1 ⊢F:V⟶1-1 ontoX→F:V⟶1-1X
3 1 2 syl ⊢φ→F:V⟶1-1X
4 3 3ad2ant1 ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→F:V⟶1-1X
5 simp2l ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→A∈V
6 simp3l ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→C∈V
7 f1fveq ⊢F:V⟶1-1X∧A∈V∧C∈V→F⁡A=F⁡C↔A=C
8 4 5 6 7 syl12anc ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→F⁡A=F⁡C↔A=C
9 simp2r ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→B∈V
10 simp3r ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→D∈V
11 f1fveq ⊢F:V⟶1-1X∧B∈V∧D∈V→F⁡B=F⁡D↔B=D
12 4 9 10 11 syl12anc ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→F⁡B=F⁡D↔B=D
13 8 12 anbi12d ⊢φ∧A∈V∧B∈V∧C∈V∧D∈V→F⁡A=F⁡C∧F⁡B=F⁡D↔A=C∧B=D