Metamath Proof Explorer

Theorem tposres

Description: The transposition restricted to a relation. (Contributed by Zhi Wang, 6-Oct-2025)

Ref Expression
Assertion tposres 
|- ( Rel R -> ( tpos F |` R ) = tpos ( F |` `' R ) )

Proof

Step Hyp Ref Expression
1 0nelrel0 
 |-  ( Rel R -> -. (/) e. R )
2 nel2nelin 
 |-  ( -. (/) e. R -> -. (/) e. ( dom F i^i R ) )
3 1 2 syl 
 |-  ( Rel R -> -. (/) e. ( dom F i^i R ) )
4 3 tposres3 
 |-  ( Rel R -> ( tpos F |` R ) = tpos ( F |` `' R ) )