let phi be Ordinal-Sequence; :: thesis: ( phi is increasing implies phi is one-to-one )
assume A1: for A, B being Ordinal st A in B & B in dom phi holds
phi . A in phi . B ; :: according to ORDINAL2:def 16 :: thesis: phi is one-to-one
let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in dom phi or not b₁ in dom phi or not phi . x = phi . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in dom phi or not y in dom phi or not phi . x = phi . y or x = y )
assume A2: ( x in dom phi & y in dom phi & phi . x = phi . y ) ; :: thesis: x = y
then reconsider A = x, B = y as Ordinal ;
( not phi . A in phi . B & ( A in B or A = B or B in A ) ) by A2, ORDINAL1:24;
hence x = y by A1, A2; :: thesis: verum