Metamath Proof Explorer

Theorem cdlemfnid

Description: cdlemf with additional constraint of non-identity. (Contributed by NM, 20-Jun-2013)

		Ref	Expression
	Hypotheses	cdlemfnid.b	$⊢ B = {Base}_{K}$
		cdlemfnid.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		cdlemfnid.a	$⊢ A = Atoms (K)$
		cdlemfnid.h	$⊢ H = LHyp (K)$
		cdlemfnid.t	$⊢ T = LTrn (K) (W)$
		cdlemfnid.r	$⊢ R = trL (K) (W)$
	Assertion	cdlemfnid	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \to \exists f \in T (R (f) = U \land f \neq {I ↾}_{B})$

Proof

Step	Hyp	Ref	Expression
1		cdlemfnid.b	$⊢ B = {Base}_{K}$
2		cdlemfnid.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemfnid.a	$⊢ A = Atoms (K)$
4		cdlemfnid.h	$⊢ H = LHyp (K)$
5		cdlemfnid.t	$⊢ T = LTrn (K) (W)$
6		cdlemfnid.r	$⊢ R = trL (K) (W)$
7	2 3 4 5 6	cdlemf	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \to \exists f \in T R (f) = U$
8		simp3	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land f \in T \land R (f) = U) \to R (f) = U$
9		simp1rl	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land f \in T \land R (f) = U) \to U \in A$
10	8 9	eqeltrd	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land f \in T \land R (f) = U) \to R (f) \in A$
11		simp1l	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land f \in T \land R (f) = U) \to (K \in HL \land W \in H)$
12		simp2	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land f \in T \land R (f) = U) \to f \in T$
13	1 3 4 5 6	trlnidatb	$⊢ ((K \in HL \land W \in H) \land f \in T) \to (f \neq {I ↾}_{B} \leftrightarrow R (f) \in A)$
14	11 12 13	syl2anc	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land f \in T \land R (f) = U) \to (f \neq {I ↾}_{B} \leftrightarrow R (f) \in A)$
15	10 14	mpbird	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land f \in T \land R (f) = U) \to f \neq {I ↾}_{B}$
16	8 15	jca	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land f \in T \land R (f) = U) \to (R (f) = U \land f \neq {I ↾}_{B})$
17	16	3expia	$⊢ (((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \land f \in T) \to (R (f) = U \to (R (f) = U \land f \neq {I ↾}_{B}))$
18	17	reximdva	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \to (\exists f \in T R (f) = U \to \exists f \in T (R (f) = U \land f \neq {I ↾}_{B}))$
19	7 18	mpd	$⊢ ((K \in HL \land W \in H) \land (U \in A \land U \underset{˙}{\leq} W)) \to \exists f \in T (R (f) = U \land f \neq {I ↾}_{B})$