This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ↦ ⟨ 𝑥 , 𝑥 ⟩ )