Metamath Proof Explorer

Theorem dmfco

Description: Domains of a function composition. (Contributed by NM, 27-Jan-1997)

Ref Expression
Assertion dmfco ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( 𝐴 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ ( 𝐺 ‘ 𝐴 ) ∈ dom 𝐹 ) )

Proof

Step Hyp Ref Expression
1 eldm2g ⊢ ( 𝐴 ∈ dom 𝐺 → ( 𝐴 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ ( 𝐹 ∘ 𝐺 ) ) )
2 opelco2g ⊢ ( ( 𝐴 ∈ dom 𝐺 ∧ 𝑦 ∈ V ) → ( ⟨ 𝐴 , 𝑦 ⟩ ∈ ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
3 2 elvd ⊢ ( 𝐴 ∈ dom 𝐺 → ( ⟨ 𝐴 , 𝑦 ⟩ ∈ ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
4 3 exbidv ⊢ ( 𝐴 ∈ dom 𝐺 → ( ∃ 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑦 ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
5 1 4 bitrd ⊢ ( 𝐴 ∈ dom 𝐺 → ( 𝐴 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑦 ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
6 5 adantl ⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( 𝐴 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ ∃ 𝑦 ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
7 fvex ⊢ ( 𝐺 ‘ 𝐴 ) ∈ V
8 7 eldm2 ⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ dom 𝐹 ↔ ∃ 𝑦 ⟨ ( 𝐺 ‘ 𝐴 ) , 𝑦 ⟩ ∈ 𝐹 )
9 opeq1 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝐴 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ ( 𝐺 ‘ 𝐴 ) , 𝑦 ⟩ )
10 9 eleq1d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝐴 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ↔ ⟨ ( 𝐺 ‘ 𝐴 ) , 𝑦 ⟩ ∈ 𝐹 ) )
11 7 10 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = ( 𝐺 ‘ 𝐴 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ↔ ⟨ ( 𝐺 ‘ 𝐴 ) , 𝑦 ⟩ ∈ 𝐹 )
12 eqcom ⊢ ( 𝑥 = ( 𝐺 ‘ 𝐴 ) ↔ ( 𝐺 ‘ 𝐴 ) = 𝑥 )
13 funopfvb ⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ( 𝐺 ‘ 𝐴 ) = 𝑥 ↔ ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ) )
14 12 13 bitrid ⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( 𝑥 = ( 𝐺 ‘ 𝐴 ) ↔ ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ) )
15 14 anbi1d ⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ( 𝑥 = ( 𝐺 ‘ 𝐴 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ↔ ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
16 15 exbidv ⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ∃ 𝑥 ( 𝑥 = ( 𝐺 ‘ 𝐴 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ↔ ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
17 11 16 bitr3id ⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ⟨ ( 𝐺 ‘ 𝐴 ) , 𝑦 ⟩ ∈ 𝐹 ↔ ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
18 17 exbidv ⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ∃ 𝑦 ⟨ ( 𝐺 ‘ 𝐴 ) , 𝑦 ⟩ ∈ 𝐹 ↔ ∃ 𝑦 ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
19 8 18 bitrid ⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( ( 𝐺 ‘ 𝐴 ) ∈ dom 𝐹 ↔ ∃ 𝑦 ∃ 𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
20 6 19 bitr4d ⊢ ( ( Fun 𝐺 ∧ 𝐴 ∈ dom 𝐺 ) → ( 𝐴 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ ( 𝐺 ‘ 𝐴 ) ∈ dom 𝐹 ) )