Metamath Proof Explorer

Theorem coflton

Description: Cofinality theorem for ordinals. If A is cofinal with B and B precedes C , then A precedes C . Compare cofsslt for surreals. (Contributed by Scott Fenton, 20-Jan-2025)

Ref Expression
Hypotheses coflton.1 
|- ( ph -> A C_ On )
coflton.2 
|- ( ph -> B C_ On )
coflton.3 
|- ( ph -> C C_ On )
coflton.4 
|- ( ph -> A. x e. A E. y e. B x C_ y )
coflton.5 
|- ( ph -> A. z e. B A. w e. C z e. w )
Assertion coflton 
|- ( ph -> A. a e. A A. c e. C a e. c )

Proof

Step Hyp Ref Expression
1 coflton.1 
 |-  ( ph -> A C_ On )
2 coflton.2 
 |-  ( ph -> B C_ On )
3 coflton.3 
 |-  ( ph -> C C_ On )
4 coflton.4 
 |-  ( ph -> A. x e. A E. y e. B x C_ y )
5 coflton.5 
 |-  ( ph -> A. z e. B A. w e. C z e. w )
6 sseq1 
 |-  ( x = a -> ( x C_ y <-> a C_ y ) )
7 6 rexbidv 
 |-  ( x = a -> ( E. y e. B x C_ y <-> E. y e. B a C_ y ) )
8 4 adantr 
 |-  ( ( ph /\ a e. A ) -> A. x e. A E. y e. B x C_ y )
9 simpr 
 |-  ( ( ph /\ a e. A ) -> a e. A )
10 7 8 9 rspcdva 
 |-  ( ( ph /\ a e. A ) -> E. y e. B a C_ y )
11 10 adantrr 
 |-  ( ( ph /\ ( a e. A /\ c e. C ) ) -> E. y e. B a C_ y )
12 sseq2 
 |-  ( y = b -> ( a C_ y <-> a C_ b ) )
13 12 cbvrexvw 
 |-  ( E. y e. B a C_ y <-> E. b e. B a C_ b )
14 11 13 sylib 
 |-  ( ( ph /\ ( a e. A /\ c e. C ) ) -> E. b e. B a C_ b )
15 simpr 
 |-  ( ( ( ph /\ ( a e. A /\ c e. C ) ) /\ b e. B ) -> b e. B )
16 simplrr 
 |-  ( ( ( ph /\ ( a e. A /\ c e. C ) ) /\ b e. B ) -> c e. C )
17 5 ad2antrr 
 |-  ( ( ( ph /\ ( a e. A /\ c e. C ) ) /\ b e. B ) -> A. z e. B A. w e. C z e. w )
18 elequ1 
 |-  ( z = b -> ( z e. w <-> b e. w ) )
19 elequ2 
 |-  ( w = c -> ( b e. w <-> b e. c ) )
20 18 19 rspc2va 
 |-  ( ( ( b e. B /\ c e. C ) /\ A. z e. B A. w e. C z e. w ) -> b e. c )
21 15 16 17 20 syl21anc 
 |-  ( ( ( ph /\ ( a e. A /\ c e. C ) ) /\ b e. B ) -> b e. c )
22 1 sselda 
 |-  ( ( ph /\ a e. A ) -> a e. On )
23 22 adantrr 
 |-  ( ( ph /\ ( a e. A /\ c e. C ) ) -> a e. On )
24 3 sselda 
 |-  ( ( ph /\ c e. C ) -> c e. On )
25 24 adantrl 
 |-  ( ( ph /\ ( a e. A /\ c e. C ) ) -> c e. On )
26 25 adantr 
 |-  ( ( ( ph /\ ( a e. A /\ c e. C ) ) /\ b e. B ) -> c e. On )
27 ontr2 
 |-  ( ( a e. On /\ c e. On ) -> ( ( a C_ b /\ b e. c ) -> a e. c ) )
28 23 26 27 syl2an2r 
 |-  ( ( ( ph /\ ( a e. A /\ c e. C ) ) /\ b e. B ) -> ( ( a C_ b /\ b e. c ) -> a e. c ) )
29 21 28 mpan2d 
 |-  ( ( ( ph /\ ( a e. A /\ c e. C ) ) /\ b e. B ) -> ( a C_ b -> a e. c ) )
30 29 rexlimdva 
 |-  ( ( ph /\ ( a e. A /\ c e. C ) ) -> ( E. b e. B a C_ b -> a e. c ) )
31 14 30 mpd 
 |-  ( ( ph /\ ( a e. A /\ c e. C ) ) -> a e. c )
32 31 ralrimivva 
 |-  ( ph -> A. a e. A A. c e. C a e. c )