Theorem infcllem

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

	Ref	Expression
Hypotheses	infcl.1	$$⊢\phi \to R\mathrm{Or}A$$
	infcl.2	$$⊢\phi \to \exists x\in A\left(\forall y\in B\neg yRx\wedge \forall y\in A\left(xRy\to \exists z\in BzRy\right)\right)$$
Assertion	infcllem	$$⊢\phi \to \exists x\in A\left(\forall y\in B\neg x{R}^{-1}y\wedge \forall y\in A\left(y{R}^{-1}x\to \exists z\in By{R}^{-1}z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		infcl.1	$$⊢\phi \to R\mathrm{Or}A$$
2		infcl.2	$$⊢\phi \to \exists x\in A\left(\forall y\in B\neg yRx\wedge \forall y\in A\left(xRy\to \exists z\in BzRy\right)\right)$$
3		vex	$$⊢x\in \mathrm{V}$$
4		vex	$$⊢y\in \mathrm{V}$$
5	3 4	brcnv	$$⊢x{R}^{-1}y\leftrightarrow yRx$$
6	5	bicomi	$$⊢yRx\leftrightarrow x{R}^{-1}y$$
7	6	notbii	$$⊢\neg yRx\leftrightarrow \neg x{R}^{-1}y$$
8	7	ralbii	$$⊢\forall y\in B\neg yRx\leftrightarrow \forall y\in B\neg x{R}^{-1}y$$
9	4 3	brcnv	$$⊢y{R}^{-1}x\leftrightarrow xRy$$
10	9	bicomi	$$⊢xRy\leftrightarrow y{R}^{-1}x$$
11		vex	$$⊢z\in \mathrm{V}$$
12	4 11	brcnv	$$⊢y{R}^{-1}z\leftrightarrow zRy$$
13	12	bicomi	$$⊢zRy\leftrightarrow y{R}^{-1}z$$
14	13	rexbii	$$⊢\exists z\in BzRy\leftrightarrow \exists z\in By{R}^{-1}z$$
15	10 14	imbi12i	$$⊢\left(xRy\to \exists z\in BzRy\right)\leftrightarrow \left(y{R}^{-1}x\to \exists z\in By{R}^{-1}z\right)$$
16	15	ralbii	$$⊢\forall y\in A\left(xRy\to \exists z\in BzRy\right)\leftrightarrow \forall y\in A\left(y{R}^{-1}x\to \exists z\in By{R}^{-1}z\right)$$
17	8 16	anbi12i	$$⊢\left(\forall y\in B\neg yRx\wedge \forall y\in A\left(xRy\to \exists z\in BzRy\right)\right)\leftrightarrow \left(\forall y\in B\neg x{R}^{-1}y\wedge \forall y\in A\left(y{R}^{-1}x\to \exists z\in By{R}^{-1}z\right)\right)$$
18	17	rexbii	$$⊢\exists x\in A\left(\forall y\in B\neg yRx\wedge \forall y\in A\left(xRy\to \exists z\in BzRy\right)\right)\leftrightarrow \exists x\in A\left(\forall y\in B\neg x{R}^{-1}y\wedge \forall y\in A\left(y{R}^{-1}x\to \exists z\in By{R}^{-1}z\right)\right)$$
19	2 18	sylib	$$⊢\phi \to \exists x\in A\left(\forall y\in B\neg x{R}^{-1}y\wedge \forall y\in A\left(y{R}^{-1}x\to \exists z\in By{R}^{-1}z\right)\right)$$