Theorem prsss

Description: Relation of a subproset. (Contributed by Thierry Arnoux, 13-Sep-2018)

	Ref	Expression
Hypotheses	ordtNEW.b	|- B = ( Base ` K )
	ordtNEW.l	|- .<_ = ( ( le ` K ) i^i ( B X. B ) )
Assertion	prsss	|- ( ( K e. Proset /\ A C_ B ) -> ( .<_ i^i ( A X. A ) ) = ( ( le ` K ) i^i ( A X. A ) ) )

Proof

Step	Hyp	Ref	Expression
1		ordtNEW.b	|- B = ( Base ` K )
2		ordtNEW.l	|- .<_ = ( ( le ` K ) i^i ( B X. B ) )
3	2	ineq1i	|- ( .<_ i^i ( A X. A ) ) = ( ( ( le ` K ) i^i ( B X. B ) ) i^i ( A X. A ) )
4		inass	|- ( ( ( le ` K ) i^i ( B X. B ) ) i^i ( A X. A ) ) = ( ( le ` K ) i^i ( ( B X. B ) i^i ( A X. A ) ) )
5	3 4	eqtri	|- ( .<_ i^i ( A X. A ) ) = ( ( le ` K ) i^i ( ( B X. B ) i^i ( A X. A ) ) )
6		xpss12	|- ( ( A C_ B /\ A C_ B ) -> ( A X. A ) C_ ( B X. B ) )
7	6	anidms	|- ( A C_ B -> ( A X. A ) C_ ( B X. B ) )
8		sseqin2	|- ( ( A X. A ) C_ ( B X. B ) <-> ( ( B X. B ) i^i ( A X. A ) ) = ( A X. A ) )
9	7 8	sylib	|- ( A C_ B -> ( ( B X. B ) i^i ( A X. A ) ) = ( A X. A ) )
10	9	ineq2d	|- ( A C_ B -> ( ( le ` K ) i^i ( ( B X. B ) i^i ( A X. A ) ) ) = ( ( le ` K ) i^i ( A X. A ) ) )
11	5 10	syl5eq	|- ( A C_ B -> ( .<_ i^i ( A X. A ) ) = ( ( le ` K ) i^i ( A X. A ) ) )
12	11	adantl	|- ( ( K e. Proset /\ A C_ B ) -> ( .<_ i^i ( A X. A ) ) = ( ( le ` K ) i^i ( A X. A ) ) )