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

Metamath Proof Explorer

Theorem suplub

Description: A supremum is the least upper bound. See also supcl and supub . (Contributed by NM, 13-Oct-2004) (Revised by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypotheses supmo.1 ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
supcl.2 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
Assertion suplub ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) → ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) )

Proof

Step Hyp Ref Expression
1 supmo.1 ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2 supcl.2 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
3 simpr ⊢ ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) )
4 breq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 𝑅 𝑥 ↔ 𝑤 𝑅 𝑥 ) )
5 breq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 𝑅 𝑧 ↔ 𝑤 𝑅 𝑧 ) )
6 5 rexbidv ⊢ ( 𝑦 = 𝑤 → ( ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ↔ ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) )
7 4 6 imbi12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ↔ ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ) )
8 7 cbvralvw ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) )
9 3 8 sylib ⊢ ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) )
10 9 a1i ⊢ ( 𝑥 ∈ 𝐴 → ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ) )
11 10 ss2rabi ⊢ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } ⊆ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) }
12 1 supval2 ⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) = ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) )
13 1 2 supeu ⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
14 riotacl2 ⊢ ( ∃! 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) → ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) ∈ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } )
15 13 14 syl ⊢ ( 𝜑 → ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ) ∈ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } )
16 12 15 eqeltrd ⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } )
17 11 16 sselid ⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) } )
18 breq2 ⊢ ( 𝑥 = sup ( 𝐵 , 𝐴 , 𝑅 ) → ( 𝑤 𝑅 𝑥 ↔ 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
19 18 imbi1d ⊢ ( 𝑥 = sup ( 𝐵 , 𝐴 , 𝑅 ) → ( ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ↔ ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ) )
20 19 ralbidv ⊢ ( 𝑥 = sup ( 𝐵 , 𝐴 , 𝑅 ) → ( ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ) )
21 20 elrab ⊢ ( sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) } ↔ ( sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐴 ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ) )
22 21 simprbi ⊢ ( sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) } → ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) )
23 17 22 syl ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) )
24 breq1 ⊢ ( 𝑤 = 𝐶 → ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ↔ 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
25 breq1 ⊢ ( 𝑤 = 𝐶 → ( 𝑤 𝑅 𝑧 ↔ 𝐶 𝑅 𝑧 ) )
26 25 rexbidv ⊢ ( 𝑤 = 𝐶 → ( ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ↔ ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) )
27 24 26 imbi12d ⊢ ( 𝑤 = 𝐶 → ( ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) ↔ ( 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) ) )
28 27 rspccv ⊢ ( ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) → ( 𝐶 ∈ 𝐴 → ( 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) ) )
29 28 impd ⊢ ( ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑤 𝑅 𝑧 ) → ( ( 𝐶 ∈ 𝐴 ∧ 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) → ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) )
30 23 29 syl ⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ 𝐶 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) → ∃ 𝑧 ∈ 𝐵 𝐶 𝑅 𝑧 ) )