Metamath Proof Explorer


Theorem eqsup

Description: Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015)

Ref Expression
Hypothesis supmo.1 ( 𝜑𝑅 Or 𝐴 )
Assertion eqsup ( 𝜑 → ( ( 𝐶𝐴 ∧ ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) → sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 supmo.1 ( 𝜑𝑅 Or 𝐴 )
2 1 adantr ( ( 𝜑 ∧ ( 𝐶𝐴 ∧ ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) → 𝑅 Or 𝐴 )
3 2 supval2 ( ( 𝜑 ∧ ( 𝐶𝐴 ∧ ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) → sup ( 𝐵 , 𝐴 , 𝑅 ) = ( 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) )
4 3simpc ( ( 𝐶𝐴 ∧ ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) → ( ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) )
5 4 adantl ( ( 𝜑 ∧ ( 𝐶𝐴 ∧ ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) → ( ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) )
6 simpr1 ( ( 𝜑 ∧ ( 𝐶𝐴 ∧ ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) → 𝐶𝐴 )
7 breq1 ( 𝑥 = 𝐶 → ( 𝑥 𝑅 𝑦𝐶 𝑅 𝑦 ) )
8 7 notbid ( 𝑥 = 𝐶 → ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝐶 𝑅 𝑦 ) )
9 8 ralbidv ( 𝑥 = 𝐶 → ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ↔ ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ) )
10 breq2 ( 𝑥 = 𝐶 → ( 𝑦 𝑅 𝑥𝑦 𝑅 𝐶 ) )
11 10 imbi1d ( 𝑥 = 𝐶 → ( ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ↔ ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) )
12 11 ralbidv ( 𝑥 = 𝐶 → ( ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ↔ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) )
13 9 12 anbi12d ( 𝑥 = 𝐶 → ( ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ↔ ( ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) )
14 13 rspcev ( ( 𝐶𝐴 ∧ ( ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) → ∃ 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) )
15 6 5 14 syl2anc ( ( 𝜑 ∧ ( 𝐶𝐴 ∧ ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) → ∃ 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) )
16 2 15 supeu ( ( 𝜑 ∧ ( 𝐶𝐴 ∧ ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) → ∃! 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) )
17 13 riota2 ( ( 𝐶𝐴 ∧ ∃! 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) → ( ( ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ↔ ( 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) = 𝐶 ) )
18 6 16 17 syl2anc ( ( 𝜑 ∧ ( 𝐶𝐴 ∧ ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) → ( ( ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ↔ ( 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) = 𝐶 ) )
19 5 18 mpbid ( ( 𝜑 ∧ ( 𝐶𝐴 ∧ ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) → ( 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) = 𝐶 )
20 3 19 eqtrd ( ( 𝜑 ∧ ( 𝐶𝐴 ∧ ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) ) → sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 )
21 20 ex ( 𝜑 → ( ( 𝐶𝐴 ∧ ∀ 𝑦𝐵 ¬ 𝐶 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝐶 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) → sup ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 ) )