Theorem 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	⊢ ◡ ( 1st ↾ I ) = ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		vex	⊢ 𝑦 ∈ V
3	1 2	brcnv	⊢ ( 𝑥 ◡ ( 1st ↾ I ) 𝑦 ↔ 𝑦 ( 1st ↾ I ) 𝑥 )
4	1	brresi	⊢ ( 𝑦 ( 1st ↾ I ) 𝑥 ↔ ( 𝑦 ∈ I ∧ 𝑦 1st 𝑥 ) )
5		19.42v	⊢ ( ∃ 𝑧 ( ( 1st ‘ 𝑦 ) = 𝑥 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) ↔ ( ( 1st ‘ 𝑦 ) = 𝑥 ∧ ∃ 𝑧 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) )
6		vex	⊢ 𝑧 ∈ V
7	6 6	op1std	⊢ ( 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ → ( 1st ‘ 𝑦 ) = 𝑧 )
8	7	eqeq1d	⊢ ( 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ → ( ( 1st ‘ 𝑦 ) = 𝑥 ↔ 𝑧 = 𝑥 ) )
9	8	pm5.32ri	⊢ ( ( ( 1st ‘ 𝑦 ) = 𝑥 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) ↔ ( 𝑧 = 𝑥 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) )
10	9	exbii	⊢ ( ∃ 𝑧 ( ( 1st ‘ 𝑦 ) = 𝑥 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) )
11		fo1st	⊢ 1st : V –onto→ V
12		fofn	⊢ ( 1st : V –onto→ V → 1st Fn V )
13	11 12	ax-mp	⊢ 1st Fn V
14		fnbrfvb	⊢ ( ( 1st Fn V ∧ 𝑦 ∈ V ) → ( ( 1st ‘ 𝑦 ) = 𝑥 ↔ 𝑦 1st 𝑥 ) )
15	13 2 14	mp2an	⊢ ( ( 1st ‘ 𝑦 ) = 𝑥 ↔ 𝑦 1st 𝑥 )
16		df-id	⊢ I = { ⟨ 𝑧 , 𝑡 ⟩ ∣ 𝑧 = 𝑡 }
17	16	eleq2i	⊢ ( 𝑦 ∈ I ↔ 𝑦 ∈ { ⟨ 𝑧 , 𝑡 ⟩ ∣ 𝑧 = 𝑡 } )
18		elopab	⊢ ( 𝑦 ∈ { ⟨ 𝑧 , 𝑡 ⟩ ∣ 𝑧 = 𝑡 } ↔ ∃ 𝑧 ∃ 𝑡 ( 𝑦 = ⟨ 𝑧 , 𝑡 ⟩ ∧ 𝑧 = 𝑡 ) )
19		ancom	⊢ ( ( 𝑦 = ⟨ 𝑧 , 𝑡 ⟩ ∧ 𝑧 = 𝑡 ) ↔ ( 𝑧 = 𝑡 ∧ 𝑦 = ⟨ 𝑧 , 𝑡 ⟩ ) )
20		equcom	⊢ ( 𝑧 = 𝑡 ↔ 𝑡 = 𝑧 )
21	20	anbi1i	⊢ ( ( 𝑧 = 𝑡 ∧ 𝑦 = ⟨ 𝑧 , 𝑡 ⟩ ) ↔ ( 𝑡 = 𝑧 ∧ 𝑦 = ⟨ 𝑧 , 𝑡 ⟩ ) )
22		opeq2	⊢ ( 𝑡 = 𝑧 → ⟨ 𝑧 , 𝑡 ⟩ = ⟨ 𝑧 , 𝑧 ⟩ )
23	22	eqeq2d	⊢ ( 𝑡 = 𝑧 → ( 𝑦 = ⟨ 𝑧 , 𝑡 ⟩ ↔ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) )
24	23	pm5.32i	⊢ ( ( 𝑡 = 𝑧 ∧ 𝑦 = ⟨ 𝑧 , 𝑡 ⟩ ) ↔ ( 𝑡 = 𝑧 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) )
25	19 21 24	3bitri	⊢ ( ( 𝑦 = ⟨ 𝑧 , 𝑡 ⟩ ∧ 𝑧 = 𝑡 ) ↔ ( 𝑡 = 𝑧 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) )
26	25	exbii	⊢ ( ∃ 𝑡 ( 𝑦 = ⟨ 𝑧 , 𝑡 ⟩ ∧ 𝑧 = 𝑡 ) ↔ ∃ 𝑡 ( 𝑡 = 𝑧 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) )
27		biidd	⊢ ( 𝑡 = 𝑧 → ( 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ↔ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) )
28	27	equsexvw	⊢ ( ∃ 𝑡 ( 𝑡 = 𝑧 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) ↔ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ )
29	26 28	bitri	⊢ ( ∃ 𝑡 ( 𝑦 = ⟨ 𝑧 , 𝑡 ⟩ ∧ 𝑧 = 𝑡 ) ↔ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ )
30	29	exbii	⊢ ( ∃ 𝑧 ∃ 𝑡 ( 𝑦 = ⟨ 𝑧 , 𝑡 ⟩ ∧ 𝑧 = 𝑡 ) ↔ ∃ 𝑧 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ )
31	17 18 30	3bitrri	⊢ ( ∃ 𝑧 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ↔ 𝑦 ∈ I )
32	15 31	anbi12ci	⊢ ( ( ( 1st ‘ 𝑦 ) = 𝑥 ∧ ∃ 𝑧 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) ↔ ( 𝑦 ∈ I ∧ 𝑦 1st 𝑥 ) )
33	5 10 32	3bitr3ri	⊢ ( ( 𝑦 ∈ I ∧ 𝑦 1st 𝑥 ) ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) )
34		id	⊢ ( 𝑧 = 𝑥 → 𝑧 = 𝑥 )
35	34 34	opeq12d	⊢ ( 𝑧 = 𝑥 → ⟨ 𝑧 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑥 ⟩ )
36	35	eqeq2d	⊢ ( 𝑧 = 𝑥 → ( 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ↔ 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ ) )
37	36	equsexvw	⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) ↔ 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ )
38	33 37	bitri	⊢ ( ( 𝑦 ∈ I ∧ 𝑦 1st 𝑥 ) ↔ 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ )
39	3 4 38	3bitri	⊢ ( 𝑥 ◡ ( 1st ↾ I ) 𝑦 ↔ 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ )
40	39	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ◡ ( 1st ↾ I ) 𝑦 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ }
41		relcnv	⊢ Rel ◡ ( 1st ↾ I )
42		dfrel4v	⊢ ( Rel ◡ ( 1st ↾ I ) ↔ ◡ ( 1st ↾ I ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ◡ ( 1st ↾ I ) 𝑦 } )
43	41 42	mpbi	⊢ ◡ ( 1st ↾ I ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ◡ ( 1st ↾ I ) 𝑦 }
44		mptv	⊢ ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ }
45	40 43 44	3eqtr4i	⊢ ◡ ( 1st ↾ I ) = ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ )