# 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}=\mathrm{LHyp}\left({K}\right)$
dia1o.i ${⊢}{I}=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
Assertion diaf11N ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}:\mathrm{dom}{I}\underset{1-1 onto}{⟶}\mathrm{ran}{I}$

### Proof

Step Hyp Ref Expression
1 dia1o.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dia1o.i ${⊢}{I}=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
3 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
4 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
5 3 4 1 2 diafn ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}Fn\left\{{x}\in {\mathrm{Base}}_{{K}}|{x}{\le }_{{K}}{W}\right\}$
6 fnfun ${⊢}{I}Fn\left\{{x}\in {\mathrm{Base}}_{{K}}|{x}{\le }_{{K}}{W}\right\}\to \mathrm{Fun}{I}$
7 funfn ${⊢}\mathrm{Fun}{I}↔{I}Fn\mathrm{dom}{I}$
8 6 7 sylib ${⊢}{I}Fn\left\{{x}\in {\mathrm{Base}}_{{K}}|{x}{\le }_{{K}}{W}\right\}\to {I}Fn\mathrm{dom}{I}$
9 5 8 syl ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}Fn\mathrm{dom}{I}$
10 eqidd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{ran}{I}=\mathrm{ran}{I}$
11 3 4 1 2 diaeldm ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({x}\in \mathrm{dom}{I}↔\left({x}\in {\mathrm{Base}}_{{K}}\wedge {x}{\le }_{{K}}{W}\right)\right)$
12 3 4 1 2 diaeldm ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({y}\in \mathrm{dom}{I}↔\left({y}\in {\mathrm{Base}}_{{K}}\wedge {y}{\le }_{{K}}{W}\right)\right)$
13 11 12 anbi12d ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left(\left({x}\in \mathrm{dom}{I}\wedge {y}\in \mathrm{dom}{I}\right)↔\left(\left({x}\in {\mathrm{Base}}_{{K}}\wedge {x}{\le }_{{K}}{W}\right)\wedge \left({y}\in {\mathrm{Base}}_{{K}}\wedge {y}{\le }_{{K}}{W}\right)\right)\right)$
14 3 4 1 2 dia11N ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge {x}{\le }_{{K}}{W}\right)\wedge \left({y}\in {\mathrm{Base}}_{{K}}\wedge {y}{\le }_{{K}}{W}\right)\right)\to \left({I}\left({x}\right)={I}\left({y}\right)↔{x}={y}\right)$
15 14 biimpd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge {x}{\le }_{{K}}{W}\right)\wedge \left({y}\in {\mathrm{Base}}_{{K}}\wedge {y}{\le }_{{K}}{W}\right)\right)\to \left({I}\left({x}\right)={I}\left({y}\right)\to {x}={y}\right)$
16 15 3expib ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left(\left(\left({x}\in {\mathrm{Base}}_{{K}}\wedge {x}{\le }_{{K}}{W}\right)\wedge \left({y}\in {\mathrm{Base}}_{{K}}\wedge {y}{\le }_{{K}}{W}\right)\right)\to \left({I}\left({x}\right)={I}\left({y}\right)\to {x}={y}\right)\right)$
17 13 16 sylbid ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left(\left({x}\in \mathrm{dom}{I}\wedge {y}\in \mathrm{dom}{I}\right)\to \left({I}\left({x}\right)={I}\left({y}\right)\to {x}={y}\right)\right)$
18 17 ralrimivv ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \forall {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\left({I}\left({x}\right)={I}\left({y}\right)\to {x}={y}\right)$
19 dff1o6 ${⊢}{I}:\mathrm{dom}{I}\underset{1-1 onto}{⟶}\mathrm{ran}{I}↔\left({I}Fn\mathrm{dom}{I}\wedge \mathrm{ran}{I}=\mathrm{ran}{I}\wedge \forall {x}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{dom}{I}\phantom{\rule{.4em}{0ex}}\left({I}\left({x}\right)={I}\left({y}\right)\to {x}={y}\right)\right)$
20 9 10 18 19 syl3anbrc ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}:\mathrm{dom}{I}\underset{1-1 onto}{⟶}\mathrm{ran}{I}$