paddasslem9

	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	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)$

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		simpl1	$⊢ ((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 K \in HL$
6		simpl2	$⊢ ((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 (X \subseteq A \land Y \subseteq A \land Z \subseteq A)$
7		simpl3l	$⊢ ((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 A$
8		simpr31	$⊢ ((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 s \in A$
9	7 8	jca	$⊢ ((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 A \land s \in A)$
10		simpr1	$⊢ ((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 (x \in X \land y \in Y \land z \in Z)$
11		simpr32	$⊢ ((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 s \underset{˙}{\leq} (x \underset{˙}{\lor} y)$
12		simpl3r	$⊢ ((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 r \in A$
13	7 12 8	3jca	$⊢ ((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 A \land r \in A \land s \in A)$
14		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))$
15		ssel2	$⊢ (X \subseteq A \land x \in X) \to x \in A$
16		ssel2	$⊢ (Y \subseteq A \land y \in Y) \to y \in A$
17		ssel2	$⊢ (Z \subseteq A \land z \in Z) \to z \in A$
18	15 16 17	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)$
19	14 18	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)$
20	19	3ad2antl2	$⊢ ((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)) \to (x \in A \land y \in A \land z \in A)$
21	20	3ad2antr1	$⊢ ((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 (x \in A \land y \in A \land z \in A)$
22		simpr2l	$⊢ ((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 \neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y)$
23		simpr2r	$⊢ ((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 r \underset{˙}{\leq} (y \underset{˙}{\lor} z)$
24	22 23 11	3jca	$⊢ ((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 (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y))$
25		simpr33	$⊢ ((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 s \underset{˙}{\leq} (p \underset{˙}{\lor} z)$
26	1 2 3	paddasslem7	$⊢ ((K \in HL \land (p \in A \land r \in A \land s \in A) \land (x \in A \land y \in A \land z \in A)) \land ((\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y)) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))) \to p \underset{˙}{\leq} (s \underset{˙}{\lor} z)$
27	5 13 21 24 25 26	syl32anc	$⊢ ((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 \underset{˙}{\leq} (s \underset{˙}{\lor} z)$
28	1 2 3 4	paddasslem8	$⊢ ((K \in HL \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land s \in A)) \land ((x \in X \land y \in Y \land z \in Z) \land s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (s \underset{˙}{\lor} z))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$
29	5 6 9 10 11 27 28	syl33anc	$⊢ ((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)$

Metamath Proof Explorer

Theorem paddasslem9

Proof