Metamath Proof Explorer

Theorem dfatdmfcoafv2

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

Ref Expression
Assertion dfatdmfcoafv2 ( 𝐺 defAt 𝐴 → ( 𝐴 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ ( 𝐺 '''' 𝐴 ) ∈ dom 𝐹 ) )

Proof

Step Hyp Ref Expression
1 dfatafv2ex ⊢ ( 𝐺 defAt 𝐴 → ( 𝐺 '''' 𝐴 ) ∈ V )
2 opeq1 ⊢ ( 𝑥 = ( 𝐺 '''' 𝐴 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ ( 𝐺 '''' 𝐴 ) , 𝑦 ⟩ )
3 2 eleq1d ⊢ ( 𝑥 = ( 𝐺 '''' 𝐴 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ↔ ⟨ ( 𝐺 '''' 𝐴 ) , 𝑦 ⟩ ∈ 𝐹 ) )
4 3 ceqsexgv ⊢ ( ( 𝐺 '''' 𝐴 ) ∈ V → ( ∃ 𝑥 ( 𝑥 = ( 𝐺 '''' 𝐴 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ↔ ⟨ ( 𝐺 '''' 𝐴 ) , 𝑦 ⟩ ∈ 𝐹 ) )
5 4 bicomd ⊢ ( ( 𝐺 '''' 𝐴 ) ∈ V → ( ⟨ ( 𝐺 '''' 𝐴 ) , 𝑦 ⟩ ∈ 𝐹 ↔ ∃ 𝑥 ( 𝑥 = ( 𝐺 '''' 𝐴 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
6 1 5 syl ⊢ ( 𝐺 defAt 𝐴 → ( ⟨ ( 𝐺 '''' 𝐴 ) , 𝑦 ⟩ ∈ 𝐹 ↔ ∃ 𝑥 ( 𝑥 = ( 𝐺 '''' 𝐴 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
7 eqcom ⊢ ( 𝑥 = ( 𝐺 '''' 𝐴 ) ↔ ( 𝐺 '''' 𝐴 ) = 𝑥 )
8 dfatopafv2b ⊢ ( ( 𝐺 defAt 𝐴 ∧ 𝑥 ∈ V ) → ( ( 𝐺 '''' 𝐴 ) = 𝑥 ↔ ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ) )
9 8 elvd ⊢ ( 𝐺 defAt 𝐴 → ( ( 𝐺 '''' 𝐴 ) = 𝑥 ↔ ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ) )
10 7 9 syl5bb ⊢ ( 𝐺 defAt 𝐴 → ( 𝑥 = ( 𝐺 '''' 𝐴 ) ↔ ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ) )
11 10 anbi1d ⊢ ( 𝐺 defAt 𝐴 → ( ( 𝑥 = ( 𝐺 '''' 𝐴 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ↔ ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
12 11 exbidv ⊢ ( 𝐺 defAt 𝐴 → ( ∃ 𝑥 ( 𝑥 = ( 𝐺 '''' 𝐴 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ↔ ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
13 6 12 bitrd ⊢ ( 𝐺 defAt 𝐴 → ( ⟨ ( 𝐺 '''' 𝐴 ) , 𝑦 ⟩ ∈ 𝐹 ↔ ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
14 13 exbidv ⊢ ( 𝐺 defAt 𝐴 → ( ∃ 𝑦 ⟨ ( 𝐺 '''' 𝐴 ) , 𝑦 ⟩ ∈ 𝐹 ↔ ∃ 𝑦 ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
15 eldm2g ⊢ ( ( 𝐺 '''' 𝐴 ) ∈ V → ( ( 𝐺 '''' 𝐴 ) ∈ dom 𝐹 ↔ ∃ 𝑦 ⟨ ( 𝐺 '''' 𝐴 ) , 𝑦 ⟩ ∈ 𝐹 ) )
16 1 15 syl ⊢ ( 𝐺 defAt 𝐴 → ( ( 𝐺 '''' 𝐴 ) ∈ dom 𝐹 ↔ ∃ 𝑦 ⟨ ( 𝐺 '''' 𝐴 ) , 𝑦 ⟩ ∈ 𝐹 ) )
17 df-dfat ⊢ ( 𝐺 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐺 ∧ Fun ( 𝐺 ↾ { 𝐴 } ) ) )
18 eldm2g ⊢ ( 𝐴 ∈ dom 𝐺 → ( 𝐴 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ ( 𝐹 ∘ 𝐺 ) ) )
19 opelco2g ⊢ ( ( 𝐴 ∈ dom 𝐺 ∧ 𝑦 ∈ V ) → ( ⟨ 𝐴 , 𝑦 ⟩ ∈ ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
20 19 elvd ⊢ ( 𝐴 ∈ dom 𝐺 → ( ⟨ 𝐴 , 𝑦 ⟩ ∈ ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
21 20 exbidv ⊢ ( 𝐴 ∈ dom 𝐺 → ( ∃ 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑦 ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
22 18 21 bitrd ⊢ ( 𝐴 ∈ dom 𝐺 → ( 𝐴 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑦 ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
23 22 adantr ⊢ ( ( 𝐴 ∈ dom 𝐺 ∧ Fun ( 𝐺 ↾ { 𝐴 } ) ) → ( 𝐴 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑦 ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
24 17 23 sylbi ⊢ ( 𝐺 defAt 𝐴 → ( 𝐴 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑦 ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
25 14 16 24 3bitr4rd ⊢ ( 𝐺 defAt 𝐴 → ( 𝐴 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ ( 𝐺 '''' 𝐴 ) ∈ dom 𝐹 ) )