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 𝐺 ) )