This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oftpos

Description: The transposition of the value of a function operation for two functions is the value of the function operation for the two functions transposed. (Contributed by Stefan O'Rear, 17-Jul-2018)

Ref Expression
Assertion oftpos ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → tpos ( 𝐹 ∘f 𝑅 𝐺 ) = ( tpos 𝐹 ∘f 𝑅 tpos 𝐺 ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐹 ∈ 𝑉 → 𝐹 ∈ V )
2 1 adantr ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → 𝐹 ∈ V )
3 elex ⊢ ( 𝐺 ∈ 𝑊 → 𝐺 ∈ V )
4 3 adantl ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → 𝐺 ∈ V )
5 funmpt ⊢ Fun ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } )
6 5 a1i ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → Fun ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
7 dftpos4 ⊢ tpos 𝐹 = ( 𝐹 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
8 tposexg ⊢ ( 𝐹 ∈ 𝑉 → tpos 𝐹 ∈ V )
9 8 adantr ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → tpos 𝐹 ∈ V )
10 7 9 eqeltrrid ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( 𝐹 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ∈ V )
11 dftpos4 ⊢ tpos 𝐺 = ( 𝐺 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
12 tposexg ⊢ ( 𝐺 ∈ 𝑊 → tpos 𝐺 ∈ V )
13 12 adantl ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → tpos 𝐺 ∈ V )
14 11 13 eqeltrrid ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( 𝐺 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ∈ V )
15 ofco2 ⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ ( Fun ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ∧ ( 𝐹 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ∈ V ∧ ( 𝐺 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ∈ V ) ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) = ( ( 𝐹 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ∘f 𝑅 ( 𝐺 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ) )
16 2 4 6 10 14 15 syl23anc ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) = ( ( 𝐹 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ∘f 𝑅 ( 𝐺 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ) )
17 dftpos4 ⊢ tpos ( 𝐹 ∘f 𝑅 𝐺 ) = ( ( 𝐹 ∘f 𝑅 𝐺 ) ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) )
18 7 11 oveq12i ⊢ ( tpos 𝐹 ∘f 𝑅 tpos 𝐺 ) = ( ( 𝐹 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) ∘f 𝑅 ( 𝐺 ∘ ( 𝑥 ∈ ( ( V × V ) ∪ { ∅ } ) ↦ ∪ ◡ { 𝑥 } ) ) )
19 16 17 18 3eqtr4g ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → tpos ( 𝐹 ∘f 𝑅 𝐺 ) = ( tpos 𝐹 ∘f 𝑅 tpos 𝐺 ) )