Metamath Proof Explorer

Theorem tposrescnv

Description: The transposition restricted to a converse is the transposition of the restricted class, with the empty set removed from the domain. Note that the right hand side is a more useful form of ` ( tpos ( F |`` R ) |`( _V \ { (/) } ) ) by df-tpos . (Contributed by Zhi Wang, 6-Oct-2025)

Ref Expression
Assertion tposrescnv ( tpos 𝐹 ↾ ◡ 𝑅 ) = ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) )

Proof

Step Hyp Ref Expression
1 df-tpos ⊢ tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
2 1 reseq1i ⊢ ( tpos 𝐹 ↾ ◡ 𝑅 ) = ( ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ↾ ◡ 𝑅 )
3 resco ⊢ ( ( 𝐹 ∘ ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ↾ ◡ 𝑅 ) = ( 𝐹 ∘ ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ↾ ◡ 𝑅 ) )
4 resmpt3 ⊢ ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ↾ ◡ 𝑅 ) = ( 𝑥 ∈ ( ( ◡ dom 𝐹 ∪ { ∅ } ) ∩ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } )
5 cnvin ⊢ ◡ ( 𝑅 ∩ dom 𝐹 ) = ( ◡ 𝑅 ∩ ◡ dom 𝐹 )
6 dmres ⊢ dom ( 𝐹 ↾ 𝑅 ) = ( 𝑅 ∩ dom 𝐹 )
7 6 cnveqi ⊢ ◡ dom ( 𝐹 ↾ 𝑅 ) = ◡ ( 𝑅 ∩ dom 𝐹 )
8 incom ⊢ ( ( ◡ dom 𝐹 ∪ { ∅ } ) ∩ ◡ 𝑅 ) = ( ◡ 𝑅 ∩ ( ◡ dom 𝐹 ∪ { ∅ } ) )
9 indi ⊢ ( ◡ 𝑅 ∩ ( ◡ dom 𝐹 ∪ { ∅ } ) ) = ( ( ◡ 𝑅 ∩ ◡ dom 𝐹 ) ∪ ( ◡ 𝑅 ∩ { ∅ } ) )
10 relcnv ⊢ Rel ◡ 𝑅
11 0nelrel0 ⊢ ( Rel ◡ 𝑅 → ¬ ∅ ∈ ◡ 𝑅 )
12 10 11 ax-mp ⊢ ¬ ∅ ∈ ◡ 𝑅
13 disjsn ⊢ ( ( ◡ 𝑅 ∩ { ∅ } ) = ∅ ↔ ¬ ∅ ∈ ◡ 𝑅 )
14 12 13 mpbir ⊢ ( ◡ 𝑅 ∩ { ∅ } ) = ∅
15 14 uneq2i ⊢ ( ( ◡ 𝑅 ∩ ◡ dom 𝐹 ) ∪ ( ◡ 𝑅 ∩ { ∅ } ) ) = ( ( ◡ 𝑅 ∩ ◡ dom 𝐹 ) ∪ ∅ )
16 un0 ⊢ ( ( ◡ 𝑅 ∩ ◡ dom 𝐹 ) ∪ ∅ ) = ( ◡ 𝑅 ∩ ◡ dom 𝐹 )
17 15 16 eqtri ⊢ ( ( ◡ 𝑅 ∩ ◡ dom 𝐹 ) ∪ ( ◡ 𝑅 ∩ { ∅ } ) ) = ( ◡ 𝑅 ∩ ◡ dom 𝐹 )
18 8 9 17 3eqtri ⊢ ( ( ◡ dom 𝐹 ∪ { ∅ } ) ∩ ◡ 𝑅 ) = ( ◡ 𝑅 ∩ ◡ dom 𝐹 )
19 5 7 18 3eqtr4ri ⊢ ( ( ◡ dom 𝐹 ∪ { ∅ } ) ∩ ◡ 𝑅 ) = ◡ dom ( 𝐹 ↾ 𝑅 )
20 19 mpteq1i ⊢ ( 𝑥 ∈ ( ( ◡ dom 𝐹 ∪ { ∅ } ) ∩ ◡ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) = ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ 𝑅 ) ↦ ∪ ◡ { 𝑥 } )
21 4 20 eqtri ⊢ ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ↾ ◡ 𝑅 ) = ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ 𝑅 ) ↦ ∪ ◡ { 𝑥 } )
22 21 coeq2i ⊢ ( 𝐹 ∘ ( ( 𝑥 ∈ ( ◡ dom 𝐹 ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ↾ ◡ 𝑅 ) ) = ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) )
23 2 3 22 3eqtri ⊢ ( tpos 𝐹 ↾ ◡ 𝑅 ) = ( 𝐹 ∘ ( 𝑥 ∈ ◡ dom ( 𝐹 ↾ 𝑅 ) ↦ ∪ ◡ { 𝑥 } ) )