Metamath Proof Explorer

Theorem cofon1

Description: Cofinality theorem for ordinals. If A is cofinal with B and the upper bound of A dominates B , then their upper bounds are equal. Compare with cofcut1 for surreals. (Contributed by Scott Fenton, 20-Jan-2025)

Ref Expression
Hypotheses cofon1.1 
|- ( ph -> A e. ~P On )
cofon1.2 
|- ( ph -> A. x e. A E. y e. B x C_ y )
cofon1.3 
|- ( ph -> B C_ |^| { z e. On | A C_ z } )
Assertion cofon1 
|- ( ph -> |^| { z e. On | A C_ z } = |^| { w e. On | B C_ w } )

Proof

Step Hyp Ref Expression
1 cofon1.1 
 |-  ( ph -> A e. ~P On )
2 cofon1.2 
 |-  ( ph -> A. x e. A E. y e. B x C_ y )
3 cofon1.3 
 |-  ( ph -> B C_ |^| { z e. On | A C_ z } )
4 sseq2 
 |-  ( w = z -> ( B C_ w <-> B C_ z ) )
5 4 cbvrabv 
 |-  { w e. On | B C_ w } = { z e. On | B C_ z }
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 2 ad2antrr 
 |-  ( ( ( ph /\ z e. On ) /\ ( B C_ z /\ a e. A ) ) -> A. x e. A E. y e. B x C_ y )
9 simprr 
 |-  ( ( ( ph /\ z e. On ) /\ ( B C_ z /\ a e. A ) ) -> a e. A )
10 7 8 9 rspcdva 
 |-  ( ( ( ph /\ z e. On ) /\ ( B C_ z /\ a e. A ) ) -> E. y e. B a C_ y )
11 sseq2 
 |-  ( y = b -> ( a C_ y <-> a C_ b ) )
12 11 cbvrexvw 
 |-  ( E. y e. B a C_ y <-> E. b e. B a C_ b )
13 10 12 sylib 
 |-  ( ( ( ph /\ z e. On ) /\ ( B C_ z /\ a e. A ) ) -> E. b e. B a C_ b )
14 simprl 
 |-  ( ( ( ph /\ z e. On ) /\ ( B C_ z /\ a e. A ) ) -> B C_ z )
15 14 sselda 
 |-  ( ( ( ( ph /\ z e. On ) /\ ( B C_ z /\ a e. A ) ) /\ b e. B ) -> b e. z )
16 1 elpwid 
 |-  ( ph -> A C_ On )
17 16 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. On ) /\ ( B C_ z /\ a e. A ) ) /\ b e. B ) -> A C_ On )
18 simplrr 
 |-  ( ( ( ( ph /\ z e. On ) /\ ( B C_ z /\ a e. A ) ) /\ b e. B ) -> a e. A )
19 17 18 sseldd 
 |-  ( ( ( ( ph /\ z e. On ) /\ ( B C_ z /\ a e. A ) ) /\ b e. B ) -> a e. On )
20 simpllr 
 |-  ( ( ( ( ph /\ z e. On ) /\ ( B C_ z /\ a e. A ) ) /\ b e. B ) -> z e. On )
21 ontr2 
 |-  ( ( a e. On /\ z e. On ) -> ( ( a C_ b /\ b e. z ) -> a e. z ) )
22 19 20 21 syl2anc 
 |-  ( ( ( ( ph /\ z e. On ) /\ ( B C_ z /\ a e. A ) ) /\ b e. B ) -> ( ( a C_ b /\ b e. z ) -> a e. z ) )
23 15 22 mpan2d 
 |-  ( ( ( ( ph /\ z e. On ) /\ ( B C_ z /\ a e. A ) ) /\ b e. B ) -> ( a C_ b -> a e. z ) )
24 23 rexlimdva 
 |-  ( ( ( ph /\ z e. On ) /\ ( B C_ z /\ a e. A ) ) -> ( E. b e. B a C_ b -> a e. z ) )
25 13 24 mpd 
 |-  ( ( ( ph /\ z e. On ) /\ ( B C_ z /\ a e. A ) ) -> a e. z )
26 25 expr 
 |-  ( ( ( ph /\ z e. On ) /\ B C_ z ) -> ( a e. A -> a e. z ) )
27 26 ssrdv 
 |-  ( ( ( ph /\ z e. On ) /\ B C_ z ) -> A C_ z )
28 27 ex 
 |-  ( ( ph /\ z e. On ) -> ( B C_ z -> A C_ z ) )
29 28 ss2rabdv 
 |-  ( ph -> { z e. On | B C_ z } C_ { z e. On | A C_ z } )
30 5 29 eqsstrid 
 |-  ( ph -> { w e. On | B C_ w } C_ { z e. On | A C_ z } )
31 intss 
 |-  ( { w e. On | B C_ w } C_ { z e. On | A C_ z } -> |^| { z e. On | A C_ z } C_ |^| { w e. On | B C_ w } )
32 30 31 syl 
 |-  ( ph -> |^| { z e. On | A C_ z } C_ |^| { w e. On | B C_ w } )
33 sseq2 
 |-  ( w = |^| { z e. On | A C_ z } -> ( B C_ w <-> B C_ |^| { z e. On | A C_ z } ) )
34 ssorduni 
 |-  ( A C_ On -> Ord U. A )
35 16 34 syl 
 |-  ( ph -> Ord U. A )
36 ordsuc 
 |-  ( Ord U. A <-> Ord suc U. A )
37 35 36 sylib 
 |-  ( ph -> Ord suc U. A )
38 1 uniexd 
 |-  ( ph -> U. A e. _V )
39 sucexg 
 |-  ( U. A e. _V -> suc U. A e. _V )
40 38 39 syl 
 |-  ( ph -> suc U. A e. _V )
41 elong 
 |-  ( suc U. A e. _V -> ( suc U. A e. On <-> Ord suc U. A ) )
42 40 41 syl 
 |-  ( ph -> ( suc U. A e. On <-> Ord suc U. A ) )
43 37 42 mpbird 
 |-  ( ph -> suc U. A e. On )
44 onsucuni 
 |-  ( A C_ On -> A C_ suc U. A )
45 16 44 syl 
 |-  ( ph -> A C_ suc U. A )
46 sseq2 
 |-  ( z = suc U. A -> ( A C_ z <-> A C_ suc U. A ) )
47 46 rspcev 
 |-  ( ( suc U. A e. On /\ A C_ suc U. A ) -> E. z e. On A C_ z )
48 43 45 47 syl2anc 
 |-  ( ph -> E. z e. On A C_ z )
49 onintrab2 
 |-  ( E. z e. On A C_ z <-> |^| { z e. On | A C_ z } e. On )
50 48 49 sylib 
 |-  ( ph -> |^| { z e. On | A C_ z } e. On )
51 33 50 3 elrabd 
 |-  ( ph -> |^| { z e. On | A C_ z } e. { w e. On | B C_ w } )
52 intss1 
 |-  ( |^| { z e. On | A C_ z } e. { w e. On | B C_ w } -> |^| { w e. On | B C_ w } C_ |^| { z e. On | A C_ z } )
53 51 52 syl 
 |-  ( ph -> |^| { w e. On | B C_ w } C_ |^| { z e. On | A C_ z } )
54 32 53 eqssd 
 |-  ( ph -> |^| { z e. On | A C_ z } = |^| { w e. On | B C_ w } )