Metamath Proof Explorer

Theorem tposresg

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

Ref Expression
Assertion tposresg ( tpos 𝐹 ↾ 𝑅 ) = ( ( tpos 𝐹 ↾ ◡ ◡ 𝑅 ) ∪ ( 𝐹 ↾ ( 𝑅 ∩ { ∅ } ) ) )

Proof

Step Hyp Ref Expression
1 rescom ⊢ ( ( tpos 𝐹 ↾ ( ( V × V ) ∪ { ∅ } ) ) ↾ 𝑅 ) = ( ( tpos 𝐹 ↾ 𝑅 ) ↾ ( ( V × V ) ∪ { ∅ } ) )
2 reltpos ⊢ Rel tpos 𝐹
3 dmtposss ⊢ dom tpos 𝐹 ⊆ ( ( V × V ) ∪ { ∅ } )
4 relssres ⊢ ( ( Rel tpos 𝐹 ∧ dom tpos 𝐹 ⊆ ( ( V × V ) ∪ { ∅ } ) ) → ( tpos 𝐹 ↾ ( ( V × V ) ∪ { ∅ } ) ) = tpos 𝐹 )
5 2 3 4 mp2an ⊢ ( tpos 𝐹 ↾ ( ( V × V ) ∪ { ∅ } ) ) = tpos 𝐹
6 5 reseq1i ⊢ ( ( tpos 𝐹 ↾ ( ( V × V ) ∪ { ∅ } ) ) ↾ 𝑅 ) = ( tpos 𝐹 ↾ 𝑅 )
7 resres ⊢ ( ( tpos 𝐹 ↾ 𝑅 ) ↾ ( ( V × V ) ∪ { ∅ } ) ) = ( tpos 𝐹 ↾ ( 𝑅 ∩ ( ( V × V ) ∪ { ∅ } ) ) )
8 1 6 7 3eqtr3i ⊢ ( tpos 𝐹 ↾ 𝑅 ) = ( tpos 𝐹 ↾ ( 𝑅 ∩ ( ( V × V ) ∪ { ∅ } ) ) )
9 indi ⊢ ( 𝑅 ∩ ( ( V × V ) ∪ { ∅ } ) ) = ( ( 𝑅 ∩ ( V × V ) ) ∪ ( 𝑅 ∩ { ∅ } ) )
10 cnvcnv ⊢ ◡ ◡ 𝑅 = ( 𝑅 ∩ ( V × V ) )
11 10 uneq1i ⊢ ( ◡ ◡ 𝑅 ∪ ( 𝑅 ∩ { ∅ } ) ) = ( ( 𝑅 ∩ ( V × V ) ) ∪ ( 𝑅 ∩ { ∅ } ) )
12 9 11 eqtr4i ⊢ ( 𝑅 ∩ ( ( V × V ) ∪ { ∅ } ) ) = ( ◡ ◡ 𝑅 ∪ ( 𝑅 ∩ { ∅ } ) )
13 12 reseq2i ⊢ ( tpos 𝐹 ↾ ( 𝑅 ∩ ( ( V × V ) ∪ { ∅ } ) ) ) = ( tpos 𝐹 ↾ ( ◡ ◡ 𝑅 ∪ ( 𝑅 ∩ { ∅ } ) ) )
14 resundi ⊢ ( tpos 𝐹 ↾ ( ◡ ◡ 𝑅 ∪ ( 𝑅 ∩ { ∅ } ) ) ) = ( ( tpos 𝐹 ↾ ◡ ◡ 𝑅 ) ∪ ( tpos 𝐹 ↾ ( 𝑅 ∩ { ∅ } ) ) )
15 rescom ⊢ ( ( tpos 𝐹 ↾ { ∅ } ) ↾ 𝑅 ) = ( ( tpos 𝐹 ↾ 𝑅 ) ↾ { ∅ } )
16 tposres0 ⊢ ( tpos 𝐹 ↾ { ∅ } ) = ( 𝐹 ↾ { ∅ } )
17 16 reseq1i ⊢ ( ( tpos 𝐹 ↾ { ∅ } ) ↾ 𝑅 ) = ( ( 𝐹 ↾ { ∅ } ) ↾ 𝑅 )
18 resres ⊢ ( ( tpos 𝐹 ↾ 𝑅 ) ↾ { ∅ } ) = ( tpos 𝐹 ↾ ( 𝑅 ∩ { ∅ } ) )
19 15 17 18 3eqtr3ri ⊢ ( tpos 𝐹 ↾ ( 𝑅 ∩ { ∅ } ) ) = ( ( 𝐹 ↾ { ∅ } ) ↾ 𝑅 )
20 rescom ⊢ ( ( 𝐹 ↾ { ∅ } ) ↾ 𝑅 ) = ( ( 𝐹 ↾ 𝑅 ) ↾ { ∅ } )
21 resres ⊢ ( ( 𝐹 ↾ 𝑅 ) ↾ { ∅ } ) = ( 𝐹 ↾ ( 𝑅 ∩ { ∅ } ) )
22 19 20 21 3eqtri ⊢ ( tpos 𝐹 ↾ ( 𝑅 ∩ { ∅ } ) ) = ( 𝐹 ↾ ( 𝑅 ∩ { ∅ } ) )
23 22 uneq2i ⊢ ( ( tpos 𝐹 ↾ ◡ ◡ 𝑅 ) ∪ ( tpos 𝐹 ↾ ( 𝑅 ∩ { ∅ } ) ) ) = ( ( tpos 𝐹 ↾ ◡ ◡ 𝑅 ) ∪ ( 𝐹 ↾ ( 𝑅 ∩ { ∅ } ) ) )
24 14 23 eqtri ⊢ ( tpos 𝐹 ↾ ( ◡ ◡ 𝑅 ∪ ( 𝑅 ∩ { ∅ } ) ) ) = ( ( tpos 𝐹 ↾ ◡ ◡ 𝑅 ) ∪ ( 𝐹 ↾ ( 𝑅 ∩ { ∅ } ) ) )
25 8 13 24 3eqtri ⊢ ( tpos 𝐹 ↾ 𝑅 ) = ( ( tpos 𝐹 ↾ ◡ ◡ 𝑅 ) ∪ ( 𝐹 ↾ ( 𝑅 ∩ { ∅ } ) ) )