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 
|- ( ( F Fn A /\ G Fn A ) -> dom ( F i^i G ) = { x e. A | ( F ` x ) = ( G ` x ) } )

Proof

Step Hyp Ref Expression
1 dffn5 
 |-  ( F Fn A <-> F = ( x e. A |-> ( F ` x ) ) )
2 1 biimpi 
 |-  ( F Fn A -> F = ( x e. A |-> ( F ` x ) ) )
3 df-mpt 
 |-  ( x e. A |-> ( F ` x ) ) = { <. x , y >. | ( x e. A /\ y = ( F ` x ) ) }
4 2 3 eqtrdi 
 |-  ( F Fn A -> F = { <. x , y >. | ( x e. A /\ y = ( F ` x ) ) } )
5 dffn5 
 |-  ( G Fn A <-> G = ( x e. A |-> ( G ` x ) ) )
6 5 biimpi 
 |-  ( G Fn A -> G = ( x e. A |-> ( G ` x ) ) )
7 df-mpt 
 |-  ( x e. A |-> ( G ` x ) ) = { <. x , y >. | ( x e. A /\ y = ( G ` x ) ) }
8 6 7 eqtrdi 
 |-  ( G Fn A -> G = { <. x , y >. | ( x e. A /\ y = ( G ` x ) ) } )
9 4 8 ineqan12d 
 |-  ( ( F Fn A /\ G Fn A ) -> ( F i^i G ) = ( { <. x , y >. | ( x e. A /\ y = ( F ` x ) ) } i^i { <. x , y >. | ( x e. A /\ y = ( G ` x ) ) } ) )
10 inopab 
 |-  ( { <. x , y >. | ( x e. A /\ y = ( F ` x ) ) } i^i { <. x , y >. | ( x e. A /\ y = ( G ` x ) ) } ) = { <. x , y >. | ( ( x e. A /\ y = ( F ` x ) ) /\ ( x e. A /\ y = ( G ` x ) ) ) }
11 9 10 eqtrdi 
 |-  ( ( F Fn A /\ G Fn A ) -> ( F i^i G ) = { <. x , y >. | ( ( x e. A /\ y = ( F ` x ) ) /\ ( x e. A /\ y = ( G ` x ) ) ) } )
12 11 dmeqd 
 |-  ( ( F Fn A /\ G Fn A ) -> dom ( F i^i G ) = dom { <. x , y >. | ( ( x e. A /\ y = ( F ` x ) ) /\ ( x e. A /\ y = ( G ` x ) ) ) } )
13 19.42v 
 |-  ( E. y ( x e. A /\ ( y = ( F ` x ) /\ y = ( G ` x ) ) ) <-> ( x e. A /\ E. y ( y = ( F ` x ) /\ y = ( G ` x ) ) ) )
14 anandi 
 |-  ( ( x e. A /\ ( y = ( F ` x ) /\ y = ( G ` x ) ) ) <-> ( ( x e. A /\ y = ( F ` x ) ) /\ ( x e. A /\ y = ( G ` x ) ) ) )
15 14 exbii 
 |-  ( E. y ( x e. A /\ ( y = ( F ` x ) /\ y = ( G ` x ) ) ) <-> E. y ( ( x e. A /\ y = ( F ` x ) ) /\ ( x e. A /\ y = ( G ` x ) ) ) )
16 fvex 
 |-  ( F ` x ) e. _V
17 eqeq1 
 |-  ( y = ( F ` x ) -> ( y = ( G ` x ) <-> ( F ` x ) = ( G ` x ) ) )
18 16 17 ceqsexv 
 |-  ( E. y ( y = ( F ` x ) /\ y = ( G ` x ) ) <-> ( F ` x ) = ( G ` x ) )
19 18 anbi2i 
 |-  ( ( x e. A /\ E. y ( y = ( F ` x ) /\ y = ( G ` x ) ) ) <-> ( x e. A /\ ( F ` x ) = ( G ` x ) ) )
20 13 15 19 3bitr3i 
 |-  ( E. y ( ( x e. A /\ y = ( F ` x ) ) /\ ( x e. A /\ y = ( G ` x ) ) ) <-> ( x e. A /\ ( F ` x ) = ( G ` x ) ) )
21 20 abbii 
 |-  { x | E. y ( ( x e. A /\ y = ( F ` x ) ) /\ ( x e. A /\ y = ( G ` x ) ) ) } = { x | ( x e. A /\ ( F ` x ) = ( G ` x ) ) }
22 dmopab 
 |-  dom { <. x , y >. | ( ( x e. A /\ y = ( F ` x ) ) /\ ( x e. A /\ y = ( G ` x ) ) ) } = { x | E. y ( ( x e. A /\ y = ( F ` x ) ) /\ ( x e. A /\ y = ( G ` x ) ) ) }
23 df-rab 
 |-  { x e. A | ( F ` x ) = ( G ` x ) } = { x | ( x e. A /\ ( F ` x ) = ( G ` x ) ) }
24 21 22 23 3eqtr4i 
 |-  dom { <. x , y >. | ( ( x e. A /\ y = ( F ` x ) ) /\ ( x e. A /\ y = ( G ` x ) ) ) } = { x e. A | ( F ` x ) = ( G ` x ) }
25 12 24 eqtrdi 
 |-  ( ( F Fn A /\ G Fn A ) -> dom ( F i^i G ) = { x e. A | ( F ` x ) = ( G ` x ) } )