Theorem carsgmon

Description: Utility lemma: Apply monotony. (Contributed by Thierry Arnoux, 29-May-2020)

	Ref	Expression
Hypotheses	carsgval.1	|- ( ph -> O e. V )
	carsgval.2	|- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
	carsgmon.1	|- ( ph -> A C_ B )
	carsgmon.2	|- ( ph -> B e. ~P O )
	carsgmon.3	|- ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
Assertion	carsgmon	|- ( ph -> ( M ` A ) <_ ( M ` B ) )

Proof

Step	Hyp	Ref	Expression
1		carsgval.1	|- ( ph -> O e. V )
2		carsgval.2	|- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
3		carsgmon.1	|- ( ph -> A C_ B )
4		carsgmon.2	|- ( ph -> B e. ~P O )
5		carsgmon.3	|- ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) )
6	4 3	ssexd	|- ( ph -> A e. _V )
7		id	|- ( ph -> ph )
8		sseq1	|- ( x = A -> ( x C_ y <-> A C_ y ) )
9	8	3anbi2d	|- ( x = A -> ( ( ph /\ x C_ y /\ y e. ~P O ) <-> ( ph /\ A C_ y /\ y e. ~P O ) ) )
10		fveq2	|- ( x = A -> ( M ` x ) = ( M ` A ) )
11	10	breq1d	|- ( x = A -> ( ( M ` x ) <_ ( M ` y ) <-> ( M ` A ) <_ ( M ` y ) ) )
12	9 11	imbi12d	|- ( x = A -> ( ( ( ph /\ x C_ y /\ y e. ~P O ) -> ( M ` x ) <_ ( M ` y ) ) <-> ( ( ph /\ A C_ y /\ y e. ~P O ) -> ( M ` A ) <_ ( M ` y ) ) ) )
13		sseq2	|- ( y = B -> ( A C_ y <-> A C_ B ) )
14		eleq1	|- ( y = B -> ( y e. ~P O <-> B e. ~P O ) )
15	13 14	3anbi23d	|- ( y = B -> ( ( ph /\ A C_ y /\ y e. ~P O ) <-> ( ph /\ A C_ B /\ B e. ~P O ) ) )
16		fveq2	|- ( y = B -> ( M ` y ) = ( M ` B ) )
17	16	breq2d	|- ( y = B -> ( ( M ` A ) <_ ( M ` y ) <-> ( M ` A ) <_ ( M ` B ) ) )
18	15 17	imbi12d	|- ( y = B -> ( ( ( ph /\ A C_ y /\ y e. ~P O ) -> ( M ` A ) <_ ( M ` y ) ) <-> ( ( ph /\ A C_ B /\ B e. ~P O ) -> ( M ` A ) <_ ( M ` B ) ) ) )
19	12 18 5	vtocl2g	|- ( ( A e. _V /\ B e. ~P O ) -> ( ( ph /\ A C_ B /\ B e. ~P O ) -> ( M ` A ) <_ ( M ` B ) ) )
20	19	imp	|- ( ( ( A e. _V /\ B e. ~P O ) /\ ( ph /\ A C_ B /\ B e. ~P O ) ) -> ( M ` A ) <_ ( M ` B ) )
21	6 4 7 3 4 20	syl23anc	|- ( ph -> ( M ` A ) <_ ( M ` B ) )