Metamath Proof Explorer

Theorem nulchn

Description: Empty set is an increasing chain for every range and every relation. (Contributed by Ender Ting, 19-Nov-2024) (Revised by Ender Ting, 17-Jan-2026)

Ref Expression
Assertion nulchn 
|- (/) e. ( .< Chain A )

Proof

Step Hyp Ref Expression
1 wrd0 
 |-  (/) e. Word A
2 dm0 
 |-  dom (/) = (/)
3 2 difeq1i 
 |-  ( dom (/) \ { 0 } ) = ( (/) \ { 0 } )
4 0dif 
 |-  ( (/) \ { 0 } ) = (/)
5 3 4 eqtri 
 |-  ( dom (/) \ { 0 } ) = (/)
6 rzal 
 |-  ( ( dom (/) \ { 0 } ) = (/) -> A. x e. ( dom (/) \ { 0 } ) ( (/) ` ( x - 1 ) ) .< ( (/) ` x ) )
7 5 6 ax-mp 
 |-  A. x e. ( dom (/) \ { 0 } ) ( (/) ` ( x - 1 ) ) .< ( (/) ` x )
8 1 7 pm3.2i 
 |-  ( (/) e. Word A /\ A. x e. ( dom (/) \ { 0 } ) ( (/) ` ( x - 1 ) ) .< ( (/) ` x ) )
9 ischn 
 |-  ( (/) e. ( .< Chain A ) <-> ( (/) e. Word A /\ A. x e. ( dom (/) \ { 0 } ) ( (/) ` ( x - 1 ) ) .< ( (/) ` x ) ) )
10 8 9 mpbir 
 |-  (/) e. ( .< Chain A )