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 H G H dom F dom G dom G dom F F G F = G G F

Proof

Step Hyp Ref Expression
1 funssres Fun H F H H dom F = F
2 1 ex Fun H F H H dom F = F
3 funssres Fun H G H H dom G = G
4 3 ex Fun H G H H dom G = G
5 2 4 anim12d Fun H F H G H H dom F = F H dom G = G
6 ssres2 dom F dom G H dom F H dom G
7 ssres2 dom G dom F H dom G H dom F
8 6 7 orim12i dom F dom G dom G dom F H dom F H dom G H dom G H dom F
9 sseq12 H dom F = F H dom G = G H dom F H dom G F G
10 sseq12 H dom G = G H dom F = F H dom G H dom F G F
11 10 ancoms H dom F = F H dom G = G H dom G H dom F G F
12 9 11 orbi12d H dom F = F H dom G = G H dom F H dom G H dom G H dom F F G G F
13 8 12 syl5ib H dom F = F H dom G = G dom F dom G dom G dom F F G G F
14 5 13 syl6 Fun H F H G H dom F dom G dom G dom F F G G F
15 14 3imp Fun H F H G H dom F dom G dom G dom F F G G F
16 sspsstri F G G F F G F = G G F
17 15 16 sylib Fun H F H G H dom F dom G dom G dom F F G F = G G F