Theorem funpsstri

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

	Ref	Expression
Assertion	funpsstri	⊢ ( ( Fun 𝐻 ∧ ( 𝐹 ⊆ 𝐻 ∧ 𝐺 ⊆ 𝐻 ) ∧ ( dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹 ) ) → ( 𝐹 ⊊ 𝐺 ∨ 𝐹 = 𝐺 ∨ 𝐺 ⊊ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		funssres	⊢ ( ( Fun 𝐻 ∧ 𝐹 ⊆ 𝐻 ) → ( 𝐻 ↾ dom 𝐹 ) = 𝐹 )
2	1	ex	⊢ ( Fun 𝐻 → ( 𝐹 ⊆ 𝐻 → ( 𝐻 ↾ dom 𝐹 ) = 𝐹 ) )
3		funssres	⊢ ( ( Fun 𝐻 ∧ 𝐺 ⊆ 𝐻 ) → ( 𝐻 ↾ dom 𝐺 ) = 𝐺 )
4	3	ex	⊢ ( Fun 𝐻 → ( 𝐺 ⊆ 𝐻 → ( 𝐻 ↾ dom 𝐺 ) = 𝐺 ) )
5	2 4	anim12d	⊢ ( Fun 𝐻 → ( ( 𝐹 ⊆ 𝐻 ∧ 𝐺 ⊆ 𝐻 ) → ( ( 𝐻 ↾ dom 𝐹 ) = 𝐹 ∧ ( 𝐻 ↾ dom 𝐺 ) = 𝐺 ) ) )
6		ssres2	⊢ ( dom 𝐹 ⊆ dom 𝐺 → ( 𝐻 ↾ dom 𝐹 ) ⊆ ( 𝐻 ↾ dom 𝐺 ) )
7		ssres2	⊢ ( dom 𝐺 ⊆ dom 𝐹 → ( 𝐻 ↾ dom 𝐺 ) ⊆ ( 𝐻 ↾ dom 𝐹 ) )
8	6 7	orim12i	⊢ ( ( dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹 ) → ( ( 𝐻 ↾ dom 𝐹 ) ⊆ ( 𝐻 ↾ dom 𝐺 ) ∨ ( 𝐻 ↾ dom 𝐺 ) ⊆ ( 𝐻 ↾ dom 𝐹 ) ) )
9		sseq12	⊢ ( ( ( 𝐻 ↾ dom 𝐹 ) = 𝐹 ∧ ( 𝐻 ↾ dom 𝐺 ) = 𝐺 ) → ( ( 𝐻 ↾ dom 𝐹 ) ⊆ ( 𝐻 ↾ dom 𝐺 ) ↔ 𝐹 ⊆ 𝐺 ) )
10		sseq12	⊢ ( ( ( 𝐻 ↾ dom 𝐺 ) = 𝐺 ∧ ( 𝐻 ↾ dom 𝐹 ) = 𝐹 ) → ( ( 𝐻 ↾ dom 𝐺 ) ⊆ ( 𝐻 ↾ dom 𝐹 ) ↔ 𝐺 ⊆ 𝐹 ) )
11	10	ancoms	⊢ ( ( ( 𝐻 ↾ dom 𝐹 ) = 𝐹 ∧ ( 𝐻 ↾ dom 𝐺 ) = 𝐺 ) → ( ( 𝐻 ↾ dom 𝐺 ) ⊆ ( 𝐻 ↾ dom 𝐹 ) ↔ 𝐺 ⊆ 𝐹 ) )
12	9 11	orbi12d	⊢ ( ( ( 𝐻 ↾ dom 𝐹 ) = 𝐹 ∧ ( 𝐻 ↾ dom 𝐺 ) = 𝐺 ) → ( ( ( 𝐻 ↾ dom 𝐹 ) ⊆ ( 𝐻 ↾ dom 𝐺 ) ∨ ( 𝐻 ↾ dom 𝐺 ) ⊆ ( 𝐻 ↾ dom 𝐹 ) ) ↔ ( 𝐹 ⊆ 𝐺 ∨ 𝐺 ⊆ 𝐹 ) ) )
13	8 12	imbitrid	⊢ ( ( ( 𝐻 ↾ dom 𝐹 ) = 𝐹 ∧ ( 𝐻 ↾ dom 𝐺 ) = 𝐺 ) → ( ( dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹 ) → ( 𝐹 ⊆ 𝐺 ∨ 𝐺 ⊆ 𝐹 ) ) )
14	5 13	syl6	⊢ ( Fun 𝐻 → ( ( 𝐹 ⊆ 𝐻 ∧ 𝐺 ⊆ 𝐻 ) → ( ( dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹 ) → ( 𝐹 ⊆ 𝐺 ∨ 𝐺 ⊆ 𝐹 ) ) ) )
15	14	3imp	⊢ ( ( Fun 𝐻 ∧ ( 𝐹 ⊆ 𝐻 ∧ 𝐺 ⊆ 𝐻 ) ∧ ( dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹 ) ) → ( 𝐹 ⊆ 𝐺 ∨ 𝐺 ⊆ 𝐹 ) )
16		sspsstri	⊢ ( ( 𝐹 ⊆ 𝐺 ∨ 𝐺 ⊆ 𝐹 ) ↔ ( 𝐹 ⊊ 𝐺 ∨ 𝐹 = 𝐺 ∨ 𝐺 ⊊ 𝐹 ) )
17	15 16	sylib	⊢ ( ( Fun 𝐻 ∧ ( 𝐹 ⊆ 𝐻 ∧ 𝐺 ⊆ 𝐻 ) ∧ ( dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹 ) ) → ( 𝐹 ⊊ 𝐺 ∨ 𝐹 = 𝐺 ∨ 𝐺 ⊊ 𝐹 ) )