Theorem infcl

Description: An infimum belongs to its base class (closure law). See also inflb and infglb . (Contributed by AV, 3-Sep-2020)

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

Proof

Step	Hyp	Ref	Expression
1		infcl.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2		infcl.2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
3		df-inf	⊢ inf ( 𝐵 , 𝐴 , 𝑅 ) = sup ( 𝐵 , 𝐴 , ◡ 𝑅 )
4		cnvso	⊢ ( 𝑅 Or 𝐴 ↔ ◡ 𝑅 Or 𝐴 )
5	1 4	sylib	⊢ ( 𝜑 → ◡ 𝑅 Or 𝐴 )
6	1 2	infcllem	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) )
7	5 6	supcl	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ∈ 𝐴 )
8	3 7	eqeltrid	⊢ ( 𝜑 → inf ( 𝐵 , 𝐴 , 𝑅 ) ∈ 𝐴 )