chrelat3

Description: A consequence of relative atomicity. (Contributed by NM, 2-Jul-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	chrelat3	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A \subseteq B \leftrightarrow \forall x \in HAtoms (x \subseteq A \to x \subseteq B))$

Step	Hyp	Ref	Expression
1		chrelat2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\neg A \subseteq B \leftrightarrow \exists x \in HAtoms (x \subseteq A \land \neg x \subseteq B))$
2		dfrex2	$⊢ \exists x \in HAtoms (x \subseteq A \land \neg x \subseteq B) \leftrightarrow \neg \forall x \in HAtoms \neg (x \subseteq A \land \neg x \subseteq B)$
3	1 2	bitrdi	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\neg A \subseteq B \leftrightarrow \neg \forall x \in HAtoms \neg (x \subseteq A \land \neg x \subseteq B))$
4	3	con4bid	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A \subseteq B \leftrightarrow \forall x \in HAtoms \neg (x \subseteq A \land \neg x \subseteq B))$
5		iman	$⊢ (x \subseteq A \to x \subseteq B) \leftrightarrow \neg (x \subseteq A \land \neg x \subseteq B)$
6	5	ralbii	$⊢ \forall x \in HAtoms (x \subseteq A \to x \subseteq B) \leftrightarrow \forall x \in HAtoms \neg (x \subseteq A \land \neg x \subseteq B)$
7	4 6	bitr4di	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A \subseteq B \leftrightarrow \forall x \in HAtoms (x \subseteq A \to x \subseteq B))$

Metamath Proof Explorer