chsupsn

Description: Value of supremum of subset of CH on a singleton. (Contributed by NM, 13-Aug-2002) (New usage is discouraged.)

		Ref	Expression
	Assertion	chsupsn	$⊢ A \in C_{ℋ} \to ⋁_{ℋ} (\{A\}) = A$

Step	Hyp	Ref	Expression
1		snssi	$⊢ A \in C_{ℋ} \to \{A\} \subseteq C_{ℋ}$
2		chsupval2	$⊢ \{A\} \subseteq C_{ℋ} \to ⋁_{ℋ} (\{A\}) = ⋂ \{x \in C_{ℋ} \| ⋃ \{A\} \subseteq x\}$
3	1 2	syl	$⊢ A \in C_{ℋ} \to ⋁_{ℋ} (\{A\}) = ⋂ \{x \in C_{ℋ} \| ⋃ \{A\} \subseteq x\}$
4		unisng	$⊢ A \in C_{ℋ} \to ⋃ \{A\} = A$
5		eqimss	$⊢ ⋃ \{A\} = A \to ⋃ \{A\} \subseteq A$
6	4 5	syl	$⊢ A \in C_{ℋ} \to ⋃ \{A\} \subseteq A$
7	6	ancli	$⊢ A \in C_{ℋ} \to (A \in C_{ℋ} \land ⋃ \{A\} \subseteq A)$
8		sseq2	$⊢ x = A \to (⋃ \{A\} \subseteq x \leftrightarrow ⋃ \{A\} \subseteq A)$
9	8	elrab	$⊢ A \in \{x \in C_{ℋ} \| ⋃ \{A\} \subseteq x\} \leftrightarrow (A \in C_{ℋ} \land ⋃ \{A\} \subseteq A)$
10	7 9	sylibr	$⊢ A \in C_{ℋ} \to A \in \{x \in C_{ℋ} \| ⋃ \{A\} \subseteq x\}$
11		intss1	$⊢ A \in \{x \in C_{ℋ} \| ⋃ \{A\} \subseteq x\} \to ⋂ \{x \in C_{ℋ} \| ⋃ \{A\} \subseteq x\} \subseteq A$
12	10 11	syl	$⊢ A \in C_{ℋ} \to ⋂ \{x \in C_{ℋ} \| ⋃ \{A\} \subseteq x\} \subseteq A$
13		ssintub	$⊢ ⋃ \{A\} \subseteq ⋂ \{x \in C_{ℋ} \| ⋃ \{A\} \subseteq x\}$
14	4 13	eqsstrrdi	$⊢ A \in C_{ℋ} \to A \subseteq ⋂ \{x \in C_{ℋ} \| ⋃ \{A\} \subseteq x\}$
15	12 14	eqssd	$⊢ A \in C_{ℋ} \to ⋂ \{x \in C_{ℋ} \| ⋃ \{A\} \subseteq x\} = A$
16	3 15	eqtrd	$⊢ A \in C_{ℋ} \to ⋁_{ℋ} (\{A\}) = A$

Metamath Proof Explorer