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 )