Metamath Proof Explorer


Theorem funpsstri

Description: A condition for subset trichotomy for functions. (Contributed by Scott Fenton, 19-Apr-2011)

Ref Expression
Assertion funpsstri
|- ( ( Fun H /\ ( F C_ H /\ G C_ H ) /\ ( dom F C_ dom G \/ dom G C_ dom F ) ) -> ( F C. G \/ F = G \/ G C. F ) )

Proof

Step Hyp Ref Expression
1 funssres
 |-  ( ( Fun H /\ F C_ H ) -> ( H |` dom F ) = F )
2 1 ex
 |-  ( Fun H -> ( F C_ H -> ( H |` dom F ) = F ) )
3 funssres
 |-  ( ( Fun H /\ G C_ H ) -> ( H |` dom G ) = G )
4 3 ex
 |-  ( Fun H -> ( G C_ H -> ( H |` dom G ) = G ) )
5 2 4 anim12d
 |-  ( Fun H -> ( ( F C_ H /\ G C_ H ) -> ( ( H |` dom F ) = F /\ ( H |` dom G ) = G ) ) )
6 ssres2
 |-  ( dom F C_ dom G -> ( H |` dom F ) C_ ( H |` dom G ) )
7 ssres2
 |-  ( dom G C_ dom F -> ( H |` dom G ) C_ ( H |` dom F ) )
8 6 7 orim12i
 |-  ( ( dom F C_ dom G \/ dom G C_ dom F ) -> ( ( H |` dom F ) C_ ( H |` dom G ) \/ ( H |` dom G ) C_ ( H |` dom F ) ) )
9 sseq12
 |-  ( ( ( H |` dom F ) = F /\ ( H |` dom G ) = G ) -> ( ( H |` dom F ) C_ ( H |` dom G ) <-> F C_ G ) )
10 sseq12
 |-  ( ( ( H |` dom G ) = G /\ ( H |` dom F ) = F ) -> ( ( H |` dom G ) C_ ( H |` dom F ) <-> G C_ F ) )
11 10 ancoms
 |-  ( ( ( H |` dom F ) = F /\ ( H |` dom G ) = G ) -> ( ( H |` dom G ) C_ ( H |` dom F ) <-> G C_ F ) )
12 9 11 orbi12d
 |-  ( ( ( H |` dom F ) = F /\ ( H |` dom G ) = G ) -> ( ( ( H |` dom F ) C_ ( H |` dom G ) \/ ( H |` dom G ) C_ ( H |` dom F ) ) <-> ( F C_ G \/ G C_ F ) ) )
13 8 12 syl5ib
 |-  ( ( ( H |` dom F ) = F /\ ( H |` dom G ) = G ) -> ( ( dom F C_ dom G \/ dom G C_ dom F ) -> ( F C_ G \/ G C_ F ) ) )
14 5 13 syl6
 |-  ( Fun H -> ( ( F C_ H /\ G C_ H ) -> ( ( dom F C_ dom G \/ dom G C_ dom F ) -> ( F C_ G \/ G C_ F ) ) ) )
15 14 3imp
 |-  ( ( Fun H /\ ( F C_ H /\ G C_ H ) /\ ( dom F C_ dom G \/ dom G C_ dom F ) ) -> ( F C_ G \/ G C_ F ) )
16 sspsstri
 |-  ( ( F C_ G \/ G C_ F ) <-> ( F C. G \/ F = G \/ G C. F ) )
17 15 16 sylib
 |-  ( ( Fun H /\ ( F C_ H /\ G C_ H ) /\ ( dom F C_ dom G \/ dom G C_ dom F ) ) -> ( F C. G \/ F = G \/ G C. F ) )