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