Part1.mg

Name Size Modified
.. — —
Descr_Vo1_prop.html 3 KB
Descr_ii_prop.html 5 KB
Descr_iii_prop.html 7 KB
EmptyE.html 729 bytes
Empty_In_Power.html 668 bytes
Empty_Subq_eq.html 1 KB
Empty_eq.html 1 KB
Eps_i_ex.html 940 bytes
FalseE.html 229 bytes
If_i_0.html 4 KB
If_i_1.html 4 KB
If_i_correct.html 5 KB
If_i_or.html 2 KB
If_ii_0.html 1 KB
If_ii_1.html 1 KB
If_iii_0.html 2 KB
If_iii_1.html 2 KB
In_0_1.html 331 bytes
In_0_2.html 519 bytes
In_1_2.html 331 bytes
In_1_3.html 413 bytes
In_1_4.html 413 bytes
In_1_5.html 413 bytes
In_1_6.html 413 bytes
In_1_7.html 413 bytes
In_1_8.html 413 bytes
In_2_3.html 204 bytes
In_2_4.html 413 bytes
In_2_5.html 413 bytes
In_3_4.html 204 bytes
In_3_5.html 413 bytes
In_4_5.html 204 bytes
In_irref.html 1 KB
In_no2cycle.html 2 KB
In_rec_G_ii_In_rec_ii.html 3 KB
In_rec_G_ii_In_rec_ii_d.html 2 KB
In_rec_G_ii_c.html 4 KB
In_rec_G_ii_f.html 11 KB
In_rec_G_ii_inv.html 10 KB
In_rec_G_iii_In_rec_iii.html 3 KB
In_rec_G_iii_In_rec_iii_d.html 2 KB
In_rec_G_iii_c.html 5 KB
In_rec_G_iii_f.html 12 KB
In_rec_G_iii_inv.html 10 KB
In_rec_i_G_In_rec_i.html 3 KB
In_rec_i_G_In_rec_i_d.html 2 KB
In_rec_i_G_c.html 4 KB
In_rec_i_G_f.html 11 KB
In_rec_i_G_inv.html 9 KB
In_rec_i_eq.html 1 KB
In_rec_ii_eq.html 1 KB
In_rec_iii_eq.html 1 KB
Inj0E.html 549 bytes
Inj0I.html 549 bytes
Inj0_0.html 351 bytes
Inj0_Inj1_neq.html 4 KB
Inj0_inj.html 1 KB
Inj0_pair_0_eq.html 1 KB
Inj0_setsum.html 2 KB
Inj0_setsum_0L.html 9 KB
Inj1E.html 5 KB
Inj1I1.html 1 KB
Inj1I2.html 2 KB
Inj1NE1.html 1 KB
Inj1NE2.html 1 KB
Inj1_eq.html 5 KB
Inj1_inj.html 1 KB
Inj1_pair_1_eq.html 1 KB
Inj1_setsum.html 2 KB
Inj1_setsum_1L.html 15 KB
KnasterTarski_set.html 13 KB
PiI.html 11 KB
PigeonHole_nat.html 57 KB
PigeonHole_nat_bij.html 26 KB
PowerE.html 648 bytes
PowerI.html 648 bytes
ReplE.html 705 bytes
ReplE__2.html 2 KB
ReplE_impred.html 1 KB
ReplEq_ext.html 2 KB
ReplEq_ext_sub.html 4 KB
ReplEq_setprod_ext.html 5 KB
ReplI.html 2 KB
ReplSepE.html 4 KB
ReplSepE_impred.html 2 KB
ReplSepI.html 1 KB
Repl_Empty.html 2 KB
Repl_inv_eq.html 7 KB
Repl_invol_eq.html 658 bytes
SchroederBernstein.html 69 KB
Self_In_Power.html 617 bytes
SepE.html 18 KB
SepE1.html 801 bytes
SepE2.html 768 bytes
SepI.html 9 KB
Sep_Empty.html 1 KB
Sep_In_Power.html 826 bytes
Sep_Subq.html 211 bytes
Sigma_E.html 6 KB
Sigma_eta_proj0_proj1.html 11 KB
SingE.html 917 bytes
SingI.html 425 bytes
Sing_inj.html 1 KB
Subq_1_Sing0.html 2 KB
Subq_2_UPair01.html 4 KB
Subq_Empty.html 770 bytes
Subq_Sing0_1.html 1023 bytes
Subq_binunion_eq.html 4 KB
Subq_contra.html 442 bytes
Subq_finite.html 18 KB
Subq_ref.html 388 bytes
Subq_tra.html 962 bytes
TransSet_In_ordsucc_Subq.html 1 KB
TransSet_ordsucc.html 4 KB
TransSet_ordsucc_In_Subq.html 3 KB
TrueI.html 231 bytes
UPairE.html 8 KB
UPairI1.html 6 KB
UPairI2.html 5 KB
UnionE.html 1 KB
UnionE_impred.html 1 KB
UnionI.html 2 KB
Union_ordsucc_eq.html 6 KB
Unj_Inj0_eq.html 16 KB
Unj_Inj1_eq.html 18 KB
Unj_eq.html 6 KB
ZF_Power_closed.html 897 bytes
ZF_Repl_closed.html 1 KB
ZF_Sing_closed.html 638 bytes
ZF_UPair_closed.html 35 KB
ZF_Union_closed.html 896 bytes
ZF_binunion_closed.html 1 KB
ZF_closed_E.html 767 bytes
ZF_ordsucc_closed.html 1 KB
add_nat_0L.html 3 KB
add_nat_0R.html 645 bytes
add_nat_1_1_2.html 2 KB
add_nat_SL.html 6 KB
add_nat_SR.html 865 bytes
add_nat_com.html 5 KB
add_nat_p.html 4 KB
adjoin_finite.html 33 KB
and3E.html 765 bytes
and3I.html 926 bytes
and4I.html 961 bytes
and5I.html 1 KB
andEL.html 412 bytes
andER.html 412 bytes
andI.html 351 bytes
ap0_Sigma.html 550 bytes
ap1_Sigma.html 780 bytes
apE.html 6 KB
apI.html 4 KB
ap_Pi.html 1 KB
beta.html 5 KB
bijE.html 1 KB
bijI.html 2 KB
bij_comp.html 11 KB
bij_id.html 2 KB
bij_inv.html 12 KB
binintersectE.html 693 bytes
binintersectE1.html 695 bytes
binintersectE2.html 695 bytes
binintersectI.html 753 bytes
binintersect_Subq_1.html 229 bytes
binintersect_Subq_2.html 229 bytes
binintersect_Subq_eq_1.html 1 KB
binintersect_Subq_max.html 2 KB
binintersect_com.html 1 KB
binintersect_com_Subq.html 1 KB
binunionE.html 4 KB
binunionE__2.html 1 KB
binunionI1.html 2 KB
binunionI2.html 2 KB
binunion_Subq_1.html 221 bytes
binunion_Subq_2.html 221 bytes
binunion_Subq_min.html 2 KB
binunion_asso.html 9 KB
binunion_com.html 1 KB
binunion_com_Subq.html 2 KB
binunion_finite.html 3 KB
binunion_idl.html 3 KB
binunion_idr.html 835 bytes
cases_1.html 2 KB
cases_2.html 2 KB
cases_3.html 2 KB
dneg.html 1 KB
eq_1_Sing0.html 774 bytes
eq_i_tra.html 555 bytes
eq_or_nand.html 5 KB
equip_0_Empty.html 2 KB
equip_ref.html 1 KB
equip_sym.html 2 KB
equip_tra.html 2 KB
exactly1of2_E.html 2 KB
exactly1of2_I1.html 1 KB
exactly1of2_I2.html 1 KB
exactly1of2_or.html 2 KB
exandE_i.html 1 KB
exandE_ii.html 1 KB
exandE_iii.html 1 KB
exandE_iiii.html 1 KB
f_eq_i.html 419 bytes
famunionE.html 4 KB
famunionE_impred.html 1 KB
famunionI.html 1 KB
famunion_Empty.html 2 KB
famunion_Subq.html 2 KB
famunion_ext.html 2 KB
famunion_nat_finite.html 14 KB
finite_Empty.html 1 KB
finite_ind.html 30 KB
iffEL.html 568 bytes
iffER.html 568 bytes
iffI.html 566 bytes
iff_refl.html 902 bytes
iff_sym.html 1 KB
iff_trans.html 2 KB
image_In_Power.html 3 KB
image_monotone.html 2 KB
inj_linv.html 3 KB
lamE.html 215 bytes
lamI.html 221 bytes
lamI2.html 1 KB
lam_Pi.html 11 KB
least_ordinal_ex.html 5 KB
mul_nat_0R.html 650 bytes
mul_nat_SR.html 870 bytes
mul_nat_p.html 4 KB
nat_0.html 233 bytes
nat_0_in_ordsucc.html 2 KB
nat_1.html 438 bytes
nat_2.html 438 bytes
nat_3.html 409 bytes
nat_4.html 409 bytes
nat_5.html 409 bytes
nat_6.html 409 bytes
nat_7.html 409 bytes
nat_8.html 409 bytes
nat_Subq_add_ex.html 12 KB
nat_complete_ind.html 7 KB
nat_ind.html 7 KB
nat_inv.html 1 KB
nat_inv_impred.html 773 bytes
nat_ordsucc.html 553 bytes
nat_ordsucc_in_ordsucc.html 8 KB
nat_ordsucc_trans.html 3 KB
nat_p_UnivOf_Empty.html 2 KB
nat_p_omega.html 2 KB
nat_p_ordinal.html 2 KB
nat_p_trans.html 4 KB
nat_primrec_0.html 4 KB
nat_primrec_S.html 7 KB
nat_primrec_r.html 14 KB
nat_setsum1_ordsucc.html 25 KB
nat_trans.html 6 KB
neq_0_1.html 339 bytes
neq_0_2.html 339 bytes
neq_0_ordsucc.html 2 KB
neq_1_0.html 339 bytes
neq_1_2.html 539 bytes
neq_1_3.html 433 bytes
neq_2_0.html 339 bytes
neq_2_3.html 433 bytes
neq_2_4.html 433 bytes
neq_3_4.html 433 bytes
neq_i_sym.html 549 bytes
neq_ordsucc_0.html 801 bytes
not_all_ex_demorgan_i.html 2 KB
not_ex_all_demorgan_i.html 885 bytes
not_or_and_demorgan.html 2 KB
omega_TransSet.html 2 KB
omega_nat_p.html 730 bytes
omega_ordinal.html 2 KB
omega_ordsucc.html 981 bytes
or3E.html 644 bytes
or3I1.html 804 bytes
or3I2.html 804 bytes
or3I3.html 468 bytes
orIL.html 298 bytes
orIR.html 298 bytes
ordinal_1.html 413 bytes
ordinal_2.html 413 bytes
ordinal_Empty.html 2 KB
ordinal_Hered.html 4 KB
ordinal_In_Or_Subq.html 4 KB
ordinal_TransSet.html 834 bytes
ordinal_binintersect.html 3 KB
ordinal_binunion.html 3 KB
ordinal_famunion.html 10 KB
ordinal_ind.html 3 KB
ordinal_lim_or_succ.html 4 KB
ordinal_linear.html 2 KB
ordinal_ordsucc.html 5 KB
ordinal_ordsucc_In.html 4 KB
ordinal_ordsucc_In_Subq.html 983 bytes
ordinal_ordsucc_In_eq.html 6 KB
ordinal_trichotomy_or.html 19 KB
ordinal_trichotomy_or_impred.html 1 KB
ordsuccE.html 2 KB
ordsuccI1.html 855 bytes
ordsuccI2.html 758 bytes
ordsucc_inj.html 5 KB
ordsucc_inj_contra.html 1 KB
ordsucc_omega_ordinal.html 450 bytes
pairE.html 705 bytes
pairE0.html 7 KB
pairE1.html 8 KB
pairI0.html 461 bytes
pairI1.html 461 bytes
pair_Sigma.html 4 KB
pair_Sigma_E1.html 3 KB
pair_ap_0.html 1 KB
pair_ap_1.html 1 KB
pair_p_I.html 1 KB
pair_tuple_fun.html 1 KB
pred_ext.html 1 KB
proj0E.html 6 KB
proj0I.html 4 KB
proj0_Sigma.html 2 KB
proj0_ap_0.html 4 KB
proj0_pair_eq.html 5 KB
proj1E.html 6 KB
proj1I.html 4 KB
proj1_Sigma.html 2 KB
proj1_ap_1.html 4 KB
proj1_pair_eq.html 5 KB
proj_Sigma_eta.html 2 KB
prop_ext_2.html 985 bytes
setminusE.html 689 bytes
setminusE1.html 691 bytes
setminusE2.html 691 bytes
setminusI.html 751 bytes
setminus_In_Power.html 515 bytes
setminus_Subq.html 221 bytes
setminus_Subq_contra.html 3 KB
setminus_antimonotone.html 2 KB
setminus_idr.html 1 KB
setsum_0_0.html 908 bytes
setsum_1_0_1.html 454 bytes
setsum_1_1_2.html 454 bytes
setsum_Inj_inv.html 4 KB
surj_rinv.html 1 KB
tuple_2_0_eq.html 1 KB
tuple_2_1_eq.html 1 KB
tuple_2_Sigma.html 211 bytes
tuple_2_setprod.html 678 bytes
tuple_pair.html 30 KB
xm.html 13 KB