List of theorems referencing the symbol ONE_1_MAP

(46) Theorem one_1_test.1: [One-one map former test] ((x_thryvar in s) & (y_thryvar in s) & (((a(x_thryvar) = a(y_thryvar)) •neq (b(x_thryvar) = b(y_thryvar))))) or one_1_map({[a(x),b(x)]: x in s})
(47) Theorem one_1_test_2.1: [One-one map former test, two-variable case] ((x_thryvar in s) & (y_thryvar in t) & (x2_thryvar in s) & (y2_thryvar in t) & (not((a2(x_thryvar,y_thryvar) = a2(x2_thryvar,y2_thryvar)) •eq (b2(x_thryvar,y_thryvar) = b2(x2_thryvar,y2_thryvar))))) or one_1_map({[a2(x,y),b2(x,y)]: x in s, y in t})
(48) Theorem one_1_test_3.1: [Single-valued map former, three-variable case] ((x_thryvar in s) & (y_thryvar in t) & (z_thryvar in r) & (xp_thryvar in s) & (yp_thryvar in t) & (zp_thryvar in r) & P3(x_thryvar,y_thryvar,z_thryvar) & P3(xp_thryvar,yp_thryvar,zp_thryvar) & (((a3(x_thryvar,y_thryvar,z_thryvar) /= a3(xp_thryvar,yp_thryvar,zp_thryvar)) •eq (b3(x_thryvar,y_thryvar,z_thryvar) = b3(xp_thryvar,yp_thryvar,zp_thryvar))))) or one_1_map({[a3(x,y,wz),b3(x,y,wz)]: x in s, y in t,wz in r | P3(x,y,wz)})
(75) Theorem 54: [One-one map subsets are one-one] ((G •incin F) & one_1_map(F)) •imp one_1_map(G)
(79) Theorem 58: [Restrictions of one-one maps are one-one] one_1_map(F) •imp one_1_map(F •ON S)
(80) Theorem 59: [The null set as a map] Is_map(0) & Svm(0) & (one_1_map(0)) & (range(0) = 0) & (domain(0) = 0)
(100) Theorem fcn_symbol.6: [Mapformer one-to-oneness test] ((x_thryvar in s) & (y_thryvar in s) & (f(x_thryvar) = f(y_thryvar)) & (x_thryvar /= y_thryvar)) or one_1_map(g)
(115) Theorem 83: [One-one map-restriction to an intersection] one_1_map(F) •imp (range(F •ON (S * T)) = range(F •ON S) * range(F •ON T))
(117) Theorem 85: [One-one map restriction to disjoint sets] (one_1_map(F) & (S * T = 0)) •imp (range(F •ON S) * range(F •ON T) = 0)
(120) Theorem 88: [Union of 1-1 maps] (one_1_map(F) & one_1_map(G) & (range(F) * range(G) = 0) & (domain(F) * domain(G) = 0)) •imp one_1_map(F + G)
(121) Theorem 89: [Union of 1-1 maps, 2] (one_1_map(F + G) & ((G * F) = 0)) •imp ((domain(G) = (domain(F + G) - domain(F))) & (range(G) = (range(F + G) - range(F))))
(123) Theorem 91: [Singletons as maps] Svm({[X,Y]}) & one_1_map({[X,Y]}) & (({[X,Y]}~[X]) = Y)
(129) Theorem 97: [Range of restriction of one-one map] (one_1_map(F) & (S •incin domain(F)) & (S /= domain(F))) •imp ((range(F •ON S) •incin range(F)) & (range(F •ON S) /= range(F)))
(132) Theorem 100: [Inverse of a one-one map] one_1_map(F) •imp (one_1_map(inv(F)) & (F = inv(inv(F))) & (range(inv(F)) = domain(F)) & (domain(inv(F)) = range(F)))
(133) Theorem 101: [Inverse image of an element] (one_1_map(F) & (X in domain(F))) •imp (inv(F)~[F~[X]] = X)
(134) Theorem 102: [Inverse image of an element's map image] one_1_map(F) •imp (((X in domain(F)) •imp (inv(F)~[F~[X]] = X)) & ((X in range(F)) •imp (F~[inv(F)~[X]] = X)))
(149) Theorem 110: [Elementary properties of identity maps] one_1_map(ident(S)) & (domain(ident(S)) = S) & (range(ident(S)) = S) & (inv(ident(S)) = ident(S)) & ((X in S) •imp (ident(S)~[X] = X)) & (Is_map(F) •imp (((domain(F) •incin S) •imp (F @ ident(S) = F)) & ((range(F) •incin S) •imp (ident(S) @ F = F))))
(152) Theorem 113: [Inverses of one-one maps] one_1_map(F) •imp (((F @ inv(F)) = ident(range(F))) & ((inv(F) @ F) = ident(domain(F))))
(155) Theorem 116: [One-one-ness and singlevaluedness] one_1_map(F) •eq (Svm(F) & Svm(inv(F)))
(156) Theorem 117: [An inverse pair of maps must be 1-1 and must be each other's inverses] (Is_map(F) & Is_map(G) & (domain(F) = range(G)) & (range(F) = domain(G)) & (F @ G = ident(range(F))) & (G @ F = ident(domain(F)))) •imp (one_1_map(F) & (G = inv(F)))
(161) Theorem 122: [Images under one-one maps] (one_1_map(F) & (X in domain(F)) & (Y in domain(F)) & (F~[X] = F~[Y])) •imp (X = Y)
(166) Theorem 127: [Single-valued and one-one maps] Is_map(F) •imp (one_1_map(F) •eq one_1_map(inv(F)))
(167) Theorem 128: [Composition of one-one maps] (one_1_map(F) & one_1_map(G)) •imp one_1_map(F @ G)
(168) Theorem 129: [Elements are defined uniquely by their one-one images] Svm(F) •imp (one_1_map(F) •eq (FORALL x in domain(F), y in domain(F) | ((F~[x] = F~[y]) •imp (x = y))))
(169) Theorem 130: [A 1-1 map on a set u induces a 1-1 map on the power set of u] (one_1_map(F) & (S •incin domain(F)) & (T •incin domain(F)) & (S /= T)) •imp (range(F •ON S) /= range(F •ON T))
(172) Theorem 133: [Single-valued maps have 1-1 partial inverses] Svm(F) •imp (EXISTS h | ((domain(h) = range(F)) & (range(h) •incin domain(F)) & one_1_map(h)) & (FORALL x in range(F) | (F~[h~[x]] = x)))
(178) Theorem 139: [Cartesian modified associativity] (F = {[[[x,y],z],[x,[y,z]]]: x in A, y in B, z in C}) •imp (one_1_map(F) & (domain(F) = ((A •PROD B) •PROD C)) & (range(F) = (A •PROD (B •PROD C))))
(179) Theorem 140: [Cartesian modified commutativity] (F = {[[x,y],[y,x]]: x in A, y in B}) •imp (one_1_map(F) & (domain(F) = (A •PROD B)) & (range(F) = (B •PROD A)))
(181) Theorem 142: [Cardinality lemma] Ord(#S) & (EXISTS f in OM | (one_1_map(f) & (range(f) = S) & (domain(f) = #S))) & (not((EXISTS o in #S | (EXISTS g in OM | one_1_map(g) & (range(g) = S) & (domain(g) = o)))))
(189) Theorem 150: [Enumerability lemma] (Ord(S) & (T •incin S)) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (domain(f) •incin S) & (range(f) = T))
(190) Theorem 151: [Cardinality theorem] Card(#S) & Ord(#S) & (EXISTS f in OM | one_1_map(f) & (range(f) = S) & (domain(f) = #S))
(191) Theorem 152: [One-one maps are cardinality preserving] one_1_map(F) •imp (#range(F) = #domain(F))
(192) Theorem 153: [Equicardinality is equivalent to one-one correspondence] (EXISTS F in OM | (one_1_map(F) & (range(F) = S) & (domain(F) = T))) •eq (#S = #T)
(199) Theorem 160: [Uniqueness of Cardinality] (Card(C) & (EXISTS f in OM | (one_1_map(f) & (range(f) = S) & domain(f) = C))) •imp (C = #S)
(217) Theorem 177: [Inverse image of a range element] (one_1_map(G) & (Y in range(G))) •imp (G •INV_IM {Y} = {inv(G)~[Y]})
(225) Theorem 185: [One-one maps preserve finiteness] one_1_map(F) •imp ((Finite(domain(F))) •imp (Finite(range(F))))
(226) Theorem 186: [One-one maps preserve finiteness, 2] one_1_map(F) •imp (Finite(domain(F)) •eq Finite(range(F)))
(234) Theorem 193: [Interchange lemma] ((X in S) & (Y in S)) •imp (EXISTS f | one_1_map(f) & (range(f) = S) & (domain(f) = S) & ((f~[X]) = Y) & ((f~[Y]) = X))
(385) Theorem subseq.1: (g = (f @ h_thryvar)) & one_1_map(h_thryvar) & (domain(h_thryvar) in next(Za)) & (range(h_thryvar) •incin domain(f)) & (FORALL i in domain(h_thryvar), j in domain(h_thryvar) | (i in j) •imp ((h_thryvar~[i]) in (h_thryvar~[j])))
(408) Theorem well_founded_set.8: (EXISTS o in next(#pow(s)) | (Ord(o) & (s = {ordenm_thryvar(x): x in o}) & (FORALL x in o | (ordenm_thryvar(x) /= s)) & one_1_map({[x,ordenm_thryvar(x)]: x in o})))
(409) Theorem well_founded_set.9: (ord_thryvar in next(#pow(s))) & Ord(ord_thryvar) & (s = {ordenm_thryvar(x): x in ord_thryvar}) & (FORALL x in ord_thryvar | (ordenm_thryvar(x) /= s)) & one_1_map({[x,ordenm_thryvar(x)]: x in ord_thryvar})
(412) Theorem well_ordered_set.100: (FORALL x,y | ((x in s) & (y in s)) •imp ((not (arg1_bef_arg2(x,y) & arg1_bef_arg2(y,x))) & (not arg1_bef_arg2(x,x)))) & (FORALL x | (not(s •incin {ordenm_thryvar(y): y in x})) •imp ((ordenm_thryvar(x) in (s - {ordenm_thryvar(y): y in x})) & (FORALL y in (s - {ordenm_thryvar(y): y in x}) | not(arg1_bef_arg2(y,ordenm_thryvar(x)))))) & (FORALL x | (s •incin {ordenm_thryvar(y): y in x}) •eq (ordenm_thryvar(x) = s)) & (FORALL x | (ordenm_thryvar(x) /= s) •imp (ordenm_thryvar(x) in s)) & (FORALL u, v | (Ord(u) & Ord(v) & (ordenm_thryvar(u) /= s) & arg1_bef_arg2(ordenm_thryvar(u),ordenm_thryvar(v))) •imp (u in v)) & (FORALL v | {u: u in s | arg1_bef_arg2(u,ordenm_thryvar(v))} •incin {ordenm_thryvar(x): x in v}) & (FORALL u, v | (Ord(u) & Ord(v) & (ordenm_thryvar(u) /= s) & (ordenm_thryvar(v) /= s) & (u /= v)) •imp (ordenm_thryvar(u) /= ordenm_thryvar(v))) & (EXISTS o in next(#pow(s)) | (Ord(o) & (s = {ordenm_thryvar(x): x in o}) & (FORALL x in o | (ordenm_thryvar(x) /= s)) & one_1_map({[x,ordenm_thryvar(x)]: x in o}))) & (FORALL x | ordenm_thryvar(x) = Minrel_thryvar(s - {ordenm_thryvar(y): y in x})) & (FORALL t | Minrel_thryvar(t) = if (t •incin s) & (t /= 0) then arb({m: m in t | (FORALL y in t | (not arg1_bef_arg2(y,m)))}) else s end if)
(419) Theorem well_ordered_set.8: (EXISTS o | (Ord(o) & (s = {ordenm_thryvar(x): x in o}) & (FORALL x in o | (ordenm_thryvar(x) /= s)) & one_1_map({[x,ordenm_thryvar(x)]: x in o})))
(424) Theorem well_ordered_set.9: (Ord(V) & (ordenm_thryvar(V) /= s)) •imp ( one_1_map({[x,ordenm_thryvar(x)]: x in V}) & (domain({[x,ordenm_thryvar(x)]: x in V}) = V) & (range({[x,ordenm_thryvar(x)]: x in V}) = {u: u in s | arg1_bef_arg2(u,ordenm_thryvar(V))}) & ({u: u in s | arg1_bef_arg2(u,ordenm_thryvar(V))} = {ordenm_thryvar(x): x in V}))
(436) Theorem 343: (Ord(O1) & Ord(O2)) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (range(f) = (O1 •PROD O2)) & (FORALL x in domain(f), y in domain(f) | (x in y) •eq (((car(f~[x]) + cdr(f~[x])) in (car(f~[y]) + cdr(f~[y]))) or (((car(f~[x]) + cdr(f~[x])) = (car(f~[y]) + cdr(f~[y]))) & (car(f~[x]) in car(f~[y]))) or (((car(f~[x]) + cdr(f~[x])) = (car(f~[y]) + cdr(f~[y]))) & (car(f~[x]) = car(f~[y])) & (cdr(f~[x]) in cdr(f~[y]))))))
(437) Theorem 344: (Card(O1) & Card(O2) & (not Finite(O1 + O2))) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (range(f) = (O1 •PROD O2)) & (FORALL x in domain(f) | (EXISTS y in (O1 + O2) | range(f •ON x) •incin (y •PROD y))))
(499) Theorem wellfounded_recursive_fcn.100: (FORALL u, v | (Ord(u) & Ord(v) & (orden(u) /= s) & arg1_bef_arg2(orden(u),orden(v))) •imp (u in v)) & (EXISTS o in next(#pow(s)) | (Ord(o) & (s = {orden(x): x in o}) & (FORALL x in o | (orden(x) /= s)) & one_1_map({[x,orden(x)]: x in o})))
(500) Theorem wellfounded_recursive_fcn.100a: (EXISTS o | (Ord(o) & (s = {orden(x): x in o}) & (FORALL x in o | (orden(x) /= s)) & one_1_map({[x,orden(x)]: x in o})))
(500+) Theorem wellfounded_recursive_fcn.101: (Ord(o) & (s = {orden(x): x in o}) & (FORALL x in o | (orden(x) /= s)) & one_1_map({[x,orden(x)]: x in o}))
(520+) Theorem sigma_theory7: [Sum permutation theorem] (Finite(F) & Svm(F) & one_1_map(G) & (domain(F) = domain(G)) & (range(F) •incin s)) •imp (sigma_thryvar(F) = sigma_thryvar({[y,F~[inv(G)~[y]]]: y in range(G)}))
(900) Theorem 745: (R_SIGMA(0) = R_0) & (FORALL x in OM | (cdr(x) in Re) •imp (R_SIGMA({x}) = cdr(x))) & (FORALL f in OM | (Finite(f) & (range(f) •incin Re)) •imp (R_SIGMA(f) in Re)) & (FORALL f in OM, c in f | (Finite(f) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA(f - {c}) •R_PLUS cdr(c))) & (FORALL f in OM | (Finite(f) & Is_map(f) & (range(f) •incin Re)) •imp (FORALL t | R_SIGMA(f) = R_SIGMA(f •ON (domain(f) * t)) •R_PLUS R_SIGMA(f •ON (domain(f) - t)))) & (FORALL f in OM, g | (Finite(f) & Svm(f) & Svm(g) & (domain(f) = domain(g)) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA({[y,R_SIGMA(f •ON (g •INV_IM {y}))]: y in range(g)}))) & (FORALL f in OM, g | (Finite(f) & Svm(f) & one_1_map(g) & (domain(f) = domain(g)) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA({[y,f~[inv(g)~[y]]]: y in range(g)})))
(901) Theorem 746: (R_SIGMA(0) = R_0) & ((cdr(X) in Re) •imp (R_SIGMA({X}) = cdr(X))) & ((Finite(F) & (range(F) •incin Re)) •imp (R_SIGMA(F) in Re)) & ((Finite(F) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA(F - {c}) •R_PLUS cdr(c))) & ((Finite(F) & Is_map(F) & (range(F) •incin Re)) •imp R_SIGMA(F) = R_SIGMA(F •ON (domain(F) * T)) •R_PLUS R_SIGMA(F •ON (domain(F) - T))) & ((Finite(F) & Svm(F) & Svm(G) & (domain(F) = domain(G)) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA({[y,R_SIGMA(F •ON (G •INV_IM {y}))]: y in range(G)}))) & ((Finite(F) & Svm(F) & one_1_map(G) & (domain(F) = domain(G)) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA({[y,F~[inv(G)~[y]]]: y in range(G)})))