cdleme26f

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 6th and 7th lines on p. 115. F , N represent f(t), f_t(s) respectively. If t <_ t \/ v, then f_t(s) <_ f(t) \/ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013)

	Ref	Expression
Hypotheses	cdleme26.b	$⊢ B = {Base}_{K}$
	cdleme26.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme26.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme26.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme26.a	$⊢ A = Atoms (K)$
	cdleme26.h	$⊢ H = LHyp (K)$
	cdleme26f.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme26f.f	$⊢ F = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdleme26f.n	$⊢ N = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((S \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdleme26f.i	$⊢ I = (ι u \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to u = N))$
Assertion	cdleme26f	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to I \underset{˙}{\leq} (F \underset{˙}{\lor} V)$

Proof

Step	Hyp	Ref	Expression
1		cdleme26.b	$⊢ B = {Base}_{K}$
2		cdleme26.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdleme26.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdleme26.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdleme26.a	$⊢ A = Atoms (K)$
6		cdleme26.h	$⊢ H = LHyp (K)$
7		cdleme26f.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
8		cdleme26f.f	$⊢ F = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
9		cdleme26f.n	$⊢ N = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((S \underset{˙}{\lor} t) \underset{˙}{\land} W))$
10		cdleme26f.i	$⊢ I = (ι u \in B \| \forall t \in A ((\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to u = N))$
11		simp11	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to (K \in HL \land W \in H)$
12		simp21	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
13		simp22	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
14		simp23l	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to S \in A$
15		simp23r	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to \neg S \underset{˙}{\leq} W$
16		simp12l	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to P \neq Q$
17		simp12r	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
18	1 2 3 4 5 6 7 8 9 10	cdleme25cl	$⊢ (((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 (S \in A \land \neg S \underset{˙}{\leq} W) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to I \in B$
19	11 12 13 14 15 16 17 18	syl322anc	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to I \in B$
20		simp13l	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to t \in A$
21		simp13r	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to \neg t \underset{˙}{\leq} W$
22		simp31	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
23	1	fvexi	$⊢ B \in V$
24	23 10	riotasv	$⊢ (I \in B \land t \in A \land (\neg t \underset{˙}{\leq} W \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to I = N$
25	19 20 21 22 24	syl112anc	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to I = N$
26		simp23	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
27		simp33	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to (V \in A \land V \underset{˙}{\leq} W)$
28		simp32	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V))$
29	2 3 4 5 6 7 8 9	cdleme22f	$⊢ (((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 ((S \in A \land \neg S \underset{˙}{\leq} W) \land t \in A \land (V \in A \land V \underset{˙}{\leq} W)) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V))) \to N \underset{˙}{\leq} (F \underset{˙}{\lor} V)$
30	11 12 13 26 20 27 28 29	syl331anc	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to N \underset{˙}{\leq} (F \underset{˙}{\lor} V)$
31	25 30	eqbrtrd	$⊢ (((K \in HL \land W \in H) \land (P \neq Q \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (S \neq t \land S \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to I \underset{˙}{\leq} (F \underset{˙}{\lor} V)$

Metamath Proof Explorer

Theorem cdleme26f

Proof