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	⊢ ( 𝐴 ∈ Cℋ → ( ∨ℋ ‘ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ssrab2	⊢ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ⊆ Cℋ
2		chsupval2	⊢ ( { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ⊆ Cℋ → ( ∨ℋ ‘ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ) = ∩ { 𝑦 ∈ Cℋ ∣ ∪ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ⊆ 𝑦 } )
3	1 2	ax-mp	⊢ ( ∨ℋ ‘ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ) = ∩ { 𝑦 ∈ Cℋ ∣ ∪ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ⊆ 𝑦 }
4		unimax	⊢ ( 𝐴 ∈ Cℋ → ∪ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } = 𝐴 )
5	4	sseq1d	⊢ ( 𝐴 ∈ Cℋ → ( ∪ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ⊆ 𝑦 ↔ 𝐴 ⊆ 𝑦 ) )
6	5	rabbidv	⊢ ( 𝐴 ∈ Cℋ → { 𝑦 ∈ Cℋ ∣ ∪ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ⊆ 𝑦 } = { 𝑦 ∈ Cℋ ∣ 𝐴 ⊆ 𝑦 } )
7	6	inteqd	⊢ ( 𝐴 ∈ Cℋ → ∩ { 𝑦 ∈ Cℋ ∣ ∪ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ⊆ 𝑦 } = ∩ { 𝑦 ∈ Cℋ ∣ 𝐴 ⊆ 𝑦 } )
8		intmin	⊢ ( 𝐴 ∈ Cℋ → ∩ { 𝑦 ∈ Cℋ ∣ 𝐴 ⊆ 𝑦 } = 𝐴 )
9	7 8	eqtrd	⊢ ( 𝐴 ∈ Cℋ → ∩ { 𝑦 ∈ Cℋ ∣ ∪ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ⊆ 𝑦 } = 𝐴 )
10	3 9	eqtrid	⊢ ( 𝐴 ∈ Cℋ → ( ∨ℋ ‘ { 𝑥 ∈ Cℋ ∣ 𝑥 ⊆ 𝐴 } ) = 𝐴 )