Theorem ineccnvmo

Description: Equivalence of a double restricted universal quantification and a restricted "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 2-Sep-2021)

	Ref	Expression
Assertion	ineccnvmo	$$⊢\forall y\in B\forall z\in B\left(y=z\vee \left[y\right]F^{-1}\cap \left[z\right]F^{-1}=\varnothing \right)\leftrightarrow \forall x{\exists }^{*}y\in BxFy$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{F}^{-1}$$
2		id	$$⊢y=z\to y=z$$
3	2	inecmo	$$⊢\mathrm{Rel}{F}^{-1}\to \left(\forall y\in B\forall z\in B\left(y=z\vee \left[y\right]F^{-1}\cap \left[z\right]F^{-1}=\varnothing \right)\leftrightarrow \forall x{\exists }^{*}y\in By{F}^{-1}x\right)$$
4	1 3	ax-mp	$$⊢\forall y\in B\forall z\in B\left(y=z\vee \left[y\right]F^{-1}\cap \left[z\right]F^{-1}=\varnothing \right)\leftrightarrow \forall x{\exists }^{*}y\in By{F}^{-1}x$$
5		brcnvg	$$⊢\left(y\in \mathrm{V}\wedge x\in \mathrm{V}\right)\to \left(y{F}^{-1}x\leftrightarrow xFy\right)$$
6	5	el2v	$$⊢y{F}^{-1}x\leftrightarrow xFy$$
7	6	rmobii	$$⊢{\exists }^{*}y\in By{F}^{-1}x\leftrightarrow {\exists }^{*}y\in BxFy$$
8	7	albii	$$⊢\forall x{\exists }^{*}y\in By{F}^{-1}x\leftrightarrow \forall x{\exists }^{*}y\in BxFy$$
9	4 8	bitri	$$⊢\forall y\in B\forall z\in B\left(y=z\vee \left[y\right]F^{-1}\cap \left[z\right]F^{-1}=\varnothing \right)\leftrightarrow \forall x{\exists }^{*}y\in BxFy$$