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 
|- ( ( A : C --> D /\ B : E --> F /\ ( C i^i F ) = (/) ) -> ( A o. B ) = (/) )

Proof

Step Hyp Ref Expression
1 frn 
 |-  ( B : E --> F -> ran B C_ F )
2 1 3ad2ant2 
 |-  ( ( A : C --> D /\ B : E --> F /\ ( C i^i F ) = (/) ) -> ran B C_ F )
3 sslin 
 |-  ( ran B C_ F -> ( dom A i^i ran B ) C_ ( dom A i^i F ) )
4 2 3 syl 
 |-  ( ( A : C --> D /\ B : E --> F /\ ( C i^i F ) = (/) ) -> ( dom A i^i ran B ) C_ ( dom A i^i F ) )
5 fdm 
 |-  ( A : C --> D -> dom A = C )
6 5 3ad2ant1 
 |-  ( ( A : C --> D /\ B : E --> F /\ ( C i^i F ) = (/) ) -> dom A = C )
7 6 ineq1d 
 |-  ( ( A : C --> D /\ B : E --> F /\ ( C i^i F ) = (/) ) -> ( dom A i^i F ) = ( C i^i F ) )
8 simp3 
 |-  ( ( A : C --> D /\ B : E --> F /\ ( C i^i F ) = (/) ) -> ( C i^i F ) = (/) )
9 7 8 eqtrd 
 |-  ( ( A : C --> D /\ B : E --> F /\ ( C i^i F ) = (/) ) -> ( dom A i^i F ) = (/) )
10 4 9 sseqtrd 
 |-  ( ( A : C --> D /\ B : E --> F /\ ( C i^i F ) = (/) ) -> ( dom A i^i ran B ) C_ (/) )
11 ss0 
 |-  ( ( dom A i^i ran B ) C_ (/) -> ( dom A i^i ran B ) = (/) )
12 10 11 syl 
 |-  ( ( A : C --> D /\ B : E --> F /\ ( C i^i F ) = (/) ) -> ( dom A i^i ran B ) = (/) )
13 12 coemptyd 
 |-  ( ( A : C --> D /\ B : E --> F /\ ( C i^i F ) = (/) ) -> ( A o. B ) = (/) )