Theorem fsplitOLD

Description: Obsolete proof of fsplit as of 31-Dec-2023. (Contributed by NM, 17-Sep-2007) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	fsplitOLD	$$⊢{\left({1^{st}\upharpoonright }_{\mathrm{I}}\right)}^{-1}=\left(x\in \mathrm{V}⟼⟨x,x⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2		vex	$$⊢y\in \mathrm{V}$$
3	1 2	brcnv	$$⊢x{\left({1^{st}\upharpoonright }_{\mathrm{I}}\right)}^{-1}y\leftrightarrow y\left({1^{st}\upharpoonright }_{\mathrm{I}}\right)x$$
4	1	brresi	$$⊢y\left({1^{st}\upharpoonright }_{\mathrm{I}}\right)x\leftrightarrow \left(y\in \mathrm{I}\wedge y{1}^{st}x\right)$$
5		19.42v	$$⊢\exists z\left(1^{st}\left(y\right)=x\wedge y=⟨z,z⟩\right)\leftrightarrow \left(1^{st}\left(y\right)=x\wedge \exists zy=⟨z,z⟩\right)$$
6		vex	$$⊢z\in \mathrm{V}$$
7	6 6	op1std	$$⊢y=⟨z,z⟩\to 1^{st}\left(y\right)=z$$
8	7	eqeq1d	$$⊢y=⟨z,z⟩\to \left(1^{st}\left(y\right)=x\leftrightarrow z=x\right)$$
9	8	pm5.32ri	$$⊢\left(1^{st}\left(y\right)=x\wedge y=⟨z,z⟩\right)\leftrightarrow \left(z=x\wedge y=⟨z,z⟩\right)$$
10	9	exbii	$$⊢\exists z\left(1^{st}\left(y\right)=x\wedge y=⟨z,z⟩\right)\leftrightarrow \exists z\left(z=x\wedge y=⟨z,z⟩\right)$$
11		fo1st	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
12		fofn	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to 1^{st}Fn\mathrm{V}$$
13	11 12	ax-mp	$$⊢1^{st}Fn\mathrm{V}$$
14		fnbrfvb	$$⊢\left(1^{st}Fn\mathrm{V}\wedge y\in \mathrm{V}\right)\to \left(1^{st}\left(y\right)=x\leftrightarrow y{1}^{st}x\right)$$
15	13 2 14	mp2an	$$⊢1^{st}\left(y\right)=x\leftrightarrow y{1}^{st}x$$
16		dfid2	$$⊢\mathrm{I}=\left\{⟨z,z⟩|z=z\right\}$$
17	16	eleq2i	$$⊢y\in \mathrm{I}\leftrightarrow y\in \left\{⟨z,z⟩|z=z\right\}$$
18		nfe1	$$⊢Ⅎz\exists z\left(y=⟨z,z⟩\wedge z=z\right)$$
19	18	19.9	$$⊢\exists z\exists z\left(y=⟨z,z⟩\wedge z=z\right)\leftrightarrow \exists z\left(y=⟨z,z⟩\wedge z=z\right)$$
20		elopab	$$⊢y\in \left\{⟨z,z⟩|z=z\right\}\leftrightarrow \exists z\exists z\left(y=⟨z,z⟩\wedge z=z\right)$$
21		equid	$$⊢z=z$$
22	21	biantru	$$⊢y=⟨z,z⟩\leftrightarrow \left(y=⟨z,z⟩\wedge z=z\right)$$
23	22	exbii	$$⊢\exists zy=⟨z,z⟩\leftrightarrow \exists z\left(y=⟨z,z⟩\wedge z=z\right)$$
24	19 20 23	3bitr4i	$$⊢y\in \left\{⟨z,z⟩|z=z\right\}\leftrightarrow \exists zy=⟨z,z⟩$$
25	17 24	bitr2i	$$⊢\exists zy=⟨z,z⟩\leftrightarrow y\in \mathrm{I}$$
26	15 25	anbi12ci	$$⊢\left(1^{st}\left(y\right)=x\wedge \exists zy=⟨z,z⟩\right)\leftrightarrow \left(y\in \mathrm{I}\wedge y{1}^{st}x\right)$$
27	5 10 26	3bitr3ri	$$⊢\left(y\in \mathrm{I}\wedge y{1}^{st}x\right)\leftrightarrow \exists z\left(z=x\wedge y=⟨z,z⟩\right)$$
28		id	$$⊢z=x\to z=x$$
29	28 28	opeq12d	$$⊢z=x\to ⟨z,z⟩=⟨x,x⟩$$
30	29	eqeq2d	$$⊢z=x\to \left(y=⟨z,z⟩\leftrightarrow y=⟨x,x⟩\right)$$
31	30	equsexvw	$$⊢\exists z\left(z=x\wedge y=⟨z,z⟩\right)\leftrightarrow y=⟨x,x⟩$$
32	27 31	bitri	$$⊢\left(y\in \mathrm{I}\wedge y{1}^{st}x\right)\leftrightarrow y=⟨x,x⟩$$
33	4 32	bitri	$$⊢y\left({1^{st}\upharpoonright }_{\mathrm{I}}\right)x\leftrightarrow y=⟨x,x⟩$$
34	3 33	bitri	$$⊢x{\left({1^{st}\upharpoonright }_{\mathrm{I}}\right)}^{-1}y\leftrightarrow y=⟨x,x⟩$$
35	34	opabbii	$$⊢\left\{⟨x,y⟩|x{\left({1^{st}\upharpoonright }_{\mathrm{I}}\right)}^{-1}y\right\}=\left\{⟨x,y⟩|y=⟨x,x⟩\right\}$$
36		relcnv	$$⊢\mathrm{Rel}{\left({1^{st}\upharpoonright }_{\mathrm{I}}\right)}^{-1}$$
37		dfrel4v	$$⊢\mathrm{Rel}{\left({1^{st}\upharpoonright }_{\mathrm{I}}\right)}^{-1}\leftrightarrow {\left({1^{st}\upharpoonright }_{\mathrm{I}}\right)}^{-1}=\left\{⟨x,y⟩|x{\left({1^{st}\upharpoonright }_{\mathrm{I}}\right)}^{-1}y\right\}$$
38	36 37	mpbi	$$⊢{\left({1^{st}\upharpoonright }_{\mathrm{I}}\right)}^{-1}=\left\{⟨x,y⟩|x{\left({1^{st}\upharpoonright }_{\mathrm{I}}\right)}^{-1}y\right\}$$
39		mptv	$$⊢\left(x\in \mathrm{V}⟼⟨x,x⟩\right)=\left\{⟨x,y⟩|y=⟨x,x⟩\right\}$$
40	35 38 39	3eqtr4i	$$⊢{\left({1^{st}\upharpoonright }_{\mathrm{I}}\right)}^{-1}=\left(x\in \mathrm{V}⟼⟨x,x⟩\right)$$