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