paddasslem14

	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	paddasslem14	$⊢ ((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 (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	1 2 3 4	paddasslem11	$⊢ (((K \in HL \land p = z) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \land z \in Z) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$
6	5	3ad2antr3	$⊢ (((K \in HL \land p = z) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \land (x \in X \land y \in Y \land z \in Z)) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$
7	6	ex	$⊢ ((K \in HL \land p = z) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to ((x \in X \land y \in Y \land z \in Z) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))$
8	7	adantrd	$⊢ ((K \in HL \land p = z) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to (((x \in X \land y \in Y \land z \in Z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))$
9	8	a1d	$⊢ ((K \in HL \land p = z) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A)) \to ((p \in A \land r \in A) \to (((x \in X \land y \in Y \land z \in Z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)))$
10	9	exp31	$⊢ K \in HL \to (p = z \to ((X \subseteq A \land Y \subseteq A \land Z \subseteq A) \to ((p \in A \land r \in A) \to (((x \in X \land y \in Y \land z \in Z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)))))$
11		3simpb	$⊢ (K \in HL \land p \neq z \land x = y) \to (K \in HL \land x = y)$
12	11	3anim1i	$⊢ ((K \in HL \land p \neq z \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \to ((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A))$
13		3simpc	$⊢ (x \in X \land y \in Y \land z \in Z) \to (y \in Y \land z \in Z)$
14	13	anim1i	$⊢ ((x \in X \land y \in Y \land z \in Z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to ((y \in Y \land z \in Z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))$
15	1 2 3 4	paddasslem12	$⊢ (((K \in HL \land x = y) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A)) \land ((y \in Y \land z \in Z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$
16	12 14 15	syl2an	$⊢ (((K \in HL \land p \neq z \land x = 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 (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$
17	16	3exp1	$⊢ (K \in HL \land p \neq z \land x = y) \to ((X \subseteq A \land Y \subseteq A \land Z \subseteq A) \to ((p \in A \land r \in A) \to (((x \in X \land y \in Y \land z \in Z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))))$
18	17	3expia	$⊢ (K \in HL \land p \neq z) \to (x = y \to ((X \subseteq A \land Y \subseteq A \land Z \subseteq A) \to ((p \in A \land r \in A) \to (((x \in X \land y \in Y \land z \in Z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)))))$
19		3simpa	$⊢ (K \in HL \land p \neq z \land x \neq y) \to (K \in HL \land p \neq z)$
20	19	3anim1i	$⊢ ((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)) \to ((K \in HL \land p \neq z) \land (X \subseteq A \land Y \subseteq A \land Z \subseteq A) \land (p \in A \land r \in A))$
21		3simpa	$⊢ (x \in X \land y \in Y \land z \in Z) \to (x \in X \land y \in Y)$
22		3simpa	$⊢ (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} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r))$
23	21 22	anim12i	$⊢ ((x \in X \land y \in Y \land z \in Z) \land (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 X \land y \in Y) \land (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))$
24	1 2 3 4	paddasslem13	$⊢ (((K \in HL \land p \neq z) \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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land p \underset{˙}{\leq} (x \underset{˙}{\lor} r)))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)$
25	20 23 24	syl2an	$⊢ (((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 (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)$
26	25	expr	$⊢ (((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 ((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))$
27	26	3expd	$⊢ (((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 (r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \to (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \to (r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))))$
28	1 2 3 4	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)$
29	28	expr	$⊢ (((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 ((\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))$
30	29	3expd	$⊢ (((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 (\neg r \underset{˙}{\leq} (x \underset{˙}{\lor} y) \to (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \to (r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))))$
31	27 30	pm2.61d	$⊢ (((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 (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \to (r \underset{˙}{\leq} (y \underset{˙}{\lor} z) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)))$
32	31	impd	$⊢ (((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 ((p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z)) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))$
33	32	expimpd	$⊢ ((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)) \to (((x \in X \land y \in Y \land z \in Z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))$
34	33	3exp	$⊢ (K \in HL \land p \neq z \land x \neq y) \to ((X \subseteq A \land Y \subseteq A \land Z \subseteq A) \to ((p \in A \land r \in A) \to (((x \in X \land y \in Y \land z \in Z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))))$
35	34	3expia	$⊢ (K \in HL \land p \neq z) \to (x \neq y \to ((X \subseteq A \land Y \subseteq A \land Z \subseteq A) \to ((p \in A \land r \in A) \to (((x \in X \land y \in Y \land z \in Z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)))))$
36	18 35	pm2.61dne	$⊢ (K \in HL \land p \neq z) \to ((X \subseteq A \land Y \subseteq A \land Z \subseteq A) \to ((p \in A \land r \in A) \to (((x \in X \land y \in Y \land z \in Z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))))$
37	36	ex	$⊢ K \in HL \to (p \neq z \to ((X \subseteq A \land Y \subseteq A \land Z \subseteq A) \to ((p \in A \land r \in A) \to (((x \in X \land y \in Y \land z \in Z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z)))))$
38	10 37	pm2.61dne	$⊢ K \in HL \to ((X \subseteq A \land Y \subseteq A \land Z \subseteq A) \to ((p \in A \land r \in A) \to (((x \in X \land y \in Y \land z \in Z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land r \underset{˙}{\leq} (y \underset{˙}{\lor} z))) \to p \in ((X \underset{˙}{+} Y) \underset{˙}{+} Z))))$
39	38	3imp1	$⊢ ((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 (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 paddasslem14

Proof