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

Metamath Proof Explorer

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 ( { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐵 ¬ 𝑥 < 𝑤 } , 𝐴 , < ) )