chsupid

Description: A subspace is the supremum of all smaller subspaces. (Contributed by NM, 13-Aug-2002) (New usage is discouraged.)

		Ref	Expression
	Assertion	chsupid	$⊢ A \in C_{ℋ} \to ⋁_{ℋ} (\{x \in C_{ℋ} \| x \subseteq A\}) = A$

Step	Hyp	Ref	Expression
1		ssrab2	$⊢ \{x \in C_{ℋ} \| x \subseteq A\} \subseteq C_{ℋ}$
2		chsupval2	$⊢ \{x \in C_{ℋ} \| x \subseteq A\} \subseteq C_{ℋ} \to ⋁_{ℋ} (\{x \in C_{ℋ} \| x \subseteq A\}) = ⋂ \{y \in C_{ℋ} \| ⋃ \{x \in C_{ℋ} \| x \subseteq A\} \subseteq y\}$
3	1 2	ax-mp	$⊢ ⋁_{ℋ} (\{x \in C_{ℋ} \| x \subseteq A\}) = ⋂ \{y \in C_{ℋ} \| ⋃ \{x \in C_{ℋ} \| x \subseteq A\} \subseteq y\}$
4		unimax	$⊢ A \in C_{ℋ} \to ⋃ \{x \in C_{ℋ} \| x \subseteq A\} = A$
5	4	sseq1d	$⊢ A \in C_{ℋ} \to (⋃ \{x \in C_{ℋ} \| x \subseteq A\} \subseteq y \leftrightarrow A \subseteq y)$
6	5	rabbidv	$⊢ A \in C_{ℋ} \to \{y \in C_{ℋ} \| ⋃ \{x \in C_{ℋ} \| x \subseteq A\} \subseteq y\} = \{y \in C_{ℋ} \| A \subseteq y\}$
7	6	inteqd	$⊢ A \in C_{ℋ} \to ⋂ \{y \in C_{ℋ} \| ⋃ \{x \in C_{ℋ} \| x \subseteq A\} \subseteq y\} = ⋂ \{y \in C_{ℋ} \| A \subseteq y\}$
8		intmin	$⊢ A \in C_{ℋ} \to ⋂ \{y \in C_{ℋ} \| A \subseteq y\} = A$
9	7 8	eqtrd	$⊢ A \in C_{ℋ} \to ⋂ \{y \in C_{ℋ} \| ⋃ \{x \in C_{ℋ} \| x \subseteq A\} \subseteq y\} = A$
10	3 9	eqtrid	$⊢ A \in C_{ℋ} \to ⋁_{ℋ} (\{x \in C_{ℋ} \| x \subseteq A\}) = A$

Metamath Proof Explorer