Metamath Proof Explorer

Theorem coeq0i

Description: coeq0 but without explicitly introducing domain and range symbols. (Contributed by Stefan O'Rear, 16-Oct-2014)

Ref Expression
Assertion coeq0i ( ( 𝐴 : 𝐶 ⟶ 𝐷 ∧ 𝐵 : 𝐸 ⟶ 𝐹 ∧ ( 𝐶 ∩ 𝐹 ) = ∅ ) → ( 𝐴 ∘ 𝐵 ) = ∅ )

Proof

Step Hyp Ref Expression
1 frn ⊢ ( 𝐵 : 𝐸 ⟶ 𝐹 → ran 𝐵 ⊆ 𝐹 )
2 1 3ad2ant2 ⊢ ( ( 𝐴 : 𝐶 ⟶ 𝐷 ∧ 𝐵 : 𝐸 ⟶ 𝐹 ∧ ( 𝐶 ∩ 𝐹 ) = ∅ ) → ran 𝐵 ⊆ 𝐹 )
3 sslin ⊢ ( ran 𝐵 ⊆ 𝐹 → ( dom 𝐴 ∩ ran 𝐵 ) ⊆ ( dom 𝐴 ∩ 𝐹 ) )
4 2 3 syl ⊢ ( ( 𝐴 : 𝐶 ⟶ 𝐷 ∧ 𝐵 : 𝐸 ⟶ 𝐹 ∧ ( 𝐶 ∩ 𝐹 ) = ∅ ) → ( dom 𝐴 ∩ ran 𝐵 ) ⊆ ( dom 𝐴 ∩ 𝐹 ) )
5 fdm ⊢ ( 𝐴 : 𝐶 ⟶ 𝐷 → dom 𝐴 = 𝐶 )
6 5 3ad2ant1 ⊢ ( ( 𝐴 : 𝐶 ⟶ 𝐷 ∧ 𝐵 : 𝐸 ⟶ 𝐹 ∧ ( 𝐶 ∩ 𝐹 ) = ∅ ) → dom 𝐴 = 𝐶 )
7 6 ineq1d ⊢ ( ( 𝐴 : 𝐶 ⟶ 𝐷 ∧ 𝐵 : 𝐸 ⟶ 𝐹 ∧ ( 𝐶 ∩ 𝐹 ) = ∅ ) → ( dom 𝐴 ∩ 𝐹 ) = ( 𝐶 ∩ 𝐹 ) )
8 simp3 ⊢ ( ( 𝐴 : 𝐶 ⟶ 𝐷 ∧ 𝐵 : 𝐸 ⟶ 𝐹 ∧ ( 𝐶 ∩ 𝐹 ) = ∅ ) → ( 𝐶 ∩ 𝐹 ) = ∅ )
9 7 8 eqtrd ⊢ ( ( 𝐴 : 𝐶 ⟶ 𝐷 ∧ 𝐵 : 𝐸 ⟶ 𝐹 ∧ ( 𝐶 ∩ 𝐹 ) = ∅ ) → ( dom 𝐴 ∩ 𝐹 ) = ∅ )
10 4 9 sseqtrd ⊢ ( ( 𝐴 : 𝐶 ⟶ 𝐷 ∧ 𝐵 : 𝐸 ⟶ 𝐹 ∧ ( 𝐶 ∩ 𝐹 ) = ∅ ) → ( dom 𝐴 ∩ ran 𝐵 ) ⊆ ∅ )
11 ss0 ⊢ ( ( dom 𝐴 ∩ ran 𝐵 ) ⊆ ∅ → ( dom 𝐴 ∩ ran 𝐵 ) = ∅ )
12 10 11 syl ⊢ ( ( 𝐴 : 𝐶 ⟶ 𝐷 ∧ 𝐵 : 𝐸 ⟶ 𝐹 ∧ ( 𝐶 ∩ 𝐹 ) = ∅ ) → ( dom 𝐴 ∩ ran 𝐵 ) = ∅ )
13 12 coemptyd ⊢ ( ( 𝐴 : 𝐶 ⟶ 𝐷 ∧ 𝐵 : 𝐸 ⟶ 𝐹 ∧ ( 𝐶 ∩ 𝐹 ) = ∅ ) → ( 𝐴 ∘ 𝐵 ) = ∅ )