Metamath Proof Explorer

Theorem cdlemg1cN

Description: Any translation belongs to the set of functions constructed for cdleme . TODO: Fix comment. (Contributed by NM, 18-Apr-2013) (New usage is discouraged.)

		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	cdlemg1cN	$⊢ (((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 (P) = Q) \to (F \in T \leftrightarrow F = (ι f \in T \| f (P) = Q))$

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		simpll1	$⊢ ((((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 (P) = Q) \land F \in T) \to (K \in HL \land W \in H)$
6		simpll2	$⊢ ((((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 (P) = Q) \land F \in T) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
7		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 (P) = Q) \land F \in T) \to F \in T$
8	1 2 3 4	cdlemeiota	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T) \to F = (ι f \in T \| f (P) = F (P))$
9	5 6 7 8	syl3anc	$⊢ ((((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 (P) = Q) \land F \in T) \to F = (ι f \in T \| f (P) = F (P))$
10		simplr	$⊢ ((((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 (P) = Q) \land F \in T) \to F (P) = Q$
11	10	eqeq2d	$⊢ ((((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 (P) = Q) \land F \in T) \to (f (P) = F (P) \leftrightarrow f (P) = Q)$
12	11	riotabidv	$⊢ ((((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 (P) = Q) \land F \in T) \to (ι f \in T \| f (P) = F (P)) = (ι f \in T \| f (P) = Q)$
13	9 12	eqtrd	$⊢ ((((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 (P) = Q) \land F \in T) \to F = (ι f \in T \| f (P) = Q)$
14	1 2 3 4	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$
15	14	adantlr	$⊢ ((((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 (P) = Q) \land F = (ι f \in T \| f (P) = Q)) \to F \in T$
16	13 15	impbida	$⊢ (((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 (P) = Q) \to (F \in T \leftrightarrow F = (ι f \in T \| f (P) = Q))$