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

Metamath Proof Explorer

Theorem inflb

Description: An infimum is a lower bound. See also infcl and infglb . (Contributed by AV, 3-Sep-2020)

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

Proof

Step	Hyp	Ref	Expression
1		infcl.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2		infcl.2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
3		cnvso	⊢ ( 𝑅 Or 𝐴 ↔ ^◡ 𝑅 Or 𝐴 )
4	1 3	sylib	⊢ ( 𝜑 → ^◡ 𝑅 Or 𝐴 )
5	1 2	infcllem	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ^◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ^◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ^◡ 𝑅 𝑧 ) ) )
6	4 5	supub	⊢ ( 𝜑 → ( 𝐶 ∈ 𝐵 → ¬ sup ( 𝐵 , 𝐴 , ^◡ 𝑅 ) ^◡ 𝑅 𝐶 ) )
7	6	imp	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐵 ) → ¬ sup ( 𝐵 , 𝐴 , ^◡ 𝑅 ) ^◡ 𝑅 𝐶 )
8		df-inf	⊢ inf ( 𝐵 , 𝐴 , 𝑅 ) = sup ( 𝐵 , 𝐴 , ^◡ 𝑅 )
9	8	a1i	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐵 ) → inf ( 𝐵 , 𝐴 , 𝑅 ) = sup ( 𝐵 , 𝐴 , ^◡ 𝑅 ) )
10	9	breq2d	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐶 𝑅 inf ( 𝐵 , 𝐴 , 𝑅 ) ↔ 𝐶 𝑅 sup ( 𝐵 , 𝐴 , ^◡ 𝑅 ) ) )
11	4 5	supcl	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , ^◡ 𝑅 ) ∈ 𝐴 )
12		brcnvg	⊢ ( ( sup ( 𝐵 , 𝐴 , ^◡ 𝑅 ) ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( sup ( 𝐵 , 𝐴 , ^◡ 𝑅 ) ^◡ 𝑅 𝐶 ↔ 𝐶 𝑅 sup ( 𝐵 , 𝐴 , ^◡ 𝑅 ) ) )
13	12	bicomd	⊢ ( ( sup ( 𝐵 , 𝐴 , ^◡ 𝑅 ) ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐶 𝑅 sup ( 𝐵 , 𝐴 , ^◡ 𝑅 ) ↔ sup ( 𝐵 , 𝐴 , ^◡ 𝑅 ) ^◡ 𝑅 𝐶 ) )
14	11 13	sylan	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐶 𝑅 sup ( 𝐵 , 𝐴 , ^◡ 𝑅 ) ↔ sup ( 𝐵 , 𝐴 , ^◡ 𝑅 ) ^◡ 𝑅 𝐶 ) )
15	10 14	bitrd	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐶 𝑅 inf ( 𝐵 , 𝐴 , 𝑅 ) ↔ sup ( 𝐵 , 𝐴 , ^◡ 𝑅 ) ^◡ 𝑅 𝐶 ) )
16	7 15	mtbird	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐵 ) → ¬ 𝐶 𝑅 inf ( 𝐵 , 𝐴 , 𝑅 ) )
17	16	ex	⊢ ( 𝜑 → ( 𝐶 ∈ 𝐵 → ¬ 𝐶 𝑅 inf ( 𝐵 , 𝐴 , 𝑅 ) ) )