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

Metamath Proof Explorer

Theorem cofmpt2

Description: Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 15-Jul-2023)

Ref Expression
Hypotheses cofmpt2.1 ⊢ φ ∧ y = F ⁡ x → C = D
cofmpt2.2 ⊢ φ ∧ y ∈ B → C ∈ E
cofmpt2.3 ⊢ φ → F : A ⟶ B
cofmpt2.4 ⊢ φ → D ∈ V
Assertion cofmpt2 ⊢ φ → y ∈ B ⟼ C ∘ F = x ∈ A ⟼ D

Proof

Step Hyp Ref Expression
1 cofmpt2.1 ⊢ φ ∧ y = F ⁡ x → C = D
2 cofmpt2.2 ⊢ φ ∧ y ∈ B → C ∈ E
3 cofmpt2.3 ⊢ φ → F : A ⟶ B
4 cofmpt2.4 ⊢ φ → D ∈ V
5 2 fmpttd ⊢ φ → y ∈ B ⟼ C : B ⟶ E
6 fcompt ⊢ y ∈ B ⟼ C : B ⟶ E ∧ F : A ⟶ B → y ∈ B ⟼ C ∘ F = x ∈ A ⟼ y ∈ B ⟼ C ⁡ F ⁡ x
7 5 3 6 syl2anc ⊢ φ → y ∈ B ⟼ C ∘ F = x ∈ A ⟼ y ∈ B ⟼ C ⁡ F ⁡ x
8 eqid ⊢ y ∈ B ⟼ C = y ∈ B ⟼ C
9 1 adantlr ⊢ φ ∧ x ∈ A ∧ y = F ⁡ x → C = D
10 3 ffvelcdmda ⊢ φ ∧ x ∈ A → F ⁡ x ∈ B
11 4 adantr ⊢ φ ∧ x ∈ A → D ∈ V
12 8 9 10 11 fvmptd2 ⊢ φ ∧ x ∈ A → y ∈ B ⟼ C ⁡ F ⁡ x = D
13 12 mpteq2dva ⊢ φ → x ∈ A ⟼ y ∈ B ⟼ C ⁡ F ⁡ x = x ∈ A ⟼ D
14 7 13 eqtrd ⊢ φ → y ∈ B ⟼ C ∘ F = x ∈ A ⟼ D