Theorem infglbb

Description: Bidirectional form of infglb . (Contributed by AV, 3-Sep-2020)

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

Proof

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