Metamath Proof Explorer

Theorem cofon2

Description: Cofinality theorem for ordinals. If A and B are mutually cofinal, then their upper bounds agree. Compare cofcut2 for surreals. (Contributed by Scott Fenton, 20-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 cofon2.1 
 |-  ( ph -> A e. ~P On )
2 cofon2.2 
 |-  ( ph -> B e. ~P On )
3 cofon2.3 
 |-  ( ph -> A. x e. A E. y e. B x C_ y )
4 cofon2.4 
 |-  ( ph -> A. z e. B E. w e. A z C_ w )
5 sseq1 
 |-  ( z = b -> ( z C_ w <-> b C_ w ) )
6 5 rexbidv 
 |-  ( z = b -> ( E. w e. A z C_ w <-> E. w e. A b C_ w ) )
7 4 adantr 
 |-  ( ( ph /\ b e. B ) -> A. z e. B E. w e. A z C_ w )
8 simpr 
 |-  ( ( ph /\ b e. B ) -> b e. B )
9 6 7 8 rspcdva 
 |-  ( ( ph /\ b e. B ) -> E. w e. A b C_ w )
10 sseq2 
 |-  ( w = c -> ( b C_ w <-> b C_ c ) )
11 10 cbvrexvw 
 |-  ( E. w e. A b C_ w <-> E. c e. A b C_ c )
12 9 11 sylib 
 |-  ( ( ph /\ b e. B ) -> E. c e. A b C_ c )
13 ssintub 
 |-  A C_ |^| { a e. On | A C_ a }
14 13 a1i 
 |-  ( ( ph /\ b e. B ) -> A C_ |^| { a e. On | A C_ a } )
15 14 sselda 
 |-  ( ( ( ph /\ b e. B ) /\ c e. A ) -> c e. |^| { a e. On | A C_ a } )
16 2 elpwid 
 |-  ( ph -> B C_ On )
17 16 ad2antrr 
 |-  ( ( ( ph /\ b e. B ) /\ c e. A ) -> B C_ On )
18 simplr 
 |-  ( ( ( ph /\ b e. B ) /\ c e. A ) -> b e. B )
19 17 18 sseldd 
 |-  ( ( ( ph /\ b e. B ) /\ c e. A ) -> b e. On )
20 1 elpwid 
 |-  ( ph -> A C_ On )
21 ssorduni 
 |-  ( A C_ On -> Ord U. A )
22 20 21 syl 
 |-  ( ph -> Ord U. A )
23 ordsuc 
 |-  ( Ord U. A <-> Ord suc U. A )
24 22 23 sylib 
 |-  ( ph -> Ord suc U. A )
25 1 uniexd 
 |-  ( ph -> U. A e. _V )
26 sucexg 
 |-  ( U. A e. _V -> suc U. A e. _V )
27 elong 
 |-  ( suc U. A e. _V -> ( suc U. A e. On <-> Ord suc U. A ) )
28 25 26 27 3syl 
 |-  ( ph -> ( suc U. A e. On <-> Ord suc U. A ) )
29 24 28 mpbird 
 |-  ( ph -> suc U. A e. On )
30 onsucuni 
 |-  ( A C_ On -> A C_ suc U. A )
31 20 30 syl 
 |-  ( ph -> A C_ suc U. A )
32 sseq2 
 |-  ( a = suc U. A -> ( A C_ a <-> A C_ suc U. A ) )
33 32 rspcev 
 |-  ( ( suc U. A e. On /\ A C_ suc U. A ) -> E. a e. On A C_ a )
34 29 31 33 syl2anc 
 |-  ( ph -> E. a e. On A C_ a )
35 onintrab2 
 |-  ( E. a e. On A C_ a <-> |^| { a e. On | A C_ a } e. On )
36 34 35 sylib 
 |-  ( ph -> |^| { a e. On | A C_ a } e. On )
37 36 ad2antrr 
 |-  ( ( ( ph /\ b e. B ) /\ c e. A ) -> |^| { a e. On | A C_ a } e. On )
38 ontr2 
 |-  ( ( b e. On /\ |^| { a e. On | A C_ a } e. On ) -> ( ( b C_ c /\ c e. |^| { a e. On | A C_ a } ) -> b e. |^| { a e. On | A C_ a } ) )
39 19 37 38 syl2anc 
 |-  ( ( ( ph /\ b e. B ) /\ c e. A ) -> ( ( b C_ c /\ c e. |^| { a e. On | A C_ a } ) -> b e. |^| { a e. On | A C_ a } ) )
40 15 39 mpan2d 
 |-  ( ( ( ph /\ b e. B ) /\ c e. A ) -> ( b C_ c -> b e. |^| { a e. On | A C_ a } ) )
41 40 rexlimdva 
 |-  ( ( ph /\ b e. B ) -> ( E. c e. A b C_ c -> b e. |^| { a e. On | A C_ a } ) )
42 12 41 mpd 
 |-  ( ( ph /\ b e. B ) -> b e. |^| { a e. On | A C_ a } )
43 42 ex 
 |-  ( ph -> ( b e. B -> b e. |^| { a e. On | A C_ a } ) )
44 43 ssrdv 
 |-  ( ph -> B C_ |^| { a e. On | A C_ a } )
45 1 3 44 cofon1 
 |-  ( ph -> |^| { a e. On | A C_ a } = |^| { b e. On | B C_ b } )