Metamath Proof Explorer

Theorem dmcosseqOLD

Description: Obsolete version of dmcosseq as of 31-Dec-2025. (Contributed by NM, 28-May-1998) (Proof shortened by Andrew Salmon, 27-Aug-2011) Avoid ax-11 . (Revised by BTernaryTau, 23-Jun-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dmcosseqOLD ( 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 19.8a ⊢ ( 𝑥 𝐵 𝑦 → ∃ 𝑥 𝑥 𝐵 𝑦 )
9 8 imim1i ⊢ ( ( ∃ 𝑥 𝑥 𝐵 𝑦 → ∃ 𝑧 𝑦 𝐴 𝑧 ) → ( 𝑥 𝐵 𝑦 → ∃ 𝑧 𝑦 𝐴 𝑧 ) )
10 pm3.2 ⊢ ( 𝑥 𝐵 𝑦 → ( 𝑦 𝐴 𝑧 → ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
11 10 eximdv ⊢ ( 𝑥 𝐵 𝑦 → ( ∃ 𝑧 𝑦 𝐴 𝑧 → ∃ 𝑧 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
12 9 11 sylcom ⊢ ( ( ∃ 𝑥 𝑥 𝐵 𝑦 → ∃ 𝑧 𝑦 𝐴 𝑧 ) → ( 𝑥 𝐵 𝑦 → ∃ 𝑧 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
13 7 12 sylbi ⊢ ( ( 𝑦 ∈ ran 𝐵 → 𝑦 ∈ dom 𝐴 ) → ( 𝑥 𝐵 𝑦 → ∃ 𝑧 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
14 3 13 syl ⊢ ( ran 𝐵 ⊆ dom 𝐴 → ( 𝑥 𝐵 𝑦 → ∃ 𝑧 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
15 14 eximdv ⊢ ( ran 𝐵 ⊆ dom 𝐴 → ( ∃ 𝑦 𝑥 𝐵 𝑦 → ∃ 𝑦 ∃ 𝑧 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
16 breq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑥 𝐵 𝑦 ↔ 𝑥 𝐵 𝑤 ) )
17 breq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 𝐴 𝑧 ↔ 𝑤 𝐴 𝑧 ) )
18 16 17 anbi12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ↔ ( 𝑥 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) ) )
19 18 excomimw ⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → ∃ 𝑧 ∃ 𝑦 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) )
20 15 19 syl6 ⊢ ( ran 𝐵 ⊆ dom 𝐴 → ( ∃ 𝑦 𝑥 𝐵 𝑦 → ∃ 𝑧 ∃ 𝑦 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ) )
21 vex ⊢ 𝑥 ∈ V
22 vex ⊢ 𝑧 ∈ V
23 21 22 opelco ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑦 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) )
24 23 exbii ⊢ ( ∃ 𝑧 ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑧 ∃ 𝑦 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) )
25 20 24 imbitrrdi ⊢ ( ran 𝐵 ⊆ dom 𝐴 → ( ∃ 𝑦 𝑥 𝐵 𝑦 → ∃ 𝑧 ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) ) )
26 21 eldm ⊢ ( 𝑥 ∈ dom 𝐵 ↔ ∃ 𝑦 𝑥 𝐵 𝑦 )
27 21 eldm2 ⊢ ( 𝑥 ∈ dom ( 𝐴 ∘ 𝐵 ) ↔ ∃ 𝑧 ⟨ 𝑥 , 𝑧 ⟩ ∈ ( 𝐴 ∘ 𝐵 ) )
28 25 26 27 3imtr4g ⊢ ( ran 𝐵 ⊆ dom 𝐴 → ( 𝑥 ∈ dom 𝐵 → 𝑥 ∈ dom ( 𝐴 ∘ 𝐵 ) ) )
29 28 ssrdv ⊢ ( ran 𝐵 ⊆ dom 𝐴 → dom 𝐵 ⊆ dom ( 𝐴 ∘ 𝐵 ) )
30 2 29 eqssd ⊢ ( ran 𝐵 ⊆ dom 𝐴 → dom ( 𝐴 ∘ 𝐵 ) = dom 𝐵 )