cdlemg1cex

Description: Any translation is one of our F s. TODO: fix comment, move to its own block maybe? Would this help for cdlemf ? (Contributed by NM, 17-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	cdlemg1cex	$⊢ (K \in HL \land W \in H) \to (F \in T \leftrightarrow \exists p \in A \exists q \in A (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land 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	1 2 3 4	ltrnel	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in A \land \neg p \underset{˙}{\leq} W)) \to (F (p) \in A \land \neg F (p) \underset{˙}{\leq} W)$
6	5	3expa	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \to (F (p) \in A \land \neg F (p) \underset{˙}{\leq} W)$
7	6	simpld	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \to F (p) \in A$
8		simprr	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \to \neg p \underset{˙}{\leq} W$
9	6	simprd	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \to \neg F (p) \underset{˙}{\leq} W$
10		simpll	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
11		simpr	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \to (p \in A \land \neg p \underset{˙}{\leq} W)$
12		simplr	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \to F \in T$
13	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))$
14	10 11 12 13	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \to F = (ι f \in T \| f (p) = F (p))$
15		breq1	$⊢ q = F (p) \to (q \underset{˙}{\leq} W \leftrightarrow F (p) \underset{˙}{\leq} W)$
16	15	notbid	$⊢ q = F (p) \to (\neg q \underset{˙}{\leq} W \leftrightarrow \neg F (p) \underset{˙}{\leq} W)$
17		eqeq2	$⊢ q = F (p) \to (f (p) = q \leftrightarrow f (p) = F (p))$
18	17	riotabidv	$⊢ q = F (p) \to (ι f \in T \| f (p) = q) = (ι f \in T \| f (p) = F (p))$
19	18	eqeq2d	$⊢ q = F (p) \to (F = (ι f \in T \| f (p) = q) \leftrightarrow F = (ι f \in T \| f (p) = F (p)))$
20	16 19	3anbi23d	$⊢ q = F (p) \to ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = q)) \leftrightarrow (\neg p \underset{˙}{\leq} W \land \neg F (p) \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = F (p))))$
21	20	rspcev	$⊢ (F (p) \in A \land (\neg p \underset{˙}{\leq} W \land \neg F (p) \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = F (p)))) \to \exists q \in A (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = q))$
22	7 8 9 14 21	syl13anc	$⊢ (((K \in HL \land W \in H) \land F \in T) \land (p \in A \land \neg p \underset{˙}{\leq} W)) \to \exists q \in A (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = q))$
23	1 2 3	lhpexnle	$⊢ (K \in HL \land W \in H) \to \exists p \in A \neg p \underset{˙}{\leq} W$
24	23	adantr	$⊢ ((K \in HL \land W \in H) \land F \in T) \to \exists p \in A \neg p \underset{˙}{\leq} W$
25	22 24	reximddv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to \exists p \in A \exists q \in A (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = q))$
26	25	ex	$⊢ (K \in HL \land W \in H) \to (F \in T \to \exists p \in A \exists q \in A (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = q)))$
27		simp1	$⊢ ((K \in HL \land W \in H) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = q))) \to (K \in HL \land W \in H)$
28		simp2l	$⊢ ((K \in HL \land W \in H) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = q))) \to p \in A$
29		simp31	$⊢ ((K \in HL \land W \in H) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = q))) \to \neg p \underset{˙}{\leq} W$
30	28 29	jca	$⊢ ((K \in HL \land W \in H) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = q))) \to (p \in A \land \neg p \underset{˙}{\leq} W)$
31		simp2r	$⊢ ((K \in HL \land W \in H) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = q))) \to q \in A$
32		simp32	$⊢ ((K \in HL \land W \in H) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = q))) \to \neg q \underset{˙}{\leq} W$
33	31 32	jca	$⊢ ((K \in HL \land W \in H) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = q))) \to (q \in A \land \neg q \underset{˙}{\leq} W)$
34		simp33	$⊢ ((K \in HL \land W \in H) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = q))) \to F = (ι f \in T \| f (p) = q)$
35	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$
36	27 30 33 34 35	syl31anc	$⊢ ((K \in HL \land W \in H) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = q))) \to F \in T$
37	36	3exp	$⊢ (K \in HL \land W \in H) \to ((p \in A \land q \in A) \to ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = q)) \to F \in T))$
38	37	rexlimdvv	$⊢ (K \in HL \land W \in H) \to (\exists p \in A \exists q \in A (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = q)) \to F \in T)$
39	26 38	impbid	$⊢ (K \in HL \land W \in H) \to (F \in T \leftrightarrow \exists p \in A \exists q \in A (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = (ι f \in T \| f (p) = q)))$

Metamath Proof Explorer

Theorem cdlemg1cex

Proof