Theorem fliftcnv

Description: Converse of the relation F . (Contributed by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Hypotheses	flift.1	$$⊢F=\mathrm{ran}\left(x\in X⟼⟨A,B⟩\right)$$
	flift.2	$$⊢\left(\phi \wedge x\in X\right)\to A\in R$$
	flift.3	$$⊢\left(\phi \wedge x\in X\right)\to B\in S$$
Assertion	fliftcnv	$$⊢\phi \to F^{-1}=\mathrm{ran}\left(x\in X⟼⟨B,A⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		flift.1	$$⊢F=\mathrm{ran}\left(x\in X⟼⟨A,B⟩\right)$$
2		flift.2	$$⊢\left(\phi \wedge x\in X\right)\to A\in R$$
3		flift.3	$$⊢\left(\phi \wedge x\in X\right)\to B\in S$$
4		eqid	$$⊢\mathrm{ran}\left(x\in X⟼⟨B,A⟩\right)=\mathrm{ran}\left(x\in X⟼⟨B,A⟩\right)$$
5	4 3 2	fliftrel	$$⊢\phi \to \mathrm{ran}\left(x\in X⟼⟨B,A⟩\right)\subseteq S\times R$$
6		relxp	$$⊢\mathrm{Rel}\left(S\times R\right)$$
7		relss	$$⊢\mathrm{ran}\left(x\in X⟼⟨B,A⟩\right)\subseteq S\times R\to \left(\mathrm{Rel}\left(S\times R\right)\to \mathrm{Rel}\mathrm{ran}\left(x\in X⟼⟨B,A⟩\right)\right)$$
8	5 6 7	mpisyl	$$⊢\phi \to \mathrm{Rel}\mathrm{ran}\left(x\in X⟼⟨B,A⟩\right)$$
9		relcnv	$$⊢\mathrm{Rel}{F}^{-1}$$
10	8 9	jctil	$$⊢\phi \to \left(\mathrm{Rel}{F}^{-1}\wedge \mathrm{Rel}\mathrm{ran}\left(x\in X⟼⟨B,A⟩\right)\right)$$
11	1 2 3	fliftel	$$⊢\phi \to \left(zFy\leftrightarrow \exists x\in X\left(z=A\wedge y=B\right)\right)$$
12		vex	$$⊢y\in \mathrm{V}$$
13		vex	$$⊢z\in \mathrm{V}$$
14	12 13	brcnv	$$⊢y{F}^{-1}z\leftrightarrow zFy$$
15		ancom	$$⊢\left(y=B\wedge z=A\right)\leftrightarrow \left(z=A\wedge y=B\right)$$
16	15	rexbii	$$⊢\exists x\in X\left(y=B\wedge z=A\right)\leftrightarrow \exists x\in X\left(z=A\wedge y=B\right)$$
17	11 14 16	3bitr4g	$$⊢\phi \to \left(y{F}^{-1}z\leftrightarrow \exists x\in X\left(y=B\wedge z=A\right)\right)$$
18	4 3 2	fliftel	$$⊢\phi \to \left(y\mathrm{ran}\left(x\in X⟼⟨B,A⟩\right)z\leftrightarrow \exists x\in X\left(y=B\wedge z=A\right)\right)$$
19	17 18	bitr4d	$$⊢\phi \to \left(y{F}^{-1}z\leftrightarrow y\mathrm{ran}\left(x\in X⟼⟨B,A⟩\right)z\right)$$
20		df-br	$$⊢y{F}^{-1}z\leftrightarrow ⟨y,z⟩\in F^{-1}$$
21		df-br	$$⊢y\mathrm{ran}\left(x\in X⟼⟨B,A⟩\right)z\leftrightarrow ⟨y,z⟩\in \mathrm{ran}\left(x\in X⟼⟨B,A⟩\right)$$
22	19 20 21	3bitr3g	$$⊢\phi \to \left(⟨y,z⟩\in F^{-1}\leftrightarrow ⟨y,z⟩\in \mathrm{ran}\left(x\in X⟼⟨B,A⟩\right)\right)$$
23	22	eqrelrdv2	$$⊢\left(\left(\mathrm{Rel}{F}^{-1}\wedge \mathrm{Rel}\mathrm{ran}\left(x\in X⟼⟨B,A⟩\right)\right)\wedge \phi \right)\to F^{-1}=\mathrm{ran}\left(x\in X⟼⟨B,A⟩\right)$$
24	10 23	mpancom	$$⊢\phi \to F^{-1}=\mathrm{ran}\left(x\in X⟼⟨B,A⟩\right)$$