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 syl5bb ( ( 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 syl5bb ( ( Fun 𝐺𝐴 ∈ dom 𝐺 ) → ( ( 𝐺𝐴 ) ∈ dom 𝐹 ↔ ∃ 𝑦𝑥 ( ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐺 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ) )
20 6 19 bitr4d ( ( Fun 𝐺𝐴 ∈ dom 𝐺 ) → ( 𝐴 ∈ dom ( 𝐹𝐺 ) ↔ ( 𝐺𝐴 ) ∈ dom 𝐹 ) )