chirredlem4

Description: Lemma for chirredi . (Contributed by NM, 15-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	chirred.1	$⊢ A \in C_{ℋ}$
	chirred.2	$⊢ x \in C_{ℋ} \to A 𝐶_{ℋ} x$
Assertion	chirredlem4	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \land (r \in HAtoms \land r \subseteq p \lor_{ℋ} q)) \to (r = p \lor r = q)$

Proof

Step	Hyp	Ref	Expression
1		chirred.1	$⊢ A \in C_{ℋ}$
2		chirred.2	$⊢ x \in C_{ℋ} \to A 𝐶_{ℋ} x$
3		atelch	$⊢ r \in HAtoms \to r \in C_{ℋ}$
4		breq2	$⊢ x = r \to (A 𝐶_{ℋ} x \leftrightarrow A 𝐶_{ℋ} r)$
5	4 2	vtoclga	$⊢ r \in C_{ℋ} \to A 𝐶_{ℋ} r$
6	3 5	syl	$⊢ r \in HAtoms \to A 𝐶_{ℋ} r$
7	1	atordi	$⊢ (r \in HAtoms \land A 𝐶_{ℋ} r) \to (r \subseteq A \lor r \subseteq ⊥ (A))$
8	6 7	mpdan	$⊢ r \in HAtoms \to (r \subseteq A \lor r \subseteq ⊥ (A))$
9	8	ad2antrl	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \land (r \in HAtoms \land r \subseteq p \lor_{ℋ} q)) \to (r \subseteq A \lor r \subseteq ⊥ (A))$
10	1 2	chirredlem3	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \land (r \in HAtoms \land r \subseteq p \lor_{ℋ} q)) \to (r \subseteq A \to r = p)$
11	1	ococi	$⊢ ⊥ (⊥ (A)) = A$
12	11	sseq2i	$⊢ p \subseteq ⊥ (⊥ (A)) \leftrightarrow p \subseteq A$
13	12	biimpri	$⊢ p \subseteq A \to p \subseteq ⊥ (⊥ (A))$
14		atelch	$⊢ q \in HAtoms \to q \in C_{ℋ}$
15		atelch	$⊢ p \in HAtoms \to p \in C_{ℋ}$
16		chjcom	$⊢ (q \in C_{ℋ} \land p \in C_{ℋ}) \to q \lor_{ℋ} p = p \lor_{ℋ} q$
17	14 15 16	syl2an	$⊢ (q \in HAtoms \land p \in HAtoms) \to q \lor_{ℋ} p = p \lor_{ℋ} q$
18	17	sseq2d	$⊢ (q \in HAtoms \land p \in HAtoms) \to (r \subseteq q \lor_{ℋ} p \leftrightarrow r \subseteq p \lor_{ℋ} q)$
19	18	anbi2d	$⊢ (q \in HAtoms \land p \in HAtoms) \to ((r \in HAtoms \land r \subseteq q \lor_{ℋ} p) \leftrightarrow (r \in HAtoms \land r \subseteq p \lor_{ℋ} q))$
20	19	ad2ant2r	$⊢ ((q \in HAtoms \land q \subseteq ⊥ (A)) \land (p \in HAtoms \land p \subseteq ⊥ (⊥ (A)))) \to ((r \in HAtoms \land r \subseteq q \lor_{ℋ} p) \leftrightarrow (r \in HAtoms \land r \subseteq p \lor_{ℋ} q))$
21	1	choccli	$⊢ ⊥ (A) \in C_{ℋ}$
22		cmcm3	$⊢ (A \in C_{ℋ} \land x \in C_{ℋ}) \to (A 𝐶_{ℋ} x \leftrightarrow ⊥ (A) 𝐶_{ℋ} x)$
23	1 22	mpan	$⊢ x \in C_{ℋ} \to (A 𝐶_{ℋ} x \leftrightarrow ⊥ (A) 𝐶_{ℋ} x)$
24	2 23	mpbid	$⊢ x \in C_{ℋ} \to ⊥ (A) 𝐶_{ℋ} x$
25	21 24	chirredlem3	$⊢ (((q \in HAtoms \land q \subseteq ⊥ (A)) \land (p \in HAtoms \land p \subseteq ⊥ (⊥ (A)))) \land (r \in HAtoms \land r \subseteq q \lor_{ℋ} p)) \to (r \subseteq ⊥ (A) \to r = q)$
26	25	ex	$⊢ ((q \in HAtoms \land q \subseteq ⊥ (A)) \land (p \in HAtoms \land p \subseteq ⊥ (⊥ (A)))) \to ((r \in HAtoms \land r \subseteq q \lor_{ℋ} p) \to (r \subseteq ⊥ (A) \to r = q))$
27	20 26	sylbird	$⊢ ((q \in HAtoms \land q \subseteq ⊥ (A)) \land (p \in HAtoms \land p \subseteq ⊥ (⊥ (A)))) \to ((r \in HAtoms \land r \subseteq p \lor_{ℋ} q) \to (r \subseteq ⊥ (A) \to r = q))$
28	13 27	sylanr2	$⊢ ((q \in HAtoms \land q \subseteq ⊥ (A)) \land (p \in HAtoms \land p \subseteq A)) \to ((r \in HAtoms \land r \subseteq p \lor_{ℋ} q) \to (r \subseteq ⊥ (A) \to r = q))$
29	28	imp	$⊢ (((q \in HAtoms \land q \subseteq ⊥ (A)) \land (p \in HAtoms \land p \subseteq A)) \land (r \in HAtoms \land r \subseteq p \lor_{ℋ} q)) \to (r \subseteq ⊥ (A) \to r = q)$
30	29	ancom1s	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \land (r \in HAtoms \land r \subseteq p \lor_{ℋ} q)) \to (r \subseteq ⊥ (A) \to r = q)$
31	10 30	orim12d	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \land (r \in HAtoms \land r \subseteq p \lor_{ℋ} q)) \to ((r \subseteq A \lor r \subseteq ⊥ (A)) \to (r = p \lor r = q))$
32	9 31	mpd	$⊢ (((p \in HAtoms \land p \subseteq A) \land (q \in HAtoms \land q \subseteq ⊥ (A))) \land (r \in HAtoms \land r \subseteq p \lor_{ℋ} q)) \to (r = p \lor r = q)$

Metamath Proof Explorer

Theorem chirredlem4

Proof