fsplit

Description: A function that can be used to feed a common value to both operands of an operation. Use as the second argument of a composition with the function of fpar in order to build compound functions such as ( x e. ( 0 [,) +oo ) |-> ( ( sqrtx ) + ( sinx ) ) ) . (Contributed by NM, 17-Sep-2007) Replace use of dfid2 with df-id . (Revised by BJ, 31-Dec-2023)

		Ref	Expression
	Assertion	fsplit	$⊢ {({1^{st} ↾}_{I})}^{-1} = (x \in V ⟼ ⟨x, x⟩)$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2		vex	$⊢ y \in V$
3	1 2	brcnv	$⊢ x {({1^{st} ↾}_{I})}^{-1} y \leftrightarrow y ({1^{st} ↾}_{I}) x$
4	1	brresi	$⊢ y ({1^{st} ↾}_{I}) x \leftrightarrow (y \in I \land y 1^{st} x)$
5		19.42v	$⊢ \exists z (1^{st} (y) = x \land y = ⟨z, z⟩) \leftrightarrow (1^{st} (y) = x \land \exists z y = ⟨z, z⟩)$
6		vex	$⊢ z \in V$
7	6 6	op1std	$⊢ y = ⟨z, z⟩ \to 1^{st} (y) = z$
8	7	eqeq1d	$⊢ y = ⟨z, z⟩ \to (1^{st} (y) = x \leftrightarrow z = x)$
9	8	pm5.32ri	$⊢ (1^{st} (y) = x \land y = ⟨z, z⟩) \leftrightarrow (z = x \land y = ⟨z, z⟩)$
10	9	exbii	$⊢ \exists z (1^{st} (y) = x \land y = ⟨z, z⟩) \leftrightarrow \exists z (z = x \land y = ⟨z, z⟩)$
11		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
12		fofn	$⊢ 1^{st} : V \underset{onto}{⟶} V \to 1^{st} Fn V$
13	11 12	ax-mp	$⊢ 1^{st} Fn V$
14		fnbrfvb	$⊢ (1^{st} Fn V \land y \in V) \to (1^{st} (y) = x \leftrightarrow y 1^{st} x)$
15	13 2 14	mp2an	$⊢ 1^{st} (y) = x \leftrightarrow y 1^{st} x$
16		df-id	$⊢ I = \{⟨z, t⟩ \| z = t\}$
17	16	eleq2i	$⊢ y \in I \leftrightarrow y \in \{⟨z, t⟩ \| z = t\}$
18		elopab	$⊢ y \in \{⟨z, t⟩ \| z = t\} \leftrightarrow \exists z \exists t (y = ⟨z, t⟩ \land z = t)$
19		ancom	$⊢ (y = ⟨z, t⟩ \land z = t) \leftrightarrow (z = t \land y = ⟨z, t⟩)$
20		equcom	$⊢ z = t \leftrightarrow t = z$
21	20	anbi1i	$⊢ (z = t \land y = ⟨z, t⟩) \leftrightarrow (t = z \land y = ⟨z, t⟩)$
22		opeq2	$⊢ t = z \to ⟨z, t⟩ = ⟨z, z⟩$
23	22	eqeq2d	$⊢ t = z \to (y = ⟨z, t⟩ \leftrightarrow y = ⟨z, z⟩)$
24	23	pm5.32i	$⊢ (t = z \land y = ⟨z, t⟩) \leftrightarrow (t = z \land y = ⟨z, z⟩)$
25	19 21 24	3bitri	$⊢ (y = ⟨z, t⟩ \land z = t) \leftrightarrow (t = z \land y = ⟨z, z⟩)$
26	25	exbii	$⊢ \exists t (y = ⟨z, t⟩ \land z = t) \leftrightarrow \exists t (t = z \land y = ⟨z, z⟩)$
27		biidd	$⊢ t = z \to (y = ⟨z, z⟩ \leftrightarrow y = ⟨z, z⟩)$
28	27	equsexvw	$⊢ \exists t (t = z \land y = ⟨z, z⟩) \leftrightarrow y = ⟨z, z⟩$
29	26 28	bitri	$⊢ \exists t (y = ⟨z, t⟩ \land z = t) \leftrightarrow y = ⟨z, z⟩$
30	29	exbii	$⊢ \exists z \exists t (y = ⟨z, t⟩ \land z = t) \leftrightarrow \exists z y = ⟨z, z⟩$
31	17 18 30	3bitrri	$⊢ \exists z y = ⟨z, z⟩ \leftrightarrow y \in I$
32	15 31	anbi12ci	$⊢ (1^{st} (y) = x \land \exists z y = ⟨z, z⟩) \leftrightarrow (y \in I \land y 1^{st} x)$
33	5 10 32	3bitr3ri	$⊢ (y \in I \land y 1^{st} x) \leftrightarrow \exists z (z = x \land y = ⟨z, z⟩)$
34		id	$⊢ z = x \to z = x$
35	34 34	opeq12d	$⊢ z = x \to ⟨z, z⟩ = ⟨x, x⟩$
36	35	eqeq2d	$⊢ z = x \to (y = ⟨z, z⟩ \leftrightarrow y = ⟨x, x⟩)$
37	36	equsexvw	$⊢ \exists z (z = x \land y = ⟨z, z⟩) \leftrightarrow y = ⟨x, x⟩$
38	33 37	bitri	$⊢ (y \in I \land y 1^{st} x) \leftrightarrow y = ⟨x, x⟩$
39	3 4 38	3bitri	$⊢ x {({1^{st} ↾}_{I})}^{-1} y \leftrightarrow y = ⟨x, x⟩$
40	39	opabbii	$⊢ \{⟨x, y⟩ \| x {({1^{st} ↾}_{I})}^{-1} y\} = \{⟨x, y⟩ \| y = ⟨x, x⟩\}$
41		relcnv	$⊢ Rel {({1^{st} ↾}_{I})}^{-1}$
42		dfrel4v	$⊢ Rel {({1^{st} ↾}_{I})}^{-1} \leftrightarrow {({1^{st} ↾}_{I})}^{-1} = \{⟨x, y⟩ \| x {({1^{st} ↾}_{I})}^{-1} y\}$
43	41 42	mpbi	$⊢ {({1^{st} ↾}_{I})}^{-1} = \{⟨x, y⟩ \| x {({1^{st} ↾}_{I})}^{-1} y\}$
44		mptv	$⊢ (x \in V ⟼ ⟨x, x⟩) = \{⟨x, y⟩ \| y = ⟨x, x⟩\}$
45	40 43 44	3eqtr4i	$⊢ {({1^{st} ↾}_{I})}^{-1} = (x \in V ⟼ ⟨x, x⟩)$

Metamath Proof Explorer

Theorem fsplit

Proof