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