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

Metamath Proof Explorer

Theorem cofunex2g

Description: Existence of a composition when the second member is one-to-one. (Contributed by NM, 8-Oct-2007)

Ref Expression
Assertion cofunex2g ( ( 𝐴 ∈ 𝑉 ∧ Fun ◡ 𝐵 ) → ( 𝐴 ∘ 𝐵 ) ∈ V )

Proof

Step Hyp Ref Expression
1 cnvexg ⊢ ( 𝐴 ∈ 𝑉 → ◡ 𝐴 ∈ V )
2 cofunexg ⊢ ( ( Fun ◡ 𝐵 ∧ ◡ 𝐴 ∈ V ) → ( ◡ 𝐵 ∘ ◡ 𝐴 ) ∈ V )
3 1 2 sylan2 ⊢ ( ( Fun ◡ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( ◡ 𝐵 ∘ ◡ 𝐴 ) ∈ V )
4 cnvco ⊢ ◡ ( ◡ 𝐵 ∘ ◡ 𝐴 ) = ( ◡ ◡ 𝐴 ∘ ◡ ◡ 𝐵 )
5 cocnvcnv2 ⊢ ( ◡ ◡ 𝐴 ∘ ◡ ◡ 𝐵 ) = ( ◡ ◡ 𝐴 ∘ 𝐵 )
6 cocnvcnv1 ⊢ ( ◡ ◡ 𝐴 ∘ 𝐵 ) = ( 𝐴 ∘ 𝐵 )
7 4 5 6 3eqtrri ⊢ ( 𝐴 ∘ 𝐵 ) = ◡ ( ◡ 𝐵 ∘ ◡ 𝐴 )
8 cnvexg ⊢ ( ( ◡ 𝐵 ∘ ◡ 𝐴 ) ∈ V → ◡ ( ◡ 𝐵 ∘ ◡ 𝐴 ) ∈ V )
9 7 8 eqeltrid ⊢ ( ( ◡ 𝐵 ∘ ◡ 𝐴 ) ∈ V → ( 𝐴 ∘ 𝐵 ) ∈ V )
10 3 9 syl ⊢ ( ( Fun ◡ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∘ 𝐵 ) ∈ V )
11 10 ancoms ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Fun ◡ 𝐵 ) → ( 𝐴 ∘ 𝐵 ) ∈ V )