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

Metamath Proof Explorer

Theorem fndmin

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

Ref Expression
Assertion fndmin ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → dom ( 𝐹 ∩ 𝐺 ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 dffn5 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
2 1 biimpi ⊢ ( 𝐹 Fn 𝐴 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
3 df-mpt ⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) }
4 2 3 eqtrdi ⊢ ( 𝐹 Fn 𝐴 → 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) } )
5 dffn5 ⊢ ( 𝐺 Fn 𝐴 ↔ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑥 ) ) )
6 5 biimpi ⊢ ( 𝐺 Fn 𝐴 → 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑥 ) ) )
7 df-mpt ⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑥 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) }
8 6 7 eqtrdi ⊢ ( 𝐺 Fn 𝐴 → 𝐺 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) } )
9 4 8 ineqan12d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 ∩ 𝐺 ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) } ) )
10 inopab ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) ) }
11 9 10 eqtrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 ∩ 𝐺 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) ) } )
12 11 dmeqd ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → dom ( 𝐹 ∩ 𝐺 ) = dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) ) } )
13 19.42v ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) ) )
14 anandi ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) ) )
15 14 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) ) ↔ ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) ) )
16 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
17 eqeq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑦 = ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
18 16 17 ceqsexv ⊢ ( ∃ 𝑦 ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
19 18 anbi2i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
20 13 15 19 3bitr3i ⊢ ( ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
21 20 abbii ⊢ { 𝑥 ∣ ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) }
22 dmopab ⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) ) } = { 𝑥 ∣ ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) ) }
23 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) }
24 21 22 23 3eqtr4i ⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝐺 ‘ 𝑥 ) ) ) } = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) }
25 12 24 eqtrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → dom ( 𝐹 ∩ 𝐺 ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) } )