Theorem r0weseon

Description: _R0 is a set-like well-ordering of On X. On . Part of Proposition 7.58 of TakeutiZaring p. 54. This theorem is r0weon expressed using _R0 . (Contributed by BTernaryTau, 19-Sep-2026)

	Ref	Expression
Assertion	r0weseon	Could not format assertion : No typesetting found for |- ( _R0 We ( On X. On ) /\ _R0 Se ( On X. On ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-lexo	Could not format LexOrd = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } : No typesetting found for |- LexOrd = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) } with typecode |-
2		df-r0	Could not format _R0 = { <. z , w >. | ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z LexOrd w ) ) ) } : No typesetting found for |- _R0 = { <. z , w >. | ( ( z e. ( On X. On ) /\ w e. ( On X. On ) ) /\ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. ( ( 1st ` w ) u. ( 2nd ` w ) ) \/ ( ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( ( 1st ` w ) u. ( 2nd ` w ) ) /\ z LexOrd w ) ) ) } with typecode |-
3	1 2	r0weon	Could not format ( _R0 We ( On X. On ) /\ _R0 Se ( On X. On ) ) : No typesetting found for |- ( _R0 We ( On X. On ) /\ _R0 Se ( On X. On ) ) with typecode |-