Metamath Proof Explorer

Theorem cofonr

Description: Inverse cofinality law for ordinals. Contrast with cofcutr for surreals. (Contributed by Scott Fenton, 20-Jan-2025)

Ref Expression
Hypotheses cofonr.1 
|- ( ph -> A e. On )
cofonr.2 
|- ( ph -> A = |^| { x e. On | X C_ x } )
Assertion cofonr 
|- ( ph -> A. y e. A E. z e. X y C_ z )

Proof

Step Hyp Ref Expression
1 cofonr.1 
 |-  ( ph -> A e. On )
2 cofonr.2 
 |-  ( ph -> A = |^| { x e. On | X C_ x } )
3 onss 
 |-  ( A e. On -> A C_ On )
4 1 3 syl 
 |-  ( ph -> A C_ On )
5 4 sselda 
 |-  ( ( ph /\ y e. A ) -> y e. On )
6 eloni 
 |-  ( y e. On -> Ord y )
7 ordirr 
 |-  ( Ord y -> -. y e. y )
8 5 6 7 3syl 
 |-  ( ( ph /\ y e. A ) -> -. y e. y )
9 2 adantr 
 |-  ( ( ph /\ y e. A ) -> A = |^| { x e. On | X C_ x } )
10 9 adantr 
 |-  ( ( ( ph /\ y e. A ) /\ X C_ y ) -> A = |^| { x e. On | X C_ x } )
11 5 adantr 
 |-  ( ( ( ph /\ y e. A ) /\ X C_ y ) -> y e. On )
12 simpr 
 |-  ( ( ( ph /\ y e. A ) /\ X C_ y ) -> X C_ y )
13 sseq2 
 |-  ( x = y -> ( X C_ x <-> X C_ y ) )
14 13 elrab 
 |-  ( y e. { x e. On | X C_ x } <-> ( y e. On /\ X C_ y ) )
15 11 12 14 sylanbrc 
 |-  ( ( ( ph /\ y e. A ) /\ X C_ y ) -> y e. { x e. On | X C_ x } )
16 intss1 
 |-  ( y e. { x e. On | X C_ x } -> |^| { x e. On | X C_ x } C_ y )
17 15 16 syl 
 |-  ( ( ( ph /\ y e. A ) /\ X C_ y ) -> |^| { x e. On | X C_ x } C_ y )
18 10 17 eqsstrd 
 |-  ( ( ( ph /\ y e. A ) /\ X C_ y ) -> A C_ y )
19 simplr 
 |-  ( ( ( ph /\ y e. A ) /\ X C_ y ) -> y e. A )
20 18 19 sseldd 
 |-  ( ( ( ph /\ y e. A ) /\ X C_ y ) -> y e. y )
21 8 20 mtand 
 |-  ( ( ph /\ y e. A ) -> -. X C_ y )
22 dfss3 
 |-  ( X C_ y <-> A. z e. X z e. y )
23 21 22 sylnib 
 |-  ( ( ph /\ y e. A ) -> -. A. z e. X z e. y )
24 2 1 eqeltrrd 
 |-  ( ph -> |^| { x e. On | X C_ x } e. On )
25 onintrab2 
 |-  ( E. x e. On X C_ x <-> |^| { x e. On | X C_ x } e. On )
26 24 25 sylibr 
 |-  ( ph -> E. x e. On X C_ x )
27 26 adantr 
 |-  ( ( ph /\ y e. A ) -> E. x e. On X C_ x )
28 onss 
 |-  ( x e. On -> x C_ On )
29 28 adantl 
 |-  ( ( ( ph /\ y e. A ) /\ x e. On ) -> x C_ On )
30 sstr 
 |-  ( ( X C_ x /\ x C_ On ) -> X C_ On )
31 30 expcom 
 |-  ( x C_ On -> ( X C_ x -> X C_ On ) )
32 29 31 syl 
 |-  ( ( ( ph /\ y e. A ) /\ x e. On ) -> ( X C_ x -> X C_ On ) )
33 32 rexlimdva 
 |-  ( ( ph /\ y e. A ) -> ( E. x e. On X C_ x -> X C_ On ) )
34 27 33 mpd 
 |-  ( ( ph /\ y e. A ) -> X C_ On )
35 34 sselda 
 |-  ( ( ( ph /\ y e. A ) /\ z e. X ) -> z e. On )
36 ontri1 
 |-  ( ( y e. On /\ z e. On ) -> ( y C_ z <-> -. z e. y ) )
37 5 35 36 syl2an2r 
 |-  ( ( ( ph /\ y e. A ) /\ z e. X ) -> ( y C_ z <-> -. z e. y ) )
38 37 rexbidva 
 |-  ( ( ph /\ y e. A ) -> ( E. z e. X y C_ z <-> E. z e. X -. z e. y ) )
39 rexnal 
 |-  ( E. z e. X -. z e. y <-> -. A. z e. X z e. y )
40 38 39 bitrdi 
 |-  ( ( ph /\ y e. A ) -> ( E. z e. X y C_ z <-> -. A. z e. X z e. y ) )
41 23 40 mpbird 
 |-  ( ( ph /\ y e. A ) -> E. z e. X y C_ z )
42 41 ralrimiva 
 |-  ( ph -> A. y e. A E. z e. X y C_ z )