paddasslem10

	Ref	Expression
Hypotheses	paddasslem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	paddasslem.j	$⊢ \underset{˙}{\lor} = join (K)$
	paddasslem.a	$⊢ A = Atoms (K)$
	paddasslem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
Assertion	paddasslem10	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$

Proof

Step	Hyp	Ref	Expression
1		paddasslem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		paddasslem.j	$⊢ \underset{˙}{\lor} = join (K)$
3		paddasslem.a	$⊢ A = Atoms (K)$
4		paddasslem.p	$⊢ \underset{˙}{+} = +_{𝑃} (K)$
5		simpl11	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to K \in HL$
6		simpl3l	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to p \in A$
7		simpl3r	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to r \in A$
8	5 6 7	3jca	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to (K \in HL \land p \in A \land r \in A)$
9		an6	$⊢ ((X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (x \in X \land y \in Y \land z \in Z)) \leftrightarrow ((X \subseteq A \land x \in X) \land (Y \subseteq A \land y \in Y) \land (Z \subseteq A \land z \in Z))$
10		ssel2	$⊢ (X \subseteq A \land x \in X) \to x \in A$
11		ssel2	$⊢ (Y \subseteq A \land y \in Y) \to y \in A$
12		ssel2	$⊢ (Z \subseteq A \land z \in Z) \to z \in A$
13	10 11 12	3anim123i	$⊢ ((X \subseteq A \land x \in X) \land (Y \subseteq A \land y \in Y) \land (Z \subseteq A \land z \in Z)) \to (x \in A \land y \in A \land z \in A)$
14	9 13	sylbi	$⊢ ((X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (x \in X \land y \in Y \land z \in Z)) \to (x \in A \land y \in A \land z \in A)$
15	14	3ad2antl2	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land (x \in X \land y \in Y \land z \in Z)) \to (x \in A \land y \in A \land z \in A)$
16	15	adantrr	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to (x \in A \land y \in A \land z \in A)$
17		simpl12	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to p \neq z$
18		simpl13	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to x \neq y$
19		simprr1	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y)$
20	17 18 19	3jca	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))$
21		simprr2	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to p \underset{˙}{\leq} (x \underset{˙}{\lor} r)$
22		simprr3	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to r \underset{˙}{\leq} (y \underset{˙}{\lor} z)$
23	1 2 3	paddasslem4	$⊢ (((K \in HL \land p \in A \land r \in A) \land (x \in A \land y \in A \land z \in A) \land (p \neq z \land x \neq y \land \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to \exists s \in A (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))$
24	8 16 20 21 22 23	syl32anc	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to \exists s \in A (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))$
25		simpl2	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to (X \subseteq A \land Y \subseteq A \land Z \subseteq A)$
26		simpl3	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to (p \in A \land r \in A)$
27	5 25 26	3jca	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A))$
28	27	adantr	$⊢ ((((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \land (s \in A \land (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z)))) \to (K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A))$
29		simplrl	$⊢ ((((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \land (s \in A \land (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z)))) \to (x \in X \land y \in Y \land z \in Z)$
30	19 22	jca	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))$
31	30	adantr	$⊢ ((((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \land (s \in A \land (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z)))) \to (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))$
32		simprl	$⊢ ((((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \land (s \in A \land (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z)))) \to s \in A$
33		simprrl	$⊢ ((((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \land (s \in A \land (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z)))) \to s \underset{˙}{\leq} (x \underset{˙}{\lor} y)$
34		simprrr	$⊢ ((((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \land (s \in A \land (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z)))) \to s \underset{˙}{\leq} (p \underset{˙}{\lor} z)$
35	32 33 34	3jca	$⊢ ((((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \land (s \in A \land (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z)))) \to (s \in A \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))$
36	1 2 3 4	paddasslem9	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \land (s \in A \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z)))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$
37	28 29 31 35 36	syl13anc	$⊢ ((((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \land (s \in A \land (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z)))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$
38	24 37	rexlimddv	$⊢ (((K \in HL \land p \neq z \land x \neq y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$

Metamath Proof Explorer

Theorem paddasslem10

Proof