Metamath Proof Explorer

Theorem dfatdmfcoafv2

Description: Domain of a function composition, analogous to dmfco . (Contributed by AV, 7-Sep-2022)

Ref Expression
Assertion dfatdmfcoafv2 ⊢ G defAt A → A ∈ dom ⁡ F ∘ G ↔ G '''' A ∈ dom ⁡ F

Proof

Step Hyp Ref Expression
1 dfatafv2ex ⊢ G defAt A → G '''' A ∈ V
2 opeq1 ⊢ x = G '''' A → x y = G '''' A y
3 2 eleq1d ⊢ x = G '''' A → x y ∈ F ↔ G '''' A y ∈ F
4 3 ceqsexgv ⊢ G '''' A ∈ V → ∃ x x = G '''' A ∧ x y ∈ F ↔ G '''' A y ∈ F
5 4 bicomd ⊢ G '''' A ∈ V → G '''' A y ∈ F ↔ ∃ x x = G '''' A ∧ x y ∈ F
6 1 5 syl ⊢ G defAt A → G '''' A y ∈ F ↔ ∃ x x = G '''' A ∧ x y ∈ F
7 eqcom ⊢ x = G '''' A ↔ G '''' A = x
8 dfatopafv2b ⊢ G defAt A ∧ x ∈ V → G '''' A = x ↔ A x ∈ G
9 8 elvd ⊢ G defAt A → G '''' A = x ↔ A x ∈ G
10 7 9 bitrid ⊢ G defAt A → x = G '''' A ↔ A x ∈ G
11 10 anbi1d ⊢ G defAt A → x = G '''' A ∧ x y ∈ F ↔ A x ∈ G ∧ x y ∈ F
12 11 exbidv ⊢ G defAt A → ∃ x x = G '''' A ∧ x y ∈ F ↔ ∃ x A x ∈ G ∧ x y ∈ F
13 6 12 bitrd ⊢ G defAt A → G '''' A y ∈ F ↔ ∃ x A x ∈ G ∧ x y ∈ F
14 13 exbidv ⊢ G defAt A → ∃ y G '''' A y ∈ F ↔ ∃ y ∃ x A x ∈ G ∧ x y ∈ F
15 eldm2g ⊢ G '''' A ∈ V → G '''' A ∈ dom ⁡ F ↔ ∃ y G '''' A y ∈ F
16 1 15 syl ⊢ G defAt A → G '''' A ∈ dom ⁡ F ↔ ∃ y G '''' A y ∈ F
17 df-dfat ⊢ G defAt A ↔ A ∈ dom ⁡ G ∧ Fun ⁡ G ↾ A
18 eldm2g ⊢ A ∈ dom ⁡ G → A ∈ dom ⁡ F ∘ G ↔ ∃ y A y ∈ F ∘ G
19 opelco2g ⊢ A ∈ dom ⁡ G ∧ y ∈ V → A y ∈ F ∘ G ↔ ∃ x A x ∈ G ∧ x y ∈ F
20 19 elvd ⊢ A ∈ dom ⁡ G → A y ∈ F ∘ G ↔ ∃ x A x ∈ G ∧ x y ∈ F
21 20 exbidv ⊢ A ∈ dom ⁡ G → ∃ y A y ∈ F ∘ G ↔ ∃ y ∃ x A x ∈ G ∧ x y ∈ F
22 18 21 bitrd ⊢ A ∈ dom ⁡ G → A ∈ dom ⁡ F ∘ G ↔ ∃ y ∃ x A x ∈ G ∧ x y ∈ F
23 22 adantr ⊢ A ∈ dom ⁡ G ∧ Fun ⁡ G ↾ A → A ∈ dom ⁡ F ∘ G ↔ ∃ y ∃ x A x ∈ G ∧ x y ∈ F
24 17 23 sylbi ⊢ G defAt A → A ∈ dom ⁡ F ∘ G ↔ ∃ y ∃ x A x ∈ G ∧ x y ∈ F
25 14 16 24 3bitr4rd ⊢ G defAt A → A ∈ dom ⁡ F ∘ G ↔ G '''' A ∈ dom ⁡ F