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	$⊢ H = LHyp (K)$
	dibcl.i	$⊢ I = DIsoB (K) (W)$
Assertion	dibf11N	$⊢ (K \in HL \land W \in H) \to I : dom I \underset{1-1 onto}{⟶} ran I$

Proof

Step	Hyp	Ref	Expression
1		dibcl.h	$⊢ H = LHyp (K)$
2		dibcl.i	$⊢ I = DIsoB (K) (W)$
3		eqid	$⊢ {Base}_{K} = {Base}_{K}$
4		eqid	$⊢ \leq_{K} = \leq_{K}$
5	3 4 1 2	dibfnN	$⊢ (K \in HL \land W \in H) \to I Fn \{x \in {Base}_{K} \| x \leq_{K} W\}$
6		fnfun	$⊢ I Fn \{x \in {Base}_{K} \| x \leq_{K} W\} \to Fun I$
7		funfn	$⊢ Fun I \leftrightarrow I Fn dom I$
8	6 7	sylib	$⊢ I Fn \{x \in {Base}_{K} \| x \leq_{K} W\} \to I Fn dom I$
9	5 8	syl	$⊢ (K \in HL \land W \in H) \to I Fn dom I$
10		eqidd	$⊢ (K \in HL \land W \in H) \to ran I = ran I$
11	3 4 1 2	dibeldmN	$⊢ (K \in HL \land W \in H) \to (x \in dom I \leftrightarrow (x \in {Base}_{K} \land x \leq_{K} W))$
12	3 4 1 2	dibeldmN	$⊢ (K \in HL \land W \in H) \to (y \in dom I \leftrightarrow (y \in {Base}_{K} \land y \leq_{K} W))$
13	11 12	anbi12d	$⊢ (K \in HL \land W \in H) \to ((x \in dom I \land y \in dom I) \leftrightarrow ((x \in {Base}_{K} \land x \leq_{K} W) \land (y \in {Base}_{K} \land y \leq_{K} W)))$
14	3 4 1 2	dib11N	$⊢ ((K \in HL \land W \in H) \land (x \in {Base}_{K} \land x \leq_{K} W) \land (y \in {Base}_{K} \land y \leq_{K} W)) \to (I (x) = I (y) \leftrightarrow x = y)$
15	14	biimpd	$⊢ ((K \in HL \land W \in H) \land (x \in {Base}_{K} \land x \leq_{K} W) \land (y \in {Base}_{K} \land y \leq_{K} W)) \to (I (x) = I (y) \to x = y)$
16	15	3expib	$⊢ (K \in HL \land W \in H) \to (((x \in {Base}_{K} \land x \leq_{K} W) \land (y \in {Base}_{K} \land y \leq_{K} W)) \to (I (x) = I (y) \to x = y))$
17	13 16	sylbid	$⊢ (K \in HL \land W \in H) \to ((x \in dom I \land y \in dom I) \to (I (x) = I (y) \to x = y))$
18	17	ralrimivv	$⊢ (K \in HL \land W \in H) \to \forall x \in dom I \forall y \in dom I (I (x) = I (y) \to x = y)$
19		dff1o6	$⊢ I : dom I \underset{1-1 onto}{⟶} ran I \leftrightarrow (I Fn dom I \land ran I = ran I \land \forall x \in dom I \forall y \in dom I (I (x) = I (y) \to x = y))$
20	9 10 18 19	syl3anbrc	$⊢ (K \in HL \land W \in H) \to I : dom I \underset{1-1 onto}{⟶} ran I$

Metamath Proof Explorer

Theorem dibf11N

Proof