Theorem infnlb

Description: A lower bound is not greater than the infimum. (Contributed by AV, 3-Sep-2020)

	Ref	Expression
Hypotheses	infcl.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
	infcl.2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
Assertion	infnlb	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝐶 ) → ¬ inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		infcl.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2		infcl.2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
3	1 2	infglb	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ) → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝐶 ) )
4	3	expdimp	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝐶 ) )
5		dfrex2	⊢ ( ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝐶 ↔ ¬ ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝐶 )
6	4 5	imbitrdi	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 → ¬ ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝐶 ) )
7	6	con2d	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝐶 → ¬ inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ) )
8	7	expimpd	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝐶 ) → ¬ inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ) )