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 >. } )