Theorem infval

Description: Alternate expression for the infimum. (Contributed by AV, 2-Sep-2020)

	Ref	Expression
Hypothesis	infexd.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
Assertion	infval	⊢ ( 𝜑 → inf ( 𝐵 , 𝐴 , 𝑅 ) = ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		infexd.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2		df-inf	⊢ inf ( 𝐵 , 𝐴 , 𝑅 ) = sup ( 𝐵 , 𝐴 , ◡ 𝑅 )
3		cnvso	⊢ ( 𝑅 Or 𝐴 ↔ ◡ 𝑅 Or 𝐴 )
4	1 3	sylib	⊢ ( 𝜑 → ◡ 𝑅 Or 𝐴 )
5	4	supval2	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) = ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ) )
6		vex	⊢ 𝑥 ∈ V
7		vex	⊢ 𝑦 ∈ V
8	6 7	brcnv	⊢ ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 )
9	8	a1i	⊢ ( 𝜑 → ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) )
10	9	notbid	⊢ ( 𝜑 → ( ¬ 𝑥 ◡ 𝑅 𝑦 ↔ ¬ 𝑦 𝑅 𝑥 ) )
11	10	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ◡ 𝑅 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
12	7 6	brcnv	⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 )
13	12	a1i	⊢ ( 𝜑 → ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 ) )
14		vex	⊢ 𝑧 ∈ V
15	7 14	brcnv	⊢ ( 𝑦 ◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝑦 )
16	15	a1i	⊢ ( 𝜑 → ( 𝑦 ◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝑦 ) )
17	16	rexbidv	⊢ ( 𝜑 → ( ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ↔ ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) )
18	13 17	imbi12d	⊢ ( 𝜑 → ( ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ↔ ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
19	18	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) )
20	11 19	anbi12d	⊢ ( 𝜑 → ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) )
21	20	riotabidv	⊢ ( 𝜑 → ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 ◡ 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 ◡ 𝑅 𝑧 ) ) ) = ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) )
22	5 21	eqtrd	⊢ ( 𝜑 → sup ( 𝐵 , 𝐴 , ◡ 𝑅 ) = ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) )
23	2 22	eqtrid	⊢ ( 𝜑 → inf ( 𝐵 , 𝐴 , 𝑅 ) = ( ℩ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 𝑅 𝑦 ) ) ) )