Theorem cofss

Description: Cofinality for a subset. (Contributed by Scott Fenton, 13-Mar-2025)

	Ref	Expression
Hypotheses	cofss.1	|- ( ph -> A C_ No )
	cofss.2	|- ( ph -> B C_ A )
Assertion	cofss	|- ( ph -> A. x e. B E. y e. A x <_s y )

Proof

Step	Hyp	Ref	Expression
1		cofss.1	|- ( ph -> A C_ No )
2		cofss.2	|- ( ph -> B C_ A )
3	2	sselda	|- ( ( ph /\ z e. B ) -> z e. A )
4	2 1	sstrd	|- ( ph -> B C_ No )
5	4	sselda	|- ( ( ph /\ z e. B ) -> z e. No )
6		slerflex	|- ( z e. No -> z <_s z )
7	5 6	syl	|- ( ( ph /\ z e. B ) -> z <_s z )
8		breq2	|- ( y = z -> ( z <_s y <-> z <_s z ) )
9	8	rspcev	|- ( ( z e. A /\ z <_s z ) -> E. y e. A z <_s y )
10	3 7 9	syl2anc	|- ( ( ph /\ z e. B ) -> E. y e. A z <_s y )
11	10	ralrimiva	|- ( ph -> A. z e. B E. y e. A z <_s y )
12		breq1	|- ( x = z -> ( x <_s y <-> z <_s y ) )
13	12	rexbidv	|- ( x = z -> ( E. y e. A x <_s y <-> E. y e. A z <_s y ) )
14	13	cbvralvw	|- ( A. x e. B E. y e. A x <_s y <-> A. z e. B E. y e. A z <_s y )
15	11 14	sylibr	|- ( ph -> A. x e. B E. y e. A x <_s y )