Metamath Proof Explorer

Theorem fndmdif

Description: Two ways to express the locus of differences between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion fndmdif ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → dom ( 𝐹 ∖ 𝐺 ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 difss ⊢ ( 𝐹 ∖ 𝐺 ) ⊆ 𝐹
2 dmss ⊢ ( ( 𝐹 ∖ 𝐺 ) ⊆ 𝐹 → dom ( 𝐹 ∖ 𝐺 ) ⊆ dom 𝐹 )
3 1 2 ax-mp ⊢ dom ( 𝐹 ∖ 𝐺 ) ⊆ dom 𝐹
4 fndm ⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
5 4 adantr ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → dom 𝐹 = 𝐴 )
6 3 5 sseqtrid ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → dom ( 𝐹 ∖ 𝐺 ) ⊆ 𝐴 )
7 sseqin2 ⊢ ( dom ( 𝐹 ∖ 𝐺 ) ⊆ 𝐴 ↔ ( 𝐴 ∩ dom ( 𝐹 ∖ 𝐺 ) ) = dom ( 𝐹 ∖ 𝐺 ) )
8 6 7 sylib ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐴 ∩ dom ( 𝐹 ∖ 𝐺 ) ) = dom ( 𝐹 ∖ 𝐺 ) )
9 vex ⊢ 𝑥 ∈ V
10 9 eldm ⊢ ( 𝑥 ∈ dom ( 𝐹 ∖ 𝐺 ) ↔ ∃ 𝑦 𝑥 ( 𝐹 ∖ 𝐺 ) 𝑦 )
11 eqcom ⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
12 fnbrfvb ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ↔ 𝑥 𝐺 ( 𝐹 ‘ 𝑥 ) ) )
13 11 12 syl5bb ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ↔ 𝑥 𝐺 ( 𝐹 ‘ 𝑥 ) ) )
14 13 adantll ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ↔ 𝑥 𝐺 ( 𝐹 ‘ 𝑥 ) ) )
15 14 necon3abid ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) ↔ ¬ 𝑥 𝐺 ( 𝐹 ‘ 𝑥 ) ) )
16 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
17 breq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑥 𝐺 𝑦 ↔ 𝑥 𝐺 ( 𝐹 ‘ 𝑥 ) ) )
18 17 notbid ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ¬ 𝑥 𝐺 𝑦 ↔ ¬ 𝑥 𝐺 ( 𝐹 ‘ 𝑥 ) ) )
19 16 18 ceqsexv ⊢ ( ∃ 𝑦 ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ∧ ¬ 𝑥 𝐺 𝑦 ) ↔ ¬ 𝑥 𝐺 ( 𝐹 ‘ 𝑥 ) )
20 15 19 bitr4di ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) ↔ ∃ 𝑦 ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ∧ ¬ 𝑥 𝐺 𝑦 ) ) )
21 eqcom ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑦 )
22 fnbrfvb ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐹 𝑦 ) )
23 21 22 syl5bb ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑥 𝐹 𝑦 ) )
24 23 adantlr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑥 𝐹 𝑦 ) )
25 24 anbi1d ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ∧ ¬ 𝑥 𝐺 𝑦 ) ↔ ( 𝑥 𝐹 𝑦 ∧ ¬ 𝑥 𝐺 𝑦 ) ) )
26 brdif ⊢ ( 𝑥 ( 𝐹 ∖ 𝐺 ) 𝑦 ↔ ( 𝑥 𝐹 𝑦 ∧ ¬ 𝑥 𝐺 𝑦 ) )
27 25 26 bitr4di ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ∧ ¬ 𝑥 𝐺 𝑦 ) ↔ 𝑥 ( 𝐹 ∖ 𝐺 ) 𝑦 ) )
28 27 exbidv ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ∧ ¬ 𝑥 𝐺 𝑦 ) ↔ ∃ 𝑦 𝑥 ( 𝐹 ∖ 𝐺 ) 𝑦 ) )
29 20 28 bitr2d ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 𝑥 ( 𝐹 ∖ 𝐺 ) 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) ) )
30 10 29 syl5bb ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ dom ( 𝐹 ∖ 𝐺 ) ↔ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) ) )
31 30 rabbi2dva ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐴 ∩ dom ( 𝐹 ∖ 𝐺 ) ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) } )
32 8 31 eqtr3d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → dom ( 𝐹 ∖ 𝐺 ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) } )