Metamath Proof Explorer

Theorem dmcosseq

Description: Domain of a composition. (Contributed by NM, 28-May-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011) Avoid ax-11 . (Revised by BTernaryTau, 23-Jun-2025) Avoid ax-10 and ax-12 . (Revised by TM, 31-Dec-2025)

Ref Expression
Assertion dmcosseq ( ran 𝐵 ⊆ dom 𝐴 → dom ( 𝐴 ∘ 𝐵 ) = dom 𝐵 )

Proof

Step Hyp Ref Expression
1 dmcoss ⊢ dom ( 𝐴 ∘ 𝐵 ) ⊆ dom 𝐵
2 1 a1i ⊢ ( ran 𝐵 ⊆ dom 𝐴 → dom ( 𝐴 ∘ 𝐵 ) ⊆ dom 𝐵 )
3 ssel ⊢ ( ran 𝐵 ⊆ dom 𝐴 → ( 𝑦 ∈ ran 𝐵 → 𝑦 ∈ dom 𝐴 ) )
4 vex ⊢ 𝑦 ∈ V
5 4 elrn ⊢ ( 𝑦 ∈ ran 𝐵 ↔ ∃ 𝑥 𝑥 𝐵 𝑦 )
6 4 eldm ⊢ ( 𝑦 ∈ dom 𝐴 ↔ ∃ 𝑧 𝑦 𝐴 𝑧 )
7 5 6 imbi12i ⊢ ( ( 𝑦 ∈ ran 𝐵 → 𝑦 ∈ dom 𝐴 ) ↔ ( ∃ 𝑥 𝑥 𝐵 𝑦 → ∃ 𝑧 𝑦 𝐴 𝑧 ) )
8 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝐵 𝑦 ↔ 𝑧 𝐵 𝑦 ) )
9 8 19.8aw ⊢ ( 𝑥 𝐵 𝑦 → ∃ 𝑥 𝑥 𝐵 𝑦 )
10 9 imim1i ⊢ ( ( ∃ 𝑥 𝑥 𝐵 𝑦 → ∃ 𝑧 𝑦 𝐴 𝑧 ) → ( 𝑥 𝐵 𝑦 → ∃ 𝑧 𝑦 𝐴 𝑧 ) )
11 pm3.2 ⊢ ( 𝑥 𝐵 𝑦 → ( 𝑦 𝐴 𝑧 → ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
12 11 eximdv ⊢ ( 𝑥 𝐵 𝑦 → ( ∃ 𝑧 𝑦 𝐴 𝑧 → ∃ 𝑧 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
13 10 12 sylcom ⊢ ( ( ∃ 𝑥 𝑥 𝐵 𝑦 → ∃ 𝑧 𝑦 𝐴 𝑧 ) → ( 𝑥 𝐵 𝑦 → ∃ 𝑧 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
14 7 13 sylbi ⊢ ( ( 𝑦 ∈ ran 𝐵 → 𝑦 ∈ dom 𝐴 ) → ( 𝑥 𝐵 𝑦 → ∃ 𝑧 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
15 3 14 syl ⊢ ( ran 𝐵 ⊆ dom 𝐴 → ( 𝑥 𝐵 𝑦 → ∃ 𝑧 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
16 15 eximdv ⊢ ( ran 𝐵 ⊆ dom 𝐴 → ( ∃ 𝑦 𝑥 𝐵 𝑦 → ∃ 𝑦 ∃ 𝑧 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
17 breq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑥 𝐵 𝑦 ↔ 𝑥 𝐵 𝑤 ) )
18 breq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 𝐴 𝑧 ↔ 𝑤 𝐴 𝑧 ) )
19 17 18 anbi12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ↔ ( 𝑥 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) ) )
20 19 excomimw ⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → ∃ 𝑧 ∃ 𝑦 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) )
21 16 20 syl6 ⊢ ( ran 𝐵 ⊆ dom 𝐴 → ( ∃ 𝑦 𝑥 𝐵 𝑦 → ∃ 𝑧 ∃ 𝑦 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
22 vex ⊢ 𝑥 ∈ V
23 vex ⊢ 𝑧 ∈ V
24 22 23 opelco ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑦 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) )
25 24 exbii ⊢ ( ∃ 𝑧 ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑧 ∃ 𝑦 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) )
26 21 25 imbitrrdi ⊢ ( ran 𝐵 ⊆ dom 𝐴 → ( ∃ 𝑦 𝑥 𝐵 𝑦 → ∃ 𝑧 ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) ) )
27 22 eldm ⊢ ( 𝑥 ∈ dom 𝐵 ↔ ∃ 𝑦 𝑥 𝐵 𝑦 )
28 22 eldm2 ⊢ ( 𝑥 ∈ dom ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑧 ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) )
29 26 27 28 3imtr4g ⊢ ( ran 𝐵 ⊆ dom 𝐴 → ( 𝑥 ∈ dom 𝐵 → 𝑥 ∈ dom ( 𝐴 ∘ 𝐵 ) ) )
30 29 ssrdv ⊢ ( ran 𝐵 ⊆ dom 𝐴 → dom 𝐵 ⊆ dom ( 𝐴 ∘ 𝐵 ) )
31 2 30 eqssd ⊢ ( ran 𝐵 ⊆ dom 𝐴 → dom ( 𝐴 ∘ 𝐵 ) = dom 𝐵 )