Theorem supinf

Description: The supremum is the infimum of the upper bounds. (Contributed by SN, 29-Jun-2025)

	Ref	Expression
Hypotheses	supinf.1	⊢ ( 𝜑 → < Or 𝐴 )
	supinf.2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 < 𝑧 ) ) )
Assertion	supinf	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , < ) = inf ( { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐵 ¬ 𝑥 < 𝑤 } , 𝐴 , < ) )

Proof

Step	Hyp	Ref	Expression
1		supinf.1	⊢ ( 𝜑 → < Or 𝐴 )
2		supinf.2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 < 𝑧 ) ) )
3	1 2	supcl	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , < ) ∈ 𝐴 )
4		breq1	⊢ ( 𝑥 = sup ( 𝐵 , 𝐴 , < ) → ( 𝑥 < 𝑤 ↔ sup ( 𝐵 , 𝐴 , < ) < 𝑤 ) )
5	4	notbid	⊢ ( 𝑥 = sup ( 𝐵 , 𝐴 , < ) → ( ¬ 𝑥 < 𝑤 ↔ ¬ sup ( 𝐵 , 𝐴 , < ) < 𝑤 ) )
6	5	ralbidv	⊢ ( 𝑥 = sup ( 𝐵 , 𝐴 , < ) → ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑥 < 𝑤 ↔ ∀ 𝑤 ∈ 𝐵 ¬ sup ( 𝐵 , 𝐴 , < ) < 𝑤 ) )
7	1 2	supub	⊢ ( 𝜑 → ( 𝑣 ∈ 𝐵 → ¬ sup ( 𝐵 , 𝐴 , < ) < 𝑣 ) )
8	7	ralrimiv	⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝐵 ¬ sup ( 𝐵 , 𝐴 , < ) < 𝑣 )
9		breq2	⊢ ( 𝑣 = 𝑤 → ( sup ( 𝐵 , 𝐴 , < ) < 𝑣 ↔ sup ( 𝐵 , 𝐴 , < ) < 𝑤 ) )
10	9	notbid	⊢ ( 𝑣 = 𝑤 → ( ¬ sup ( 𝐵 , 𝐴 , < ) < 𝑣 ↔ ¬ sup ( 𝐵 , 𝐴 , < ) < 𝑤 ) )
11	10	cbvralvw	⊢ ( ∀ 𝑣 ∈ 𝐵 ¬ sup ( 𝐵 , 𝐴 , < ) < 𝑣 ↔ ∀ 𝑤 ∈ 𝐵 ¬ sup ( 𝐵 , 𝐴 , < ) < 𝑤 )
12	8 11	sylib	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐵 ¬ sup ( 𝐵 , 𝐴 , < ) < 𝑤 )
13	6 3 12	elrabd	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , < ) ∈ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐵 ¬ 𝑥 < 𝑤 } )
14		breq1	⊢ ( 𝑥 = 𝑣 → ( 𝑥 < 𝑤 ↔ 𝑣 < 𝑤 ) )
15	14	notbid	⊢ ( 𝑥 = 𝑣 → ( ¬ 𝑥 < 𝑤 ↔ ¬ 𝑣 < 𝑤 ) )
16	15	ralbidv	⊢ ( 𝑥 = 𝑣 → ( ∀ 𝑤 ∈ 𝐵 ¬ 𝑥 < 𝑤 ↔ ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 < 𝑤 ) )
17	16	elrab	⊢ ( 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐵 ¬ 𝑥 < 𝑤 } ↔ ( 𝑣 ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 < 𝑤 ) )
18		breq2	⊢ ( 𝑧 = 𝑤 → ( 𝑦 < 𝑧 ↔ 𝑦 < 𝑤 ) )
19	18	cbvrexvw	⊢ ( ∃ 𝑧 ∈ 𝐵 𝑦 < 𝑧 ↔ ∃ 𝑤 ∈ 𝐵 𝑦 < 𝑤 )
20	19	imbi2i	⊢ ( ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 < 𝑧 ) ↔ ( 𝑦 < 𝑥 → ∃ 𝑤 ∈ 𝐵 𝑦 < 𝑤 ) )
21	20	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 < 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 → ∃ 𝑤 ∈ 𝐵 𝑦 < 𝑤 ) )
22	21	anbi2i	⊢ ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 → ∃ 𝑤 ∈ 𝐵 𝑦 < 𝑤 ) ) )
23	22	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 < 𝑧 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 → ∃ 𝑤 ∈ 𝐵 𝑦 < 𝑤 ) ) )
24	2 23	sylib	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 < 𝑥 → ∃ 𝑤 ∈ 𝐵 𝑦 < 𝑤 ) ) )
25	1 24	supnub	⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐵 ¬ 𝑣 < 𝑤 ) → ¬ 𝑣 < sup ( 𝐵 , 𝐴 , < ) ) )
26	17 25	biimtrid	⊢ ( 𝜑 → ( 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐵 ¬ 𝑥 < 𝑤 } → ¬ 𝑣 < sup ( 𝐵 , 𝐴 , < ) ) )
27	26	imp	⊢ ( ( 𝜑 ∧ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐵 ¬ 𝑥 < 𝑤 } ) → ¬ 𝑣 < sup ( 𝐵 , 𝐴 , < ) )
28	1 3 13 27	infmin	⊢ ( 𝜑 → inf ( { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐵 ¬ 𝑥 < 𝑤 } , 𝐴 , < ) = sup ( 𝐵 , 𝐴 , < ) )
29	28	eqcomd	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , < ) = inf ( { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐵 ¬ 𝑥 < 𝑤 } , 𝐴 , < ) )