mdsymlem2

Description: Lemma for mdsymi . (Contributed by NM, 1-Jul-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdsymlem1.1	$⊢ A \in C_{ℋ}$
	mdsymlem1.2	$⊢ B \in C_{ℋ}$
	mdsymlem1.3	$⊢ C = A \lor_{ℋ} p$
Assertion	mdsymlem2	$⊢ ((p \in HAtoms \land B \cap C \subseteq A) \land (B 𝑀_{ℋ}^{*} A \land p \subseteq A \lor_{ℋ} B)) \to (B \neq 0_{ℋ} \to \exists r \in HAtoms \exists q \in HAtoms (p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)))$

Proof

Step	Hyp	Ref	Expression
1		mdsymlem1.1	$⊢ A \in C_{ℋ}$
2		mdsymlem1.2	$⊢ B \in C_{ℋ}$
3		mdsymlem1.3	$⊢ C = A \lor_{ℋ} p$
4	2	hatomici	$⊢ B \neq 0_{ℋ} \to \exists r \in HAtoms r \subseteq B$
5		simplll	$⊢ (((p \in HAtoms \land B \cap C \subseteq A) \land (B 𝑀_{ℋ}^{*} A \land p \subseteq A \lor_{ℋ} B)) \land (r \in HAtoms \land r \subseteq B)) \to p \in HAtoms$
6		atelch	$⊢ p \in HAtoms \to p \in C_{ℋ}$
7		atelch	$⊢ r \in HAtoms \to r \in C_{ℋ}$
8		chub1	$⊢ (p \in C_{ℋ} \land r \in C_{ℋ}) \to p \subseteq p \lor_{ℋ} r$
9	6 7 8	syl2an	$⊢ (p \in HAtoms \land r \in HAtoms) \to p \subseteq p \lor_{ℋ} r$
10	9	adantlr	$⊢ ((p \in HAtoms \land B \cap C \subseteq A) \land r \in HAtoms) \to p \subseteq p \lor_{ℋ} r$
11	10	adantlr	$⊢ (((p \in HAtoms \land B \cap C \subseteq A) \land (B 𝑀_{ℋ}^{*} A \land p \subseteq A \lor_{ℋ} B)) \land r \in HAtoms) \to p \subseteq p \lor_{ℋ} r$
12	1 2 3	mdsymlem1	$⊢ ((p \in C_{ℋ} \land B \cap C \subseteq A) \land (B 𝑀_{ℋ}^{*} A \land p \subseteq A \lor_{ℋ} B)) \to p \subseteq A$
13	6 12	sylanl1	$⊢ ((p \in HAtoms \land B \cap C \subseteq A) \land (B 𝑀_{ℋ}^{*} A \land p \subseteq A \lor_{ℋ} B)) \to p \subseteq A$
14	13	adantr	$⊢ (((p \in HAtoms \land B \cap C \subseteq A) \land (B 𝑀_{ℋ}^{*} A \land p \subseteq A \lor_{ℋ} B)) \land r \in HAtoms) \to p \subseteq A$
15	11 14	jca	$⊢ (((p \in HAtoms \land B \cap C \subseteq A) \land (B 𝑀_{ℋ}^{*} A \land p \subseteq A \lor_{ℋ} B)) \land r \in HAtoms) \to (p \subseteq p \lor_{ℋ} r \land p \subseteq A)$
16	15	anim1i	$⊢ ((((p \in HAtoms \land B \cap C \subseteq A) \land (B 𝑀_{ℋ}^{*} A \land p \subseteq A \lor_{ℋ} B)) \land r \in HAtoms) \land r \subseteq B) \to ((p \subseteq p \lor_{ℋ} r \land p \subseteq A) \land r \subseteq B)$
17		anass	$⊢ ((p \subseteq p \lor_{ℋ} r \land p \subseteq A) \land r \subseteq B) \leftrightarrow (p \subseteq p \lor_{ℋ} r \land (p \subseteq A \land r \subseteq B))$
18	16 17	sylib	$⊢ ((((p \in HAtoms \land B \cap C \subseteq A) \land (B 𝑀_{ℋ}^{*} A \land p \subseteq A \lor_{ℋ} B)) \land r \in HAtoms) \land r \subseteq B) \to (p \subseteq p \lor_{ℋ} r \land (p \subseteq A \land r \subseteq B))$
19	18	anasss	$⊢ (((p \in HAtoms \land B \cap C \subseteq A) \land (B 𝑀_{ℋ}^{*} A \land p \subseteq A \lor_{ℋ} B)) \land (r \in HAtoms \land r \subseteq B)) \to (p \subseteq p \lor_{ℋ} r \land (p \subseteq A \land r \subseteq B))$
20		oveq1	$⊢ q = p \to q \lor_{ℋ} r = p \lor_{ℋ} r$
21	20	sseq2d	$⊢ q = p \to (p \subseteq q \lor_{ℋ} r \leftrightarrow p \subseteq p \lor_{ℋ} r)$
22		sseq1	$⊢ q = p \to (q \subseteq A \leftrightarrow p \subseteq A)$
23	22	anbi1d	$⊢ q = p \to ((q \subseteq A \land r \subseteq B) \leftrightarrow (p \subseteq A \land r \subseteq B))$
24	21 23	anbi12d	$⊢ q = p \to ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \leftrightarrow (p \subseteq p \lor_{ℋ} r \land (p \subseteq A \land r \subseteq B)))$
25	24	rspcev	$⊢ (p \in HAtoms \land (p \subseteq p \lor_{ℋ} r \land (p \subseteq A \land r \subseteq B))) \to \exists q \in HAtoms (p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B))$
26	5 19 25	syl2anc	$⊢ (((p \in HAtoms \land B \cap C \subseteq A) \land (B 𝑀_{ℋ}^{*} A \land p \subseteq A \lor_{ℋ} B)) \land (r \in HAtoms \land r \subseteq B)) \to \exists q \in HAtoms (p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B))$
27	26	exp32	$⊢ ((p \in HAtoms \land B \cap C \subseteq A) \land (B 𝑀_{ℋ}^{*} A \land p \subseteq A \lor_{ℋ} B)) \to (r \in HAtoms \to (r \subseteq B \to \exists q \in HAtoms (p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B))))$
28	27	reximdvai	$⊢ ((p \in HAtoms \land B \cap C \subseteq A) \land (B 𝑀_{ℋ}^{*} A \land p \subseteq A \lor_{ℋ} B)) \to (\exists r \in HAtoms r \subseteq B \to \exists r \in HAtoms \exists q \in HAtoms (p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)))$
29	4 28	syl5	$⊢ ((p \in HAtoms \land B \cap C \subseteq A) \land (B 𝑀_{ℋ}^{*} A \land p \subseteq A \lor_{ℋ} B)) \to (B \neq 0_{ℋ} \to \exists r \in HAtoms \exists q \in HAtoms (p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)))$

Metamath Proof Explorer

Theorem mdsymlem2

Proof