Metamath Proof Explorer


Theorem dibf11N

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 dibcl.h 𝐻 = ( LHyp ‘ 𝐾 )
dibcl.i 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
Assertion dibf11N ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐼 : dom 𝐼1-1-onto→ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 dibcl.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dibcl.i 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
3 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
4 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5 3 4 1 2 dibfnN ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐼 Fn { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑥 ( le ‘ 𝐾 ) 𝑊 } )
6 fnfun ( 𝐼 Fn { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑥 ( le ‘ 𝐾 ) 𝑊 } → Fun 𝐼 )
7 funfn ( Fun 𝐼𝐼 Fn dom 𝐼 )
8 6 7 sylib ( 𝐼 Fn { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑥 ( le ‘ 𝐾 ) 𝑊 } → 𝐼 Fn dom 𝐼 )
9 5 8 syl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐼 Fn dom 𝐼 )
10 eqidd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ran 𝐼 = ran 𝐼 )
11 3 4 1 2 dibeldmN ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝑥 ∈ dom 𝐼 ↔ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) ) )
12 3 4 1 2 dibeldmN ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝑦 ∈ dom 𝐼 ↔ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑊 ) ) )
13 11 12 anbi12d ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( 𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼 ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑊 ) ) ) )
14 3 4 1 2 dib11N ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝐼𝑥 ) = ( 𝐼𝑦 ) ↔ 𝑥 = 𝑦 ) )
15 14 biimpd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝐼𝑥 ) = ( 𝐼𝑦 ) → 𝑥 = 𝑦 ) )
16 15 3expib ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝐼𝑥 ) = ( 𝐼𝑦 ) → 𝑥 = 𝑦 ) ) )
17 13 16 sylbid ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( 𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼 ) → ( ( 𝐼𝑥 ) = ( 𝐼𝑦 ) → 𝑥 = 𝑦 ) ) )
18 17 ralrimivv ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ∀ 𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼 ( ( 𝐼𝑥 ) = ( 𝐼𝑦 ) → 𝑥 = 𝑦 ) )
19 dff1o6 ( 𝐼 : dom 𝐼1-1-onto→ ran 𝐼 ↔ ( 𝐼 Fn dom 𝐼 ∧ ran 𝐼 = ran 𝐼 ∧ ∀ 𝑥 ∈ dom 𝐼𝑦 ∈ dom 𝐼 ( ( 𝐼𝑥 ) = ( 𝐼𝑦 ) → 𝑥 = 𝑦 ) ) )
20 9 10 18 19 syl3anbrc ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐼 : dom 𝐼1-1-onto→ ran 𝐼 )