Theorem nomaxmo

Description: A class of surreals has at most one maximum. (Contributed by Scott Fenton, 5-Dec-2021)

	Ref	Expression
Assertion	nomaxmo	⊢ ( 𝑆 ⊆ No → ∃* 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ¬ 𝑥 <s 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		sltso	⊢ <s Or No
2		soss	⊢ ( 𝑆 ⊆ No → ( <s Or No → <s Or 𝑆 ) )
3	1 2	mpi	⊢ ( 𝑆 ⊆ No → <s Or 𝑆 )
4		cnvso	⊢ ( <s Or 𝑆 ↔ ◡ <s Or 𝑆 )
5	3 4	sylib	⊢ ( 𝑆 ⊆ No → ◡ <s Or 𝑆 )
6		somo	⊢ ( ◡ <s Or 𝑆 → ∃* 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ¬ 𝑦 ◡ <s 𝑥 )
7	5 6	syl	⊢ ( 𝑆 ⊆ No → ∃* 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ¬ 𝑦 ◡ <s 𝑥 )
8		vex	⊢ 𝑦 ∈ V
9		vex	⊢ 𝑥 ∈ V
10	8 9	brcnv	⊢ ( 𝑦 ◡ <s 𝑥 ↔ 𝑥 <s 𝑦 )
11	10	notbii	⊢ ( ¬ 𝑦 ◡ <s 𝑥 ↔ ¬ 𝑥 <s 𝑦 )
12	11	ralbii	⊢ ( ∀ 𝑦 ∈ 𝑆 ¬ 𝑦 ◡ <s 𝑥 ↔ ∀ 𝑦 ∈ 𝑆 ¬ 𝑥 <s 𝑦 )
13	12	rmobii	⊢ ( ∃* 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ¬ 𝑦 ◡ <s 𝑥 ↔ ∃* 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ¬ 𝑥 <s 𝑦 )
14	7 13	sylib	⊢ ( 𝑆 ⊆ No → ∃* 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ¬ 𝑥 <s 𝑦 )