Theorem infval

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

	Ref	Expression
Hypothesis	infexd.1	|- ( ph -> R Or A )
Assertion	infval	|- ( ph -> inf ( B , A , R ) = ( iota_ x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		infexd.1	|- ( ph -> R Or A )
2		df-inf	|- inf ( B , A , R ) = sup ( B , A , `' R )
3		cnvso	|- ( R Or A <-> `' R Or A )
4	1 3	sylib	|- ( ph -> `' R Or A )
5	4	supval2	|- ( ph -> sup ( B , A , `' R ) = ( iota_ x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) ) )
6		vex	|- x e. _V
7		vex	|- y e. _V
8	6 7	brcnv	|- ( x `' R y <-> y R x )
9	8	a1i	|- ( ph -> ( x `' R y <-> y R x ) )
10	9	notbid	|- ( ph -> ( -. x `' R y <-> -. y R x ) )
11	10	ralbidv	|- ( ph -> ( A. y e. B -. x `' R y <-> A. y e. B -. y R x ) )
12	7 6	brcnv	|- ( y `' R x <-> x R y )
13	12	a1i	|- ( ph -> ( y `' R x <-> x R y ) )
14		vex	|- z e. _V
15	7 14	brcnv	|- ( y `' R z <-> z R y )
16	15	a1i	|- ( ph -> ( y `' R z <-> z R y ) )
17	16	rexbidv	|- ( ph -> ( E. z e. B y `' R z <-> E. z e. B z R y ) )
18	13 17	imbi12d	|- ( ph -> ( ( y `' R x -> E. z e. B y `' R z ) <-> ( x R y -> E. z e. B z R y ) ) )
19	18	ralbidv	|- ( ph -> ( A. y e. A ( y `' R x -> E. z e. B y `' R z ) <-> A. y e. A ( x R y -> E. z e. B z R y ) ) )
20	11 19	anbi12d	|- ( ph -> ( ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) <-> ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) )
21	20	riotabidv	|- ( ph -> ( iota_ x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) ) = ( iota_ x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) )
22	5 21	eqtrd	|- ( ph -> sup ( B , A , `' R ) = ( iota_ x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) )
23	2 22	syl5eq	|- ( ph -> inf ( B , A , R ) = ( iota_ x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) ) )