Metamath Proof Explorer

Theorem eqfunresadj

Description: Law for adjoining an element to restrictions of functions. (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Assertion eqfunresadj ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → ( 𝐹 ↾ ( 𝑋 ∪ { 𝑌 } ) ) = ( 𝐺 ↾ ( 𝑋 ∪ { 𝑌 } ) ) )

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ( 𝐹 ↾ ( 𝑋 ∪ { 𝑌 } ) )
2 relres ⊢ Rel ( 𝐺 ↾ ( 𝑋 ∪ { 𝑌 } ) )
3 breq ⊢ ( ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) → ( 𝑥 ( 𝐹 ↾ 𝑋 ) 𝑦 ↔ 𝑥 ( 𝐺 ↾ 𝑋 ) 𝑦 ) )
4 3 3ad2ant2 ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → ( 𝑥 ( 𝐹 ↾ 𝑋 ) 𝑦 ↔ 𝑥 ( 𝐺 ↾ 𝑋 ) 𝑦 ) )
5 velsn ⊢ ( 𝑥 ∈ { 𝑌 } ↔ 𝑥 = 𝑌 )
6 simp33 ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) )
7 6 eqeq1d ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → ( ( 𝐹 ‘ 𝑌 ) = 𝑦 ↔ ( 𝐺 ‘ 𝑌 ) = 𝑦 ) )
8 simp1l ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → Fun 𝐹 )
9 simp31 ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → 𝑌 ∈ dom 𝐹 )
10 funbrfvb ⊢ ( ( Fun 𝐹 ∧ 𝑌 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑌 ) = 𝑦 ↔ 𝑌 𝐹 𝑦 ) )
11 8 9 10 syl2anc ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → ( ( 𝐹 ‘ 𝑌 ) = 𝑦 ↔ 𝑌 𝐹 𝑦 ) )
12 simp1r ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → Fun 𝐺 )
13 simp32 ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → 𝑌 ∈ dom 𝐺 )
14 funbrfvb ⊢ ( ( Fun 𝐺 ∧ 𝑌 ∈ dom 𝐺 ) → ( ( 𝐺 ‘ 𝑌 ) = 𝑦 ↔ 𝑌 𝐺 𝑦 ) )
15 12 13 14 syl2anc ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → ( ( 𝐺 ‘ 𝑌 ) = 𝑦 ↔ 𝑌 𝐺 𝑦 ) )
16 7 11 15 3bitr3d ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → ( 𝑌 𝐹 𝑦 ↔ 𝑌 𝐺 𝑦 ) )
17 breq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 𝐹 𝑦 ↔ 𝑌 𝐹 𝑦 ) )
18 breq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 𝐺 𝑦 ↔ 𝑌 𝐺 𝑦 ) )
19 17 18 bibi12d ⊢ ( 𝑥 = 𝑌 → ( ( 𝑥 𝐹 𝑦 ↔ 𝑥 𝐺 𝑦 ) ↔ ( 𝑌 𝐹 𝑦 ↔ 𝑌 𝐺 𝑦 ) ) )
20 16 19 syl5ibrcom ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → ( 𝑥 = 𝑌 → ( 𝑥 𝐹 𝑦 ↔ 𝑥 𝐺 𝑦 ) ) )
21 5 20 syl5bi ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → ( 𝑥 ∈ { 𝑌 } → ( 𝑥 𝐹 𝑦 ↔ 𝑥 𝐺 𝑦 ) ) )
22 21 pm5.32d ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → ( ( 𝑥 ∈ { 𝑌 } ∧ 𝑥 𝐹 𝑦 ) ↔ ( 𝑥 ∈ { 𝑌 } ∧ 𝑥 𝐺 𝑦 ) ) )
23 vex ⊢ 𝑦 ∈ V
24 23 brresi ⊢ ( 𝑥 ( 𝐹 ↾ { 𝑌 } ) 𝑦 ↔ ( 𝑥 ∈ { 𝑌 } ∧ 𝑥 𝐹 𝑦 ) )
25 23 brresi ⊢ ( 𝑥 ( 𝐺 ↾ { 𝑌 } ) 𝑦 ↔ ( 𝑥 ∈ { 𝑌 } ∧ 𝑥 𝐺 𝑦 ) )
26 22 24 25 3bitr4g ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → ( 𝑥 ( 𝐹 ↾ { 𝑌 } ) 𝑦 ↔ 𝑥 ( 𝐺 ↾ { 𝑌 } ) 𝑦 ) )
27 4 26 orbi12d ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → ( ( 𝑥 ( 𝐹 ↾ 𝑋 ) 𝑦 ∨ 𝑥 ( 𝐹 ↾ { 𝑌 } ) 𝑦 ) ↔ ( 𝑥 ( 𝐺 ↾ 𝑋 ) 𝑦 ∨ 𝑥 ( 𝐺 ↾ { 𝑌 } ) 𝑦 ) ) )
28 resundi ⊢ ( 𝐹 ↾ ( 𝑋 ∪ { 𝑌 } ) ) = ( ( 𝐹 ↾ 𝑋 ) ∪ ( 𝐹 ↾ { 𝑌 } ) )
29 28 breqi ⊢ ( 𝑥 ( 𝐹 ↾ ( 𝑋 ∪ { 𝑌 } ) ) 𝑦 ↔ 𝑥 ( ( 𝐹 ↾ 𝑋 ) ∪ ( 𝐹 ↾ { 𝑌 } ) ) 𝑦 )
30 brun ⊢ ( 𝑥 ( ( 𝐹 ↾ 𝑋 ) ∪ ( 𝐹 ↾ { 𝑌 } ) ) 𝑦 ↔ ( 𝑥 ( 𝐹 ↾ 𝑋 ) 𝑦 ∨ 𝑥 ( 𝐹 ↾ { 𝑌 } ) 𝑦 ) )
31 29 30 bitri ⊢ ( 𝑥 ( 𝐹 ↾ ( 𝑋 ∪ { 𝑌 } ) ) 𝑦 ↔ ( 𝑥 ( 𝐹 ↾ 𝑋 ) 𝑦 ∨ 𝑥 ( 𝐹 ↾ { 𝑌 } ) 𝑦 ) )
32 resundi ⊢ ( 𝐺 ↾ ( 𝑋 ∪ { 𝑌 } ) ) = ( ( 𝐺 ↾ 𝑋 ) ∪ ( 𝐺 ↾ { 𝑌 } ) )
33 32 breqi ⊢ ( 𝑥 ( 𝐺 ↾ ( 𝑋 ∪ { 𝑌 } ) ) 𝑦 ↔ 𝑥 ( ( 𝐺 ↾ 𝑋 ) ∪ ( 𝐺 ↾ { 𝑌 } ) ) 𝑦 )
34 brun ⊢ ( 𝑥 ( ( 𝐺 ↾ 𝑋 ) ∪ ( 𝐺 ↾ { 𝑌 } ) ) 𝑦 ↔ ( 𝑥 ( 𝐺 ↾ 𝑋 ) 𝑦 ∨ 𝑥 ( 𝐺 ↾ { 𝑌 } ) 𝑦 ) )
35 33 34 bitri ⊢ ( 𝑥 ( 𝐺 ↾ ( 𝑋 ∪ { 𝑌 } ) ) 𝑦 ↔ ( 𝑥 ( 𝐺 ↾ 𝑋 ) 𝑦 ∨ 𝑥 ( 𝐺 ↾ { 𝑌 } ) 𝑦 ) )
36 27 31 35 3bitr4g ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → ( 𝑥 ( 𝐹 ↾ ( 𝑋 ∪ { 𝑌 } ) ) 𝑦 ↔ 𝑥 ( 𝐺 ↾ ( 𝑋 ∪ { 𝑌 } ) ) 𝑦 ) )
37 1 2 36 eqbrrdiv ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹 ↾ 𝑋 ) = ( 𝐺 ↾ 𝑋 ) ∧ ( 𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ ( 𝐹 ‘ 𝑌 ) = ( 𝐺 ‘ 𝑌 ) ) ) → ( 𝐹 ↾ ( 𝑋 ∪ { 𝑌 } ) ) = ( 𝐺 ↾ ( 𝑋 ∪ { 𝑌 } ) ) )