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

Metamath Proof Explorer

Theorem infssd

Description: Inequality deduction for infimum of a subset. (Contributed by AV, 4-Oct-2020)

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

Proof

Step Hyp Ref Expression
1 infssd.0 ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2 infssd.1 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐵 )
3 infssd.3 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐶 𝑧 𝑅 𝑦 ) ) )
4 infssd.4 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
5 1 4 infcl ⊢ ( 𝜑 → inf ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐴 )
6 2 sseld ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐶 → 𝑧 ∈ 𝐵 ) )
7 1 4 inflb ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐵 → ¬ 𝑧 𝑅 inf ( 𝐵 , 𝐴 , 𝑅 ) ) )
8 6 7 syld ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐶 → ¬ 𝑧 𝑅 inf ( 𝐵 , 𝐴 , 𝑅 ) ) )
9 8 ralrimiv ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐶 ¬ 𝑧 𝑅 inf ( 𝐵 , 𝐴 , 𝑅 ) )
10 1 3 infnlb ⊢ ( 𝜑 → ( ( inf ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐴 ∧ ∀ 𝑧 ∈ 𝐶 ¬ 𝑧 𝑅 inf ( 𝐵 , 𝐴 , 𝑅 ) ) → ¬ inf ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 inf ( 𝐵 , 𝐴 , 𝑅 ) ) )
11 5 9 10 mp2and ⊢ ( 𝜑 → ¬ inf ( 𝐶 , 𝐴 , 𝑅 ) 𝑅 inf ( 𝐵 , 𝐴 , 𝑅 ) )