Metamath Proof Explorer

Theorem coinitsslt

Description: If B is coinitial with C and A precedes C , then A precedes B . (Contributed by Scott Fenton, 24-Sep-2024)

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

Proof

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