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 \land (F \subseteq H \land G \subseteq H) \land (dom F \subseteq dom G \lor dom G \subseteq dom F)) \to (F \subset G \lor F = G \lor G \subset F)$

Proof

Step	Hyp	Ref	Expression
1		funssres	$⊢ (Fun H \land F \subseteq H) \to {H ↾}_{dom F} = F$
2	1	ex	$⊢ Fun H \to (F \subseteq H \to {H ↾}_{dom F} = F)$
3		funssres	$⊢ (Fun H \land G \subseteq H) \to {H ↾}_{dom G} = G$
4	3	ex	$⊢ Fun H \to (G \subseteq H \to {H ↾}_{dom G} = G)$
5	2 4	anim12d	$⊢ Fun H \to ((F \subseteq H \land G \subseteq H) \to ({H ↾}_{dom F} = F \land {H ↾}_{dom G} = G))$
6		ssres2	$⊢ dom F \subseteq dom G \to {H ↾}_{dom F} \subseteq {H ↾}_{dom G}$
7		ssres2	$⊢ dom G \subseteq dom F \to {H ↾}_{dom G} \subseteq {H ↾}_{dom F}$
8	6 7	orim12i	$⊢ (dom F \subseteq dom G \lor dom G \subseteq dom F) \to ({H ↾}_{dom F} \subseteq {H ↾}_{dom G} \lor {H ↾}_{dom G} \subseteq {H ↾}_{dom F})$
9		sseq12	$⊢ ({H ↾}_{dom F} = F \land {H ↾}_{dom G} = G) \to ({H ↾}_{dom F} \subseteq {H ↾}_{dom G} \leftrightarrow F \subseteq G)$
10		sseq12	$⊢ ({H ↾}_{dom G} = G \land {H ↾}_{dom F} = F) \to ({H ↾}_{dom G} \subseteq {H ↾}_{dom F} \leftrightarrow G \subseteq F)$
11	10	ancoms	$⊢ ({H ↾}_{dom F} = F \land {H ↾}_{dom G} = G) \to ({H ↾}_{dom G} \subseteq {H ↾}_{dom F} \leftrightarrow G \subseteq F)$
12	9 11	orbi12d	$⊢ ({H ↾}_{dom F} = F \land {H ↾}_{dom G} = G) \to (({H ↾}_{dom F} \subseteq {H ↾}_{dom G} \lor {H ↾}_{dom G} \subseteq {H ↾}_{dom F}) \leftrightarrow (F \subseteq G \lor G \subseteq F))$
13	8 12	syl5ib	$⊢ ({H ↾}_{dom F} = F \land {H ↾}_{dom G} = G) \to ((dom F \subseteq dom G \lor dom G \subseteq dom F) \to (F \subseteq G \lor G \subseteq F))$
14	5 13	syl6	$⊢ Fun H \to ((F \subseteq H \land G \subseteq H) \to ((dom F \subseteq dom G \lor dom G \subseteq dom F) \to (F \subseteq G \lor G \subseteq F)))$
15	14	3imp	$⊢ (Fun H \land (F \subseteq H \land G \subseteq H) \land (dom F \subseteq dom G \lor dom G \subseteq dom F)) \to (F \subseteq G \lor G \subseteq F)$
16		sspsstri	$⊢ (F \subseteq G \lor G \subseteq F) \leftrightarrow (F \subset G \lor F = G \lor G \subset F)$
17	15 16	sylib	$⊢ (Fun H \land (F \subseteq H \land G \subseteq H) \land (dom F \subseteq dom G \lor dom G \subseteq dom F)) \to (F \subset G \lor F = G \lor G \subset F)$