Database
BASIC STRUCTURES
Extensible structures
Definition of the structure quotient
f1ocpbllem
Next ⟩
f1ocpbl
Metamath Proof Explorer
Ascii
Unicode
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