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

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 ( 𝐵 , 𝐴 , 𝑅 ) = 𝐶 ) )