Metamath Proof Explorer

Theorem dfatco

Description: The predicate "defined at" for a function composition. (Contributed by AV, 8-Sep-2022)

Ref Expression
Assertion dfatco ⊢ G defAt X ∧ F defAt G '''' X → F ∘ G defAt X

Proof

Step Hyp Ref Expression
1 dfatcolem ⊢ G defAt X ∧ F defAt G '''' X → ∃! y X F ∘ G y
2 euex ⊢ ∃! y X F ∘ G y → ∃ y X F ∘ G y
3 1 2 syl ⊢ G defAt X ∧ F defAt G '''' X → ∃ y X F ∘ G y
4 df-dm ⊢ dom ⁡ F ∘ G = x | ∃ y x F ∘ G y
5 4 eleq2i ⊢ X ∈ dom ⁡ F ∘ G ↔ X ∈ x | ∃ y x F ∘ G y
6 df-dfat ⊢ G defAt X ↔ X ∈ dom ⁡ G ∧ Fun ⁡ G ↾ X
7 6 simplbi ⊢ G defAt X → X ∈ dom ⁡ G
8 7 adantr ⊢ G defAt X ∧ F defAt G '''' X → X ∈ dom ⁡ G
9 breq1 ⊢ x = X → x F ∘ G y ↔ X F ∘ G y
10 9 exbidv ⊢ x = X → ∃ y x F ∘ G y ↔ ∃ y X F ∘ G y
11 10 elabg ⊢ X ∈ dom ⁡ G → X ∈ x | ∃ y x F ∘ G y ↔ ∃ y X F ∘ G y
12 8 11 syl ⊢ G defAt X ∧ F defAt G '''' X → X ∈ x | ∃ y x F ∘ G y ↔ ∃ y X F ∘ G y
13 5 12 bitrid ⊢ G defAt X ∧ F defAt G '''' X → X ∈ dom ⁡ F ∘ G ↔ ∃ y X F ∘ G y
14 3 13 mpbird ⊢ G defAt X ∧ F defAt G '''' X → X ∈ dom ⁡ F ∘ G
15 dfdfat2 ⊢ F ∘ G defAt X ↔ X ∈ dom ⁡ F ∘ G ∧ ∃! y X F ∘ G y
16 14 1 15 sylanbrc ⊢ G defAt X ∧ F defAt G '''' X → F ∘ G defAt X