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 ⊢ φ → F : V ⟶ 1-1 onto X
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 onto X
2 f1of1 ⊢ F : V ⟶ 1-1 onto X → F : V ⟶ 1-1 X
3 1 2 syl ⊢ φ → F : V ⟶ 1-1 X
4 3 3ad2ant1 ⊢ φ ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → F : V ⟶ 1-1 X
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-1 X ∧ 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-1 X ∧ 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