Theorem infglb

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

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

Proof

Step	Hyp	Ref	Expression
1		infcl.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2		infcl.2	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
3		df-inf	⊢ inf ( 𝐵 , 𝐴 , 𝑅 ) = sup ( 𝐵 , 𝐴 , ◡ 𝑅 )
4	3	breq1i	⊢ ( inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ↔ sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) 𝑅 𝐶 )
5		simpr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → 𝐶 ∈ 𝐴 )
6		cnvso	⊢ ( 𝑅 Or 𝐴 ↔ ◡ 𝑅 Or 𝐴 )
7	1 6	sylib	⊢ ( 𝜑 → ◡ 𝑅 Or 𝐴 )
8	1 2	infcllem	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) )
9	7 8	supcl	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ∈ 𝐴 )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ∈ 𝐴 )
11		brcnvg	⊢ ( ( 𝐶 ∈ 𝐴 ∧ sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ∈ 𝐴 ) → ( 𝐶 ◡ 𝑅 sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ↔ sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) 𝑅 𝐶 ) )
12	11	bicomd	⊢ ( ( 𝐶 ∈ 𝐴 ∧ sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ∈ 𝐴 ) → ( sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) 𝑅 𝐶 ↔ 𝐶 ◡ 𝑅 sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ) )
13	5 10 12	syl2anc	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) 𝑅 𝐶 ↔ 𝐶 ◡ 𝑅 sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ) )
14	4 13	bitrid	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ↔ 𝐶 ◡ 𝑅 sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ) )
15	7 8	suplub	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ 𝐶 ◡ 𝑅 sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) ) → ∃ 𝑧 ∈ 𝐵 𝐶 ◡ 𝑅 𝑧 ) )
16	15	expdimp	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐶 ◡ 𝑅 sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝐶 ◡ 𝑅 𝑧 ) )
17		vex	⊢ 𝑧 ∈ V
18		brcnvg	⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝑧 ∈ V ) → ( 𝐶 ◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝐶 ) )
19	5 17 18	sylancl	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐶 ◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝐶 ) )
20	19	rexbidv	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ 𝐵 𝐶 ◡ 𝑅 𝑧 ↔ ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝐶 ) )
21	16 20	sylibd	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐶 ◡ 𝑅 sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝐶 ) )
22	14 21	sylbid	⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝐶 ) )
23	22	expimpd	⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐴 ∧ inf ( 𝐵 , 𝐴 , 𝑅 ) 𝑅 𝐶 ) → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝐶 ) )