Metamath Proof Explorer

Theorem cofsslt

Description: If every element of A is bounded by some element of B and B precedes C , then A precedes C . Note - we will often use the term "cofinal" to denote that every element of A is bounded above by some element of B . Similarly, we will use the term "coinitial" to denote that every element of A is bounded below by some element of B . (Contributed by Scott Fenton, 24-Sep-2024)

Ref Expression
Assertion cofsslt 
|- ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < A <

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < A e. ~P No )
2 ssltex2 
 |-  ( B < C e. _V )
3 2 3ad2ant3 
 |-  ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < C e. _V )
4 1 elpwid 
 |-  ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < A C_ No )
5 ssltss2 
 |-  ( B < C C_ No )
6 5 3ad2ant3 
 |-  ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < C C_ No )
7 breq1 
 |-  ( x = a -> ( x <_s y <-> a <_s y ) )
8 7 rexbidv 
 |-  ( x = a -> ( E. y e. B x <_s y <-> E. y e. B a <_s y ) )
9 simp12 
 |-  ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < A. x e. A E. y e. B x <_s y )
10 simp2 
 |-  ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < a e. A )
11 8 9 10 rspcdva 
 |-  ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < E. y e. B a <_s y )
12 breq2 
 |-  ( y = b -> ( a <_s y <-> a <_s b ) )
13 12 cbvrexvw 
 |-  ( E. y e. B a <_s y <-> E. b e. B a <_s b )
14 11 13 sylib 
 |-  ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < E. b e. B a <_s b )
15 simpl11 
 |-  ( ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < A e. ~P No )
16 15 elpwid 
 |-  ( ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < A C_ No )
17 simpl2 
 |-  ( ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < a e. A )
18 16 17 sseldd 
 |-  ( ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < a e. No )
19 simpl13 
 |-  ( ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < B <
20 ssltss1 
 |-  ( B < B C_ No )
21 19 20 syl 
 |-  ( ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < B C_ No )
22 simprl 
 |-  ( ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < b e. B )
23 21 22 sseldd 
 |-  ( ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < b e. No )
24 19 5 syl 
 |-  ( ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < C C_ No )
25 simpl3 
 |-  ( ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < c e. C )
26 24 25 sseldd 
 |-  ( ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < c e. No )
27 simprr 
 |-  ( ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < a <_s b )
28 19 22 25 ssltsepcd 
 |-  ( ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < b
29 18 23 26 27 28 slelttrd 
 |-  ( ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < a
30 14 29 rexlimddv 
 |-  ( ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < a
31 1 3 4 6 30 ssltd 
 |-  ( ( A e. ~P No /\ A. x e. A E. y e. B x <_s y /\ B < A <