cdlemg2ce

Description: Utility theorem to eliminate p,q when converting theorems with explicit f. TODO: fix comment. (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))$
	cdlemg2ce.p	$⊢ F = G \to (ψ \leftrightarrow χ)$
	cdlemg2ce.c	$⊢ (((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 φ) \to χ$
Assertion	cdlemg2ce	$⊢ ((K \in HL \land W \in H) \land F \in T \land φ) \to ψ$

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		cdlemg2ce.p	$⊢ F = G \to (ψ \leftrightarrow χ)$
13		cdlemg2ce.c	$⊢ (((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 φ) \to χ$
14		simp2	$⊢ ((K \in HL \land W \in H) \land F \in T \land φ) \to F \in T$
15	1 2 3 4 5 6 7 8 9 10 11	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))$
16	15	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land F \in T \land φ) \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))$
17	14 16	mpbid	$⊢ ((K \in HL \land W \in H) \land F \in T \land φ) \to \exists p \in A \exists q \in A (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G)$
18		simp11	$⊢ (((K \in HL \land W \in H) \land F \in T \land φ) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G)) \to (K \in HL \land W \in H)$
19		simp2l	$⊢ (((K \in HL \land W \in H) \land F \in T \land φ) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G)) \to p \in A$
20		simp31	$⊢ (((K \in HL \land W \in H) \land F \in T \land φ) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G)) \to \neg p \underset{˙}{\leq} W$
21	19 20	jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land φ) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G)) \to (p \in A \land \neg p \underset{˙}{\leq} W)$
22		simp2r	$⊢ (((K \in HL \land W \in H) \land F \in T \land φ) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G)) \to q \in A$
23		simp32	$⊢ (((K \in HL \land W \in H) \land F \in T \land φ) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G)) \to \neg q \underset{˙}{\leq} W$
24	22 23	jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land φ) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G)) \to (q \in A \land \neg q \underset{˙}{\leq} W)$
25		simp13	$⊢ (((K \in HL \land W \in H) \land F \in T \land φ) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G)) \to φ$
26	18 21 24 25 13	syl31anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land φ) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G)) \to χ$
27		simp33	$⊢ (((K \in HL \land W \in H) \land F \in T \land φ) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G)) \to F = G$
28	27 12	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land φ) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G)) \to (ψ \leftrightarrow χ)$
29	26 28	mpbird	$⊢ (((K \in HL \land W \in H) \land F \in T \land φ) \land (p \in A \land q \in A) \land (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G)) \to ψ$
30	29	3exp	$⊢ ((K \in HL \land W \in H) \land F \in T \land φ) \to ((p \in A \land q \in A) \to ((\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G) \to ψ))$
31	30	rexlimdvv	$⊢ ((K \in HL \land W \in H) \land F \in T \land φ) \to (\exists p \in A \exists q \in A (\neg p \underset{˙}{\leq} W \land \neg q \underset{˙}{\leq} W \land F = G) \to ψ)$
32	17 31	mpd	$⊢ ((K \in HL \land W \in H) \land F \in T \land φ) \to ψ$

Metamath Proof Explorer

Theorem cdlemg2ce

Proof