Metamath Proof Explorer


Theorem ex-res

Description: Example for df-res . Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Assertion ex-res
|- ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F |` B ) = { <. 2 , 6 >. } )

Proof

Step Hyp Ref Expression
1 simpl
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> F = { <. 2 , 6 >. , <. 3 , 9 >. } )
2 df-pr
 |-  { <. 2 , 6 >. , <. 3 , 9 >. } = ( { <. 2 , 6 >. } u. { <. 3 , 9 >. } )
3 1 2 eqtrdi
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> F = ( { <. 2 , 6 >. } u. { <. 3 , 9 >. } ) )
4 3 reseq1d
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F |` B ) = ( ( { <. 2 , 6 >. } u. { <. 3 , 9 >. } ) |` B ) )
5 resundir
 |-  ( ( { <. 2 , 6 >. } u. { <. 3 , 9 >. } ) |` B ) = ( ( { <. 2 , 6 >. } |` B ) u. ( { <. 3 , 9 >. } |` B ) )
6 4 5 eqtrdi
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F |` B ) = ( ( { <. 2 , 6 >. } |` B ) u. ( { <. 3 , 9 >. } |` B ) ) )
7 2re
 |-  2 e. RR
8 7 elexi
 |-  2 e. _V
9 6re
 |-  6 e. RR
10 9 elexi
 |-  6 e. _V
11 8 10 relsnop
 |-  Rel { <. 2 , 6 >. }
12 dmsnopss
 |-  dom { <. 2 , 6 >. } C_ { 2 }
13 snsspr2
 |-  { 2 } C_ { 1 , 2 }
14 simpr
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> B = { 1 , 2 } )
15 13 14 sseqtrrid
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> { 2 } C_ B )
16 12 15 sstrid
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> dom { <. 2 , 6 >. } C_ B )
17 relssres
 |-  ( ( Rel { <. 2 , 6 >. } /\ dom { <. 2 , 6 >. } C_ B ) -> ( { <. 2 , 6 >. } |` B ) = { <. 2 , 6 >. } )
18 11 16 17 sylancr
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( { <. 2 , 6 >. } |` B ) = { <. 2 , 6 >. } )
19 1re
 |-  1 e. RR
20 1lt3
 |-  1 < 3
21 19 20 gtneii
 |-  3 =/= 1
22 2lt3
 |-  2 < 3
23 7 22 gtneii
 |-  3 =/= 2
24 21 23 nelpri
 |-  -. 3 e. { 1 , 2 }
25 14 eleq2d
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( 3 e. B <-> 3 e. { 1 , 2 } ) )
26 24 25 mtbiri
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> -. 3 e. B )
27 ressnop0
 |-  ( -. 3 e. B -> ( { <. 3 , 9 >. } |` B ) = (/) )
28 26 27 syl
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( { <. 3 , 9 >. } |` B ) = (/) )
29 18 28 uneq12d
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( ( { <. 2 , 6 >. } |` B ) u. ( { <. 3 , 9 >. } |` B ) ) = ( { <. 2 , 6 >. } u. (/) ) )
30 un0
 |-  ( { <. 2 , 6 >. } u. (/) ) = { <. 2 , 6 >. }
31 29 30 eqtrdi
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( ( { <. 2 , 6 >. } |` B ) u. ( { <. 3 , 9 >. } |` B ) ) = { <. 2 , 6 >. } )
32 6 31 eqtrd
 |-  ( ( F = { <. 2 , 6 >. , <. 3 , 9 >. } /\ B = { 1 , 2 } ) -> ( F |` B ) = { <. 2 , 6 >. } )