% Mizar problem: t64_classes1,classes1,1516,29 
fof(t64_classes1,conjecture,(
    ! [A] : 
      ( v3_ordinal1(A)
     => k5_classes1(A) = A ) ),
    inference(mizar_bg_added,[status(thm)],[cc2_ordinal1,rc1_ordinal1,dt_k5_classes1,cc1_ordinal1,t62_classes1]),
    [file(classes1,t64_classes1)]).

fof(cc2_ordinal1,axiom,(
    ! [A] : 
      ( ( v1_ordinal1(A)
        & v2_ordinal1(A) )
     => v3_ordinal1(A) ) ),
    file(ordinal1,cc2_ordinal1),
    []).

fof(rc1_ordinal1,axiom,(
    ? [A] : 
      ( v1_ordinal1(A)
      & v2_ordinal1(A)
      & v3_ordinal1(A) ) ),
    file(ordinal1,rc1_ordinal1),
    []).

fof(dt_k5_classes1,axiom,(
    $true ),
    file(classes1,k5_classes1),
    []).

fof(cc1_ordinal1,axiom,(
    ! [A] : 
      ( v3_ordinal1(A)
     => ( v1_ordinal1(A)
        & v2_ordinal1(A) ) ) ),
    file(ordinal1,cc1_ordinal1),
    []).

fof(t62_classes1,axiom,(
    ! [A] : 
      ( v1_ordinal1(A)
     => k5_classes1(A) = A ) ),
    file(classes1,t62_classes1),
    []).