Theorem supssd

Description: Inequality deduction for supremum of a subset. (Contributed by Thierry Arnoux, 21-Mar-2017)

	Ref	Expression
Hypotheses	supssd.0	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
	supssd.1	⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )
	supssd.2	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
	supssd.3	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
	supssd.4	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) )
Assertion	supssd	⊢ ( 𝜑 → ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		supssd.0	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2		supssd.1	⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )
3		supssd.2	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
4		supssd.3	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
5		supssd.4	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) )
6	1 5	supcl	⊢ ( 𝜑 → sup ( 𝐶 , 𝐴 , 𝑅 ) ∈ 𝐴 )
7	2	sseld	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐵 → 𝑧 ∈ 𝐶 ) )
8	1 5	supub	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐶 → ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 𝑧 ) )
9	7 8	syld	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐵 → ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 𝑧 ) )
10	9	ralrimiv	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 𝑧 )
11	1 4	supnub	⊢ ( 𝜑 → ( ( sup ( 𝐶 , 𝐴 , 𝑅 ) ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐵 ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 𝑧 ) → ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) ) )
12	6 10 11	mp2and	⊢ ( 𝜑 → ¬ sup ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 sup ( 𝐵 , 𝐴 , 𝑅 ) )