% Mizar ND problem: t1_card_4,card_4,39,38 
fof(dh_c1_1__card_4,definition,
    ( ( v1_finset_1(c1_1__card_4)
    <=> v1_finset_1(k1_card_1(c1_1__card_4)) )
   => ! [A] : 
        ( v1_finset_1(A)
      <=> v1_finset_1(k1_card_1(A)) ) ),
    introduced(definition,[new_symbol(c1_1__card_4),file(card_4,c1_1__card_4)]),
    [interesting(0.8),axiom,file(card_4,c1_1__card_4)]).

fof(cc1_card_1,theorem,(
    ! [A] : 
      ( v1_card_1(A)
     => ( v1_ordinal1(A)
        & v2_ordinal1(A)
        & v3_ordinal1(A) ) ) ),
    file(card_1,cc1_card_1),
    [interesting(0.9),axiom,file(card_1,cc1_card_1)]).

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

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

fof(rc1_card_1,theorem,(
    ? [A] : v1_card_1(A) ),
    file(card_1,rc1_card_1),
    [interesting(0.9),axiom,file(card_1,rc1_card_1)]).

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

fof(rc2_card_1,theorem,(
    ? [A] : 
      ( v1_ordinal1(A)
      & v2_ordinal1(A)
      & v3_ordinal1(A)
      & v1_finset_1(A)
      & v1_card_1(A) ) ),
    file(card_1,rc2_card_1),
    [interesting(0.9),axiom,file(card_1,rc2_card_1)]).

fof(symmetry_r2_wellord2,theorem,(
    ! [A,B] : 
      ( r2_wellord2(A,B)
     => r2_wellord2(B,A) ) ),
    file(wellord2,r2_wellord2),
    [interesting(0.9),axiom,file(wellord2,r2_wellord2)]).

fof(reflexivity_r2_wellord2,theorem,(
    ! [A,B] : r2_wellord2(A,A) ),
    file(wellord2,r2_wellord2),
    [interesting(0.9),axiom,file(wellord2,r2_wellord2)]).

fof(redefinition_r2_wellord2,definition,(
    ! [A,B] : 
      ( r2_wellord2(A,B)
    <=> r2_tarski(A,B) ) ),
    file(wellord2,r2_wellord2),
    [interesting(0.9),axiom,file(wellord2,r2_wellord2)]).

fof(dt_k1_card_1,axiom,(
    ! [A] : v1_card_1(k1_card_1(A)) ),
    file(card_1,k1_card_1),
    [interesting(0.9),axiom,file(card_1,k1_card_1)]).

fof(dt_c1_1__card_4,assumption,(
    $true ),
    introduced(assumption,[file(card_4,c1_1__card_4)]),
    [interesting(0.8),axiom,file(card_4,c1_1__card_4)]).

fof(fc2_card_1,theorem,(
    ! [A] : 
      ( v1_finset_1(A)
     => ( v1_ordinal1(k1_card_1(A))
        & v2_ordinal1(k1_card_1(A))
        & v3_ordinal1(k1_card_1(A))
        & v1_finset_1(k1_card_1(A))
        & v1_card_1(k1_card_1(A)) ) ) ),
    file(card_1,fc2_card_1),
    [interesting(0.9),axiom,file(card_1,fc2_card_1)]).

fof(d5_card_1,definition,(
    ! [A,B] : 
      ( v1_card_1(B)
     => ( B = k1_card_1(A)
      <=> r2_wellord2(A,B) ) ) ),
    file(card_1,d5_card_1),
    [interesting(0.9),axiom,file(card_1,d5_card_1)]).

fof(e1_1__card_4,plain,(
    r2_wellord2(c1_1__card_4,k1_card_1(c1_1__card_4)) ),
    inference(mizar_by,[status(thm),assumptions([dt_c1_1__card_4])],[cc1_ordinal1,cc2_ordinal1,rc1_ordinal1,symmetry_r2_wellord2,reflexivity_r2_wellord2,redefinition_r2_wellord2,dt_k1_card_1,dt_c1_1__card_4,cc1_card_1,rc1_card_1,d5_card_1]),
    [interesting(0.8),file(card_4,e1_1__card_4),[file(card_4,e1_1__card_4)]]).

fof(t68_card_1,theorem,(
    ! [A,B] : 
      ( ( r2_wellord2(A,B)
        & v1_finset_1(A) )
     => v1_finset_1(B) ) ),
    file(card_1,t68_card_1),
    [interesting(0.9),axiom,file(card_1,t68_card_1)]).

fof(e2_1__card_4,plain,
    ( v1_finset_1(c1_1__card_4)
  <=> v1_finset_1(k1_card_1(c1_1__card_4)) ),
    inference(mizar_by,[status(thm),assumptions([dt_c1_1__card_4])],[cc1_card_1,cc1_ordinal1,cc2_ordinal1,rc1_card_1,rc1_ordinal1,rc2_card_1,symmetry_r2_wellord2,reflexivity_r2_wellord2,redefinition_r2_wellord2,dt_k1_card_1,dt_c1_1__card_4,fc2_card_1,e1_1__card_4,t68_card_1]),
    [interesting(0.8),file(card_4,e2_1__card_4),[file(card_4,e2_1__card_4)]]).

fof(i2_1__card_4,theorem,(
    $true ),
    introduced(tautology,[file(card_4,i2_1__card_4)]),
    [interesting(0.8),trivial,file(card_4,i2_1__card_4)]).

fof(i1_1__card_4,plain,
    ( v1_finset_1(c1_1__card_4)
  <=> v1_finset_1(k1_card_1(c1_1__card_4)) ),
    inference(conclusion,[status(thm),assumptions([dt_c1_1__card_4])],[e2_1__card_4,i2_1__card_4]),
    [interesting(0.8),file(card_4,i1_1__card_4),[file(card_4,i1_1__card_4)]]).

fof(i1_1_tmp__card_4,plain,
    ( v1_finset_1(c1_1__card_4)
  <=> v1_finset_1(k1_card_1(c1_1__card_4)) ),
    inference(discharge_asm,[status(thm),assumptions([]),discharge_asm(discharge,[dt_c1_1__card_4])],[dt_c1_1__card_4,i1_1__card_4]),
    [interesting(1),t1_card_4]).

fof(t1_card_4,theorem,(
    ! [A] : 
      ( v1_finset_1(A)
    <=> v1_finset_1(k1_card_1(A)) ) ),
    inference(let,[status(thm),assumptions([])],[i1_1_tmp__card_4,dh_c1_1__card_4]),
    [interesting(1),file(card_4,t1_card_4),[file(card_4,t1_card_4)]]).