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

Metamath Proof Explorer

Theorem eqfnun

Description: Two functions on A u. B are equal if and only if they have equal restrictions to both A and B . (Contributed by Jeff Madsen, 19-Jun-2011)

Ref Expression
Assertion eqfnun ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ 𝐺 Fn ( 𝐴 ∪ 𝐵 ) ) → ( 𝐹 = 𝐺 ↔ ( ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) ∧ ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 reseq1 ⊢ ( 𝐹 = 𝐺 → ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) )
2 reseq1 ⊢ ( 𝐹 = 𝐺 → ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) )
3 1 2 jca ⊢ ( 𝐹 = 𝐺 → ( ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) ∧ ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ) )
4 elun ⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
5 fveq1 ⊢ ( ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( ( 𝐺 ↾ 𝐴 ) ‘ 𝑥 ) )
6 fvres ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
7 5 6 sylan9req ⊢ ( ( ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
8 fvres ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐺 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
9 8 adantl ⊢ ( ( ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
10 7 9 eqtr3d ⊢ ( ( ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
11 10 adantlr ⊢ ( ( ( ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) ∧ ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
12 fveq1 ⊢ ( ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) = ( ( 𝐺 ↾ 𝐵 ) ‘ 𝑥 ) )
13 fvres ⊢ ( 𝑥 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
14 12 13 sylan9req ⊢ ( ( ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐺 ↾ 𝐵 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
15 fvres ⊢ ( 𝑥 ∈ 𝐵 → ( ( 𝐺 ↾ 𝐵 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
16 15 adantl ⊢ ( ( ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝐺 ↾ 𝐵 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
17 14 16 eqtr3d ⊢ ( ( ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
18 17 adantll ⊢ ( ( ( ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) ∧ ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
19 11 18 jaodan ⊢ ( ( ( ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) ∧ ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
20 4 19 sylan2b ⊢ ( ( ( ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) ∧ ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ) ∧ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
21 20 ralrimiva ⊢ ( ( ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) ∧ ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ) → ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
22 eqfnfv ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ 𝐺 Fn ( 𝐴 ∪ 𝐵 ) ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
23 21 22 imbitrrid ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ 𝐺 Fn ( 𝐴 ∪ 𝐵 ) ) → ( ( ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) ∧ ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ) → 𝐹 = 𝐺 ) )
24 3 23 impbid2 ⊢ ( ( 𝐹 Fn ( 𝐴 ∪ 𝐵 ) ∧ 𝐺 Fn ( 𝐴 ∪ 𝐵 ) ) → ( 𝐹 = 𝐺 ↔ ( ( 𝐹 ↾ 𝐴 ) = ( 𝐺 ↾ 𝐴 ) ∧ ( 𝐹 ↾ 𝐵 ) = ( 𝐺 ↾ 𝐵 ) ) ) )