Metamath Proof Explorer

Theorem cocanss2

Description: Cancellation law for composition. Suggested by BJ. (Contributed by Eric Schmidt, 30-Sep-2026)

Ref Expression
Hypotheses cocan2g.1 
|- ( ph -> Fun F )
cocan2g.2 
|- ( ph -> Rel H )
cocan2g.3 
|- ( ph -> dom H C_ ran F )
Assertion cocanss2 
|- ( ph -> ( ( H o. F ) C_ ( K o. F ) <-> H C_ K ) )

Proof

Step Hyp Ref Expression
1 cocan2g.1 
 |-  ( ph -> Fun F )
2 cocan2g.2 
 |-  ( ph -> Rel H )
3 cocan2g.3 
 |-  ( ph -> dom H C_ ran F )
4 2 adantr 
 |-  ( ( ph /\ ( H o. F ) C_ ( K o. F ) ) -> Rel H )
5 vex 
 |-  y e. _V
6 vex 
 |-  z e. _V
7 5 6 breldm 
 |-  ( y H z -> y e. dom H )
8 3 sseld 
 |-  ( ph -> ( y e. dom H -> y e. ran F ) )
9 7 8 syl5 
 |-  ( ph -> ( y H z -> y e. ran F ) )
10 5 elrn 
 |-  ( y e. ran F <-> E. x x F y )
11 9 10 imbitrdi 
 |-  ( ph -> ( y H z -> E. x x F y ) )
12 11 adantr 
 |-  ( ( ph /\ ( H o. F ) C_ ( K o. F ) ) -> ( y H z -> E. x x F y ) )
13 19.8a 
 |-  ( ( x F y /\ y H z ) -> E. y ( x F y /\ y H z ) )
14 vex 
 |-  x e. _V
15 14 6 brco 
 |-  ( x ( H o. F ) z <-> E. y ( x F y /\ y H z ) )
16 13 15 sylibr 
 |-  ( ( x F y /\ y H z ) -> x ( H o. F ) z )
17 ssbr 
 |-  ( ( H o. F ) C_ ( K o. F ) -> ( x ( H o. F ) z -> x ( K o. F ) z ) )
18 16 17 syl5 
 |-  ( ( H o. F ) C_ ( K o. F ) -> ( ( x F y /\ y H z ) -> x ( K o. F ) z ) )
19 14 6 brco 
 |-  ( x ( K o. F ) z <-> E. w ( x F w /\ w K z ) )
20 18 19 imbitrdi 
 |-  ( ( H o. F ) C_ ( K o. F ) -> ( ( x F y /\ y H z ) -> E. w ( x F w /\ w K z ) ) )
21 20 adantl 
 |-  ( ( ph /\ ( H o. F ) C_ ( K o. F ) ) -> ( ( x F y /\ y H z ) -> E. w ( x F w /\ w K z ) ) )
22 vex 
 |-  w e. _V
23 14 5 22 fununiq 
 |-  ( Fun F -> ( ( x F y /\ x F w ) -> y = w ) )
24 23 imp 
 |-  ( ( Fun F /\ ( x F y /\ x F w ) ) -> y = w )
25 24 breq1d 
 |-  ( ( Fun F /\ ( x F y /\ x F w ) ) -> ( y K z <-> w K z ) )
26 25 biimprd 
 |-  ( ( Fun F /\ ( x F y /\ x F w ) ) -> ( w K z -> y K z ) )
27 26 expr 
 |-  ( ( Fun F /\ x F y ) -> ( x F w -> ( w K z -> y K z ) ) )
28 27 impd 
 |-  ( ( Fun F /\ x F y ) -> ( ( x F w /\ w K z ) -> y K z ) )
29 28 exlimdv 
 |-  ( ( Fun F /\ x F y ) -> ( E. w ( x F w /\ w K z ) -> y K z ) )
30 1 29 sylan 
 |-  ( ( ph /\ x F y ) -> ( E. w ( x F w /\ w K z ) -> y K z ) )
31 30 ex 
 |-  ( ph -> ( x F y -> ( E. w ( x F w /\ w K z ) -> y K z ) ) )
32 31 adantr 
 |-  ( ( ph /\ ( H o. F ) C_ ( K o. F ) ) -> ( x F y -> ( E. w ( x F w /\ w K z ) -> y K z ) ) )
33 32 adantrd 
 |-  ( ( ph /\ ( H o. F ) C_ ( K o. F ) ) -> ( ( x F y /\ y H z ) -> ( E. w ( x F w /\ w K z ) -> y K z ) ) )
34 21 33 mpdd 
 |-  ( ( ph /\ ( H o. F ) C_ ( K o. F ) ) -> ( ( x F y /\ y H z ) -> y K z ) )
35 34 expd 
 |-  ( ( ph /\ ( H o. F ) C_ ( K o. F ) ) -> ( x F y -> ( y H z -> y K z ) ) )
36 35 exlimdv 
 |-  ( ( ph /\ ( H o. F ) C_ ( K o. F ) ) -> ( E. x x F y -> ( y H z -> y K z ) ) )
37 36 com23 
 |-  ( ( ph /\ ( H o. F ) C_ ( K o. F ) ) -> ( y H z -> ( E. x x F y -> y K z ) ) )
38 12 37 mpdd 
 |-  ( ( ph /\ ( H o. F ) C_ ( K o. F ) ) -> ( y H z -> y K z ) )
39 df-br 
 |-  ( y H z <-> <. y , z >. e. H )
40 df-br 
 |-  ( y K z <-> <. y , z >. e. K )
41 38 39 40 3imtr3g 
 |-  ( ( ph /\ ( H o. F ) C_ ( K o. F ) ) -> ( <. y , z >. e. H -> <. y , z >. e. K ) )
42 4 41 relssdv 
 |-  ( ( ph /\ ( H o. F ) C_ ( K o. F ) ) -> H C_ K )
43 42 ex 
 |-  ( ph -> ( ( H o. F ) C_ ( K o. F ) -> H C_ K ) )
44 coss1 
 |-  ( H C_ K -> ( H o. F ) C_ ( K o. F ) )
45 43 44 impbid1 
 |-  ( ph -> ( ( H o. F ) C_ ( K o. F ) <-> H C_ K ) )