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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 snssi ⊢ ( 𝐴 ∈ Cℋ → { 𝐴 } ⊆ Cℋ )
2 chsupval2 ⊢ ( { 𝐴 } ⊆ Cℋ → ( ∨ℋ ‘ { 𝐴 } ) = ∩ { 𝑥 ∈ Cℋ ∣ ∪ { 𝐴 } ⊆ 𝑥 } )
3 1 2 syl ⊢ ( 𝐴 ∈ Cℋ → ( ∨ℋ ‘ { 𝐴 } ) = ∩ { 𝑥 ∈ Cℋ ∣ ∪ { 𝐴 } ⊆ 𝑥 } )
4 unisng ⊢ ( 𝐴 ∈ Cℋ → ∪ { 𝐴 } = 𝐴 )
5 eqimss ⊢ ( ∪ { 𝐴 } = 𝐴 → ∪ { 𝐴 } ⊆ 𝐴 )
6 4 5 syl ⊢ ( 𝐴 ∈ Cℋ → ∪ { 𝐴 } ⊆ 𝐴 )
7 6 ancli ⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ∈ Cℋ ∧ ∪ { 𝐴 } ⊆ 𝐴 ) )
8 sseq2 ⊢ ( 𝑥 = 𝐴 → ( ∪ { 𝐴 } ⊆ 𝑥 ↔ ∪ { 𝐴 } ⊆ 𝐴 ) )
9 8 elrab ⊢ ( 𝐴 ∈ { 𝑥 ∈ Cℋ ∣ ∪ { 𝐴 } ⊆ 𝑥 } ↔ ( 𝐴 ∈ Cℋ ∧ ∪ { 𝐴 } ⊆ 𝐴 ) )
10 7 9 sylibr ⊢ ( 𝐴 ∈ Cℋ → 𝐴 ∈ { 𝑥 ∈ Cℋ ∣ ∪ { 𝐴 } ⊆ 𝑥 } )
11 intss1 ⊢ ( 𝐴 ∈ { 𝑥 ∈ Cℋ ∣ ∪ { 𝐴 } ⊆ 𝑥 } → ∩ { 𝑥 ∈ Cℋ ∣ ∪ { 𝐴 } ⊆ 𝑥 } ⊆ 𝐴 )
12 10 11 syl ⊢ ( 𝐴 ∈ Cℋ → ∩ { 𝑥 ∈ Cℋ ∣ ∪ { 𝐴 } ⊆ 𝑥 } ⊆ 𝐴 )
13 ssintub ⊢ ∪ { 𝐴 } ⊆ ∩ { 𝑥 ∈ Cℋ ∣ ∪ { 𝐴 } ⊆ 𝑥 }
14 4 13 eqsstrrdi ⊢ ( 𝐴 ∈ Cℋ → 𝐴 ⊆ ∩ { 𝑥 ∈ Cℋ ∣ ∪ { 𝐴 } ⊆ 𝑥 } )
15 12 14 eqssd ⊢ ( 𝐴 ∈ Cℋ → ∩ { 𝑥 ∈ Cℋ ∣ ∪ { 𝐴 } ⊆ 𝑥 } = 𝐴 )
16 3 15 eqtrd ⊢ ( 𝐴 ∈ Cℋ → ( ∨ℋ ‘ { 𝐴 } ) = 𝐴 )