Step |
Hyp |
Ref |
Expression |
1 |
|
ltrnatb.b |
|- B = ( Base ` K ) |
2 |
|
ltrnatb.a |
|- A = ( Atoms ` K ) |
3 |
|
ltrnatb.h |
|- H = ( LHyp ` K ) |
4 |
|
ltrnatb.t |
|- T = ( ( LTrn ` K ) ` W ) |
5 |
1 3 4
|
ltrn1o |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F : B -1-1-onto-> B ) |
6 |
|
f1ocnvdm |
|- ( ( F : B -1-1-onto-> B /\ P e. B ) -> ( `' F ` P ) e. B ) |
7 |
5 6
|
stoic3 |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( `' F ` P ) e. B ) |
8 |
1 2 3 4
|
ltrnatb |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( `' F ` P ) e. B ) -> ( ( `' F ` P ) e. A <-> ( F ` ( `' F ` P ) ) e. A ) ) |
9 |
7 8
|
syld3an3 |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( ( `' F ` P ) e. A <-> ( F ` ( `' F ` P ) ) e. A ) ) |
10 |
|
f1ocnvfv2 |
|- ( ( F : B -1-1-onto-> B /\ P e. B ) -> ( F ` ( `' F ` P ) ) = P ) |
11 |
5 10
|
stoic3 |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( F ` ( `' F ` P ) ) = P ) |
12 |
11
|
eleq1d |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( ( F ` ( `' F ` P ) ) e. A <-> P e. A ) ) |
13 |
9 12
|
bitr2d |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( P e. A <-> ( `' F ` P ) e. A ) ) |