This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ 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ℋ ∣ 𝑥 ⊆ 𝐴 } ) = 𝐴 )