Metamath Proof Explorer


Theorem 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 C x C | x A = A

Proof

Step Hyp Ref Expression
1 ssrab2 x C | x A C
2 chsupval2 x C | x A C x C | x A = y C | x C | x A y
3 1 2 ax-mp x C | x A = y C | x C | x A y
4 unimax A C x C | x A = A
5 4 sseq1d A C x C | x A y A y
6 5 rabbidv A C y C | x C | x A y = y C | A y
7 6 inteqd A C y C | x C | x A y = y C | A y
8 intmin A C y C | A y = A
9 7 8 eqtrd A C y C | x C | x A y = A
10 3 9 syl5eq A C x C | x A = A