This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdlemg1ci2

Description: Any function of the form of the function constructed for cdleme is a translation. TODO: Fix comment. (Contributed by NM, 18-Apr-2013)

		Ref	Expression
	Hypotheses	cdlemg1c.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		cdlemg1c.a	$⊢ A = Atoms (K)$
		cdlemg1c.h	$⊢ H = LHyp (K)$
		cdlemg1c.t	$⊢ T = LTrn (K) (W)$
	Assertion	cdlemg1ci2	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F = (ι f \in T \| f (P) = Q)) \to F \in T$

Proof

Step	Hyp	Ref	Expression
1		cdlemg1c.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg1c.a	$⊢ A = Atoms (K)$
3		cdlemg1c.h	$⊢ H = LHyp (K)$
4		cdlemg1c.t	$⊢ T = LTrn (K) (W)$
5		simpr	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F = (ι f \in T \| f (P) = Q)) \to F = (ι f \in T \| f (P) = Q)$
6		eqid	$⊢ (ι f \in T \| f (P) = Q) = (ι f \in T \| f (P) = Q)$
7	1 2 3 4 6	ltrniotacl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (ι f \in T \| f (P) = Q) \in T$
8	7	adantr	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F = (ι f \in T \| f (P) = Q)) \to (ι f \in T \| f (P) = Q) \in T$
9	5 8	eqeltrd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F = (ι f \in T \| f (P) = Q)) \to F \in T$