4atexlem7

Description: Whenever there are at least 4 atoms under P .\/ Q (specifically, P , Q , r , and ( P .\/ Q ) ./\ W ), there are also at least 4 atoms under P .\/ S . This proves the statement in Lemma E of Crawley p. 114, last line, "...p \/ q/0 and hence p \/ s/0 contains at least four atoms..." Note that by cvlsupr2 , our ( P .\/ r ) = ( Q .\/ r ) is a shorter way to express r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) . With a longer proof, the condition -. S .<_ ( P .\/ Q ) could be eliminated (see 4atex ), although for some purposes this more restricted lemma may be adequate. (Contributed by NM, 25-Nov-2012)

	Ref	Expression
Hypotheses	4that.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	4that.j	$⊢ \underset{˙}{\lor} = join (K)$
	4that.a	$⊢ A = Atoms (K)$
	4that.h	$⊢ H = LHyp (K)$
Assertion	4atexlem7	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)$

Proof

Step	Hyp	Ref	Expression
1		4that.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		4that.j	$⊢ \underset{˙}{\lor} = join (K)$
3		4that.a	$⊢ A = Atoms (K)$
4		4that.h	$⊢ H = LHyp (K)$
5		simp11l	$⊢ ((((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r)) \to (K \in HL \land W \in H)$
6		simp1r1	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
7	6	3ad2ant1	$⊢ ((((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
8		simp1r2	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
9	8	3ad2ant1	$⊢ ((((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
10		simp2	$⊢ ((((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r)) \to r \in A$
11		simp3l	$⊢ ((((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r)) \to \neg r \underset{˙}{\leq} W$
12	10 11	jca	$⊢ ((((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r)) \to (r \in A \land \neg r \underset{˙}{\leq} W)$
13		simp1r3	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \in A$
14	13	3ad2ant1	$⊢ ((((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r)) \to S \in A$
15		simp3r	$⊢ ((((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r)) \to P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r$
16		simp12	$⊢ ((((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r)) \to P \neq Q$
17		simp13	$⊢ ((((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r)) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
18		eqid	$⊢ meet (K) = meet (K)$
19	1 2 18 3 4	4atexlemex6	$⊢ (((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 ((r \in A \land \neg r \underset{˙}{\leq} W) \land S \in A) \land (P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)$
20	5 7 9 12 14 15 16 17 19	syl323anc	$⊢ ((((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land r \in A \land (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r)) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)$
21	20	rexlimdv3a	$⊢ (((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 P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (\exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z))$
22	21	3exp	$⊢ ((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)) \to (P \neq Q \to (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to (\exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z))))$
23	22	3impd	$⊢ ((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)) \to ((P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r)) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z))$
24	23	3impia	$⊢ ((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 (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \exists r \in A (\neg r \underset{˙}{\leq} W \land P \underset{˙}{\lor} r = Q \underset{˙}{\lor} r))) \to \exists z \in A (\neg z \underset{˙}{\leq} W \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)$

Metamath Proof Explorer

Theorem 4atexlem7

Proof