src/ZF/AC/AC1_WO2.ML
changeset 2469 b50b8c0eec01
parent 2167 5819e85ad261
child 4091 771b1f6422a8
equal deleted inserted replaced
2468:428efffe8599 2469:b50b8c0eec01
    11 val [prem] = goal thy "f : (PROD X:Pow(x) - {0}. X) ==>  \
    11 val [prem] = goal thy "f : (PROD X:Pow(x) - {0}. X) ==>  \
    12 \       ?g(f) : bij(x, LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x})";
    12 \       ?g(f) : bij(x, LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x})";
    13 by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1);
    13 by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1);
    14 by (rtac f_subsets_imp_UN_HH_eq_x 1);
    14 by (rtac f_subsets_imp_UN_HH_eq_x 1);
    15 by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2));
    15 by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2));
    16 by (fast_tac (AC_cs addSDs [equals0D, prem RS apply_type]) 1);
    16 by (fast_tac (!claset addSDs [equals0D, prem RS apply_type]) 1);
    17 by (fast_tac (AC_cs addSIs [prem RS Pi_weaken_type]) 1);
    17 by (fast_tac (!claset addSIs [prem RS Pi_weaken_type]) 1);
    18 val lemma1 = uresult() |> standard;
    18 val lemma1 = uresult() |> standard;
    19 
    19 
    20 goalw thy [AC1_def, WO2_def, eqpoll_def] "!!Z. AC1 ==> WO2";
    20 goalw thy [AC1_def, WO2_def, eqpoll_def] "!!Z. AC1 ==> WO2";
    21 by (rtac allI 1);
    21 by (rtac allI 1);
    22 by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1);
    22 by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1);
    23 by (fast_tac (AC_cs addSDs [lemma1] addSIs [Ord_Least]) 1);
    23 by (fast_tac (!claset addSDs [lemma1] addSIs [Ord_Least]) 1);
    24 qed "AC1_WO2";
    24 qed "AC1_WO2";