Metamath Proof Explorer


Theorem conrel1d

Description: Deduction about composition with a class with no relational content. (Contributed by RP, 24-Dec-2019)

Ref Expression
Hypothesis conrel1d.a φ A -1 =
Assertion conrel1d φ A B =

Proof

Step Hyp Ref Expression
1 conrel1d.a φ A -1 =
2 incom dom A ran B = ran B dom A
3 dfdm4 dom A = ran A -1
4 1 rneqd φ ran A -1 = ran
5 rn0 ran =
6 4 5 eqtrdi φ ran A -1 =
7 3 6 syl5eq φ dom A =
8 ineq2 dom A = ran B dom A = ran B
9 in0 ran B =
10 8 9 eqtrdi dom A = ran B dom A =
11 7 10 syl φ ran B dom A =
12 2 11 syl5eq φ dom A ran B =
13 12 coemptyd φ A B =