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 ( 𝐹𝐺 ) = { 𝑥𝐴 ∣ ( 𝐹𝑥 ) ≠ ( 𝐺𝑥 ) } )