Metamath Proof Explorer

Theorem elsetpreimafveq

Description: If two preimages of function values contain elements with identical function values, then both preimages are equal. (Contributed by AV, 8-Mar-2024)

Ref Expression
Hypothesis setpreimafvex.p 
|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
Assertion elsetpreimafveq 
|- ( ( F Fn A /\ ( S e. P /\ R e. P ) /\ ( X e. S /\ Y e. R ) ) -> ( ( F ` X ) = ( F ` Y ) -> S = R ) )

Proof

Step Hyp Ref Expression
1 setpreimafvex.p 
 |-  P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
2 eqeq2 
 |-  ( ( F ` X ) = ( F ` Y ) -> ( ( F ` x ) = ( F ` X ) <-> ( F ` x ) = ( F ` Y ) ) )
3 2 rabbidv 
 |-  ( ( F ` X ) = ( F ` Y ) -> { x e. A | ( F ` x ) = ( F ` X ) } = { x e. A | ( F ` x ) = ( F ` Y ) } )
4 3 adantl 
 |-  ( ( ( F Fn A /\ ( S e. P /\ R e. P ) /\ ( X e. S /\ Y e. R ) ) /\ ( F ` X ) = ( F ` Y ) ) -> { x e. A | ( F ` x ) = ( F ` X ) } = { x e. A | ( F ` x ) = ( F ` Y ) } )
5 id 
 |-  ( F Fn A -> F Fn A )
6 simpl 
 |-  ( ( S e. P /\ R e. P ) -> S e. P )
7 simpl 
 |-  ( ( X e. S /\ Y e. R ) -> X e. S )
8 5 6 7 3anim123i 
 |-  ( ( F Fn A /\ ( S e. P /\ R e. P ) /\ ( X e. S /\ Y e. R ) ) -> ( F Fn A /\ S e. P /\ X e. S ) )
9 8 adantr 
 |-  ( ( ( F Fn A /\ ( S e. P /\ R e. P ) /\ ( X e. S /\ Y e. R ) ) /\ ( F ` X ) = ( F ` Y ) ) -> ( F Fn A /\ S e. P /\ X e. S ) )
10 1 elsetpreimafvrab 
 |-  ( ( F Fn A /\ S e. P /\ X e. S ) -> S = { x e. A | ( F ` x ) = ( F ` X ) } )
11 9 10 syl 
 |-  ( ( ( F Fn A /\ ( S e. P /\ R e. P ) /\ ( X e. S /\ Y e. R ) ) /\ ( F ` X ) = ( F ` Y ) ) -> S = { x e. A | ( F ` x ) = ( F ` X ) } )
12 simpr 
 |-  ( ( S e. P /\ R e. P ) -> R e. P )
13 simpr 
 |-  ( ( X e. S /\ Y e. R ) -> Y e. R )
14 5 12 13 3anim123i 
 |-  ( ( F Fn A /\ ( S e. P /\ R e. P ) /\ ( X e. S /\ Y e. R ) ) -> ( F Fn A /\ R e. P /\ Y e. R ) )
15 14 adantr 
 |-  ( ( ( F Fn A /\ ( S e. P /\ R e. P ) /\ ( X e. S /\ Y e. R ) ) /\ ( F ` X ) = ( F ` Y ) ) -> ( F Fn A /\ R e. P /\ Y e. R ) )
16 1 elsetpreimafvrab 
 |-  ( ( F Fn A /\ R e. P /\ Y e. R ) -> R = { x e. A | ( F ` x ) = ( F ` Y ) } )
17 15 16 syl 
 |-  ( ( ( F Fn A /\ ( S e. P /\ R e. P ) /\ ( X e. S /\ Y e. R ) ) /\ ( F ` X ) = ( F ` Y ) ) -> R = { x e. A | ( F ` x ) = ( F ` Y ) } )
18 4 11 17 3eqtr4d 
 |-  ( ( ( F Fn A /\ ( S e. P /\ R e. P ) /\ ( X e. S /\ Y e. R ) ) /\ ( F ` X ) = ( F ` Y ) ) -> S = R )
19 18 ex 
 |-  ( ( F Fn A /\ ( S e. P /\ R e. P ) /\ ( X e. S /\ Y e. R ) ) -> ( ( F ` X ) = ( F ` Y ) -> S = R ) )