Metamath Proof Explorer


Theorem diaf11N

Description: The partial isomorphism A for a lattice K is a one-to-one function. Part of Lemma M of Crawley p. 120 line 27. (Contributed by NM, 4-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses dia1o.h
|- H = ( LHyp ` K )
dia1o.i
|- I = ( ( DIsoA ` K ) ` W )
Assertion diaf11N
|- ( ( K e. HL /\ W e. H ) -> I : dom I -1-1-onto-> ran I )

Proof

Step Hyp Ref Expression
1 dia1o.h
 |-  H = ( LHyp ` K )
2 dia1o.i
 |-  I = ( ( DIsoA ` K ) ` W )
3 eqid
 |-  ( Base ` K ) = ( Base ` K )
4 eqid
 |-  ( le ` K ) = ( le ` K )
5 3 4 1 2 diafn
 |-  ( ( K e. HL /\ W e. H ) -> I Fn { x e. ( Base ` K ) | x ( le ` K ) W } )
6 fnfun
 |-  ( I Fn { x e. ( Base ` K ) | x ( le ` K ) W } -> Fun I )
7 funfn
 |-  ( Fun I <-> I Fn dom I )
8 6 7 sylib
 |-  ( I Fn { x e. ( Base ` K ) | x ( le ` K ) W } -> I Fn dom I )
9 5 8 syl
 |-  ( ( K e. HL /\ W e. H ) -> I Fn dom I )
10 eqidd
 |-  ( ( K e. HL /\ W e. H ) -> ran I = ran I )
11 3 4 1 2 diaeldm
 |-  ( ( K e. HL /\ W e. H ) -> ( x e. dom I <-> ( x e. ( Base ` K ) /\ x ( le ` K ) W ) ) )
12 3 4 1 2 diaeldm
 |-  ( ( K e. HL /\ W e. H ) -> ( y e. dom I <-> ( y e. ( Base ` K ) /\ y ( le ` K ) W ) ) )
13 11 12 anbi12d
 |-  ( ( K e. HL /\ W e. H ) -> ( ( x e. dom I /\ y e. dom I ) <-> ( ( x e. ( Base ` K ) /\ x ( le ` K ) W ) /\ ( y e. ( Base ` K ) /\ y ( le ` K ) W ) ) ) )
14 3 4 1 2 dia11N
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. ( Base ` K ) /\ x ( le ` K ) W ) /\ ( y e. ( Base ` K ) /\ y ( le ` K ) W ) ) -> ( ( I ` x ) = ( I ` y ) <-> x = y ) )
15 14 biimpd
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. ( Base ` K ) /\ x ( le ` K ) W ) /\ ( y e. ( Base ` K ) /\ y ( le ` K ) W ) ) -> ( ( I ` x ) = ( I ` y ) -> x = y ) )
16 15 3expib
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( x e. ( Base ` K ) /\ x ( le ` K ) W ) /\ ( y e. ( Base ` K ) /\ y ( le ` K ) W ) ) -> ( ( I ` x ) = ( I ` y ) -> x = y ) ) )
17 13 16 sylbid
 |-  ( ( K e. HL /\ W e. H ) -> ( ( x e. dom I /\ y e. dom I ) -> ( ( I ` x ) = ( I ` y ) -> x = y ) ) )
18 17 ralrimivv
 |-  ( ( K e. HL /\ W e. H ) -> A. x e. dom I A. y e. dom I ( ( I ` x ) = ( I ` y ) -> x = y ) )
19 dff1o6
 |-  ( I : dom I -1-1-onto-> ran I <-> ( I Fn dom I /\ ran I = ran I /\ A. x e. dom I A. y e. dom I ( ( I ` x ) = ( I ` y ) -> x = y ) ) )
20 9 10 18 19 syl3anbrc
 |-  ( ( K e. HL /\ W e. H ) -> I : dom I -1-1-onto-> ran I )