Theorem infcllem

Description: Lemma for infcl , inflb , infglb , etc. (Contributed by AV, 3-Sep-2020)

	Ref	Expression
Hypotheses	infcl.1	|- ( ph -> R Or A )
	infcl.2	|- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )
Assertion	infcllem	|- ( ph -> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) )

Proof

Step	Hyp	Ref	Expression
1		infcl.1	|- ( ph -> R Or A )
2		infcl.2	|- ( ph -> E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )
3		vex	|- x e. _V
4		vex	|- y e. _V
5	3 4	brcnv	|- ( x `' R y <-> y R x )
6	5	bicomi	|- ( y R x <-> x `' R y )
7	6	notbii	|- ( -. y R x <-> -. x `' R y )
8	7	ralbii	|- ( A. y e. B -. y R x <-> A. y e. B -. x `' R y )
9	4 3	brcnv	|- ( y `' R x <-> x R y )
10	9	bicomi	|- ( x R y <-> y `' R x )
11		vex	|- z e. _V
12	4 11	brcnv	|- ( y `' R z <-> z R y )
13	12	bicomi	|- ( z R y <-> y `' R z )
14	13	rexbii	|- ( E. z e. B z R y <-> E. z e. B y `' R z )
15	10 14	imbi12i	|- ( ( x R y -> E. z e. B z R y ) <-> ( y `' R x -> E. z e. B y `' R z ) )
16	15	ralbii	|- ( A. y e. A ( x R y -> E. z e. B z R y ) <-> A. y e. A ( y `' R x -> E. z e. B y `' R z ) )
17	8 16	anbi12i	|- ( ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) <-> ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) )
18	17	rexbii	|- ( E. x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) <-> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) )
19	2 18	sylib	|- ( ph -> E. x e. A ( A. y e. B -. x `' R y /\ A. y e. A ( y `' R x -> E. z e. B y `' R z ) ) )