cdlemg2cex

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, 22-Apr-2013)

	Ref	Expression
Hypotheses	cdlemg2.b	$⊢ B = {Base}_{K}$
	cdlemg2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg2.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemg2.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemg2.a	$⊢ A = Atoms (K)$
	cdlemg2.h	$⊢ H = LHyp (K)$
	cdlemg2.t	$⊢ T = LTrn (K) (W)$
	cdlemg2ex.u	$⊢ U = (p \underset{˙}{\lor} q) \underset{˙}{\land} W$
	cdlemg2ex.d	$⊢ D = (t \underset{˙}{\lor} U) \underset{˙}{\land} (q \underset{˙}{\lor} ((p \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdlemg2ex.e	$⊢ E = (p \underset{˙}{\lor} q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdlemg2ex.g	$⊢ G = (x \in B ⟼ if ((p \neq q \land \neg x \underset{˙}{\leq} W), (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (x \underset{˙}{\land} W) = x) \to z = if (s \underset{˙}{\leq} (p \underset{˙}{\lor} q), (ι y \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (p \underset{˙}{\lor} q)) \to y = E)), ⦋ s / t ⦌ D) \underset{˙}{\lor} (x \underset{˙}{\land} W))), x))$
Assertion	cdlemg2cex	$⊢ (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 = G))$

Proof

Step	Hyp	Ref	Expression
1		cdlemg2.b	$⊢ B = {Base}_{K}$
2		cdlemg2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemg2.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemg2.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemg2.a	$⊢ A = Atoms (K)$
6		cdlemg2.h	$⊢ H = LHyp (K)$
7		cdlemg2.t	$⊢ T = LTrn (K) (W)$
8		cdlemg2ex.u	$⊢ U = (p \underset{˙}{\lor} q) \underset{˙}{\land} W$
9		cdlemg2ex.d	$⊢ D = (t \underset{˙}{\lor} U) \underset{˙}{\land} (q \underset{˙}{\lor} ((p \underset{˙}{\lor} t) \underset{˙}{\land} W))$
10		cdlemg2ex.e	$⊢ E = (p \underset{˙}{\lor} q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} t) \underset{˙}{\land} W))$
11		cdlemg2ex.g	$⊢ G = (x \in B ⟼ if ((p \neq q \land \neg x \underset{˙}{\leq} W), (ι z \in B \| \forall s \in A ((\neg s \underset{˙}{\leq} W \land s \underset{˙}{\lor} (x \underset{˙}{\land} W) = x) \to z = if (s \underset{˙}{\leq} (p \underset{˙}{\lor} q), (ι y \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (p \underset{˙}{\lor} q)) \to y = E)), ⦋ s / t ⦌ D) \underset{˙}{\lor} (x \underset{˙}{\land} W))), x))$
12	2 5 6 7	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)))$
13		simplll	$⊢ (((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)) \to K \in HL$
14		simpllr	$⊢ (((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)) \to W \in H$
15		simplrl	$⊢ (((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)) \to p \in A$
16		simprl	$⊢ (((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)) \to \neg p \underset{˙}{\leq} W$
17		simplrr	$⊢ (((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)) \to q \in A$
18		simprr	$⊢ (((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)) \to \neg q \underset{˙}{\leq} W$
19		eqid	$⊢ (ι f \in T \| f (p) = q) = (ι f \in T \| f (p) = q)$
20	1 2 3 4 5 6 8 9 10 11 7 19	cdlemg1b2	$⊢ ((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) = G$
21	13 14 15 16 17 18 20	syl222anc	$⊢ (((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)) \to (ι f \in T \| f (p) = q) = G$
22	21	eqeq2d	$⊢ (((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)) \to (F = (ι f \in T \| f (p) = q) \leftrightarrow F = G)$
23	22	pm5.32da	$⊢ ((K \in HL \land W \in H) \land (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)) \leftrightarrow ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land F = G))$
24		df-3an	$⊢ (\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 q \underset{˙}{\leq} W) \land F = (ι f \in T \| f (p) = q))$
25		df-3an	$⊢ (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G) \leftrightarrow ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W) \land F = G)$
26	23 24 25	3bitr4g	$⊢ ((K \in HL \land W \in H) \land (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)) \leftrightarrow (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G))$
27	26	2rexbidva	$⊢ (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)) \leftrightarrow \exists p \in A \exists q \in A (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G))$
28	12 27	bitrd	$⊢ (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 = G))$

Metamath Proof Explorer

Theorem cdlemg2cex

Proof