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	imbitrid	|- ( ( ( 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 ) )