Most Recent Proofs - Metamath Proof Explorer

Most Recent Proofs    These are the 10 (GIF, Unicode) or 100 (GIF, Unicode) most recent proofs in the Metamath Proof Explorer and the Hilbert Space Explorer. The official, cleaned up set.mm database file in the Metamath program download is sometimes several days behind the preproduction set.mm (7MB) or set.mm.bz2 (compressed, 2MB) that corresponds to this page. Email: Norm Megill. Wikis: AsteroidMeta (Recent Changes); Ghestalt (Recent Changes). Mailing list: Google Groups. Syndication: RSS feed (web version) courtesy of Dan Getz (note: the feed URL was changed on 22-Sep-2008).

The standard port 80 is not available for the development site, and some users have reported that the original port 8888 is sometimes blocked. Therefore I added two other ports, 88 and 443. You can discuss this problem here. — Norm 24 Jun 2008

Last updated on 20-Nov-2008 at 2:09 AM ET.

Recent Additions to the Metamath Proof Explorer   Notes (last updated 18-Nov-08 )   News (last updated 24-Aug-08 )

Date	Label	Description
Theorem
20-Nov-2008	rpneg 6076	Either a nonzero real or its negation is a positive real, but not both. Axiom 8 of [Apostol] p. 20.
⊢ ((A ∈ ℝ ⋀ A ≠ 0) → (A ∈ ℝ+ ↔ ¬ -A ∈ ℝ+))
19-Nov-2008	pwne 4507	No set equals its power set.
⊢ (A ∈ B → ℘A ≠ A)
18-Nov-2008	rerpdivcl 6075	Closure law for division of a real by a positive real.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ+) → (A / B) ∈ ℝ)
18-Nov-2008	sbc8g 1966	This is the closest we can get to df-sbc 1949 if we start from dfsbcq 1950 (see its comments).
⊢ (A ∈ B → ([A / x]φ ↔ A ∈ {x∣φ}))
18-Nov-2008	sbc7g 1965	An equivalence for class substitution in the spirit of df-clab 1470. Note that x and A don't have to be distinct.
⊢ (A ∈ B → ([A / x]φ ↔ ∃y(y = A ⋀ [y / x]φ)))
17-Nov-2008	isepic 10774	The predicate "is an epimorphism" when the morphism F belongs to a homset.
⊢ O = dom (id ‘T)    &   ⊢ H = (hom ‘T)    &   ⊢ R = (o ‘T)    ⇒   ⊢ ((T ∈ Cat ⋀ (A ∈ O ⋀ B ∈ O) ⋀ F ∈ (H ‘⟨A, B⟩)) → (F ∈ (Epi ‘T) ↔ ∀c ∈ O ∀g ∈ (H ‘⟨B, c⟩)∀h ∈ (H ‘⟨B, c⟩)((gRF) = (hRF) → g = h)))
17-Nov-2008	usinuniop 10643	If a topology is connected, its underlying set can't be partitioned into two non empty non-overlapping open sets.
⊢ X = ∪J    ⇒   ⊢ (J ∈ Con → ∀x ∈ J ∀y ∈ J ((x ≠ ∅ ⋀ y ≠ ∅ ⋀ (x ∩ y) = ∅) → X ≠ (x ∪ y)))
17-Nov-2008	iscon2 10642	The predicate J is a connected topology .
⊢ (J ∈ Con ↔ (J ∈ Top ⋀ (J ∩ (Clsd ‘J)) = {∅, ∪J}))
17-Nov-2008	iscon 10641	The predicate J is a connected topology .
⊢ (J ∈ Top → (J ∈ Con ↔ (J ∩ (Clsd ‘J)) = {∅, ∪J}))
17-Nov-2008	vri 10523	The properties of a real vector space, which is an abelian group (i.e. the vectors, with the operation of vector addition) accompanied by a scalar multiplication operation on the field of real numbers. The variable W was chosen because V is already used for the universal class.
⊢ G = (1st ‘W)    &   ⊢ S = (2nd ‘W)    &   ⊢ X = ran G    ⇒   ⊢ (W ∈ RVec → (G ∈ Abel ⋀ S:(ℝ × X)–→X ⋀ ∀x ∈ X ((1Sx) = x ⋀ ∀y ∈ ℝ (∀z ∈ X (yS(xGz)) = ((ySx)G(ySz)) ⋀ ∀z ∈ ℝ (((y + z)Sx) = ((ySx)G(zSx)) ⋀ ((y · z)Sx) = (yS(zSx)))))))
17-Nov-2008	vrrel 10522	The class of all real vector spaces is a relation.
⊢ Rel RVec
17-Nov-2008	feq123 10508	Equality theorem for functions.
⊢ ((F = G ⋀ A = C ⋀ B = D) → (F:A–→B ↔ G:C–→D))
17-Nov-2008	twpar2 10507	Two ways to say that A and B partition C (when A and B don't overlap and A is a part of C).
⊢ ((A ⊆ C ⋀ (A ∩ B) = ∅) → ((A ∪ B) = C ↔ (C ∖ A) = B))
17-Nov-2008	ref3w 10506	Two ways to state a relation is reflexive. (Adapted from Tarski.)
⊢ (∀x ∈ ∪∪RxRx ↔ (I ↾ ∪∪R) ⊆ R)
17-Nov-2008	eltids 10505	⟨A, A⟩ belongs to a restriction of the identity class iff A belongs to the restricting class.
⊢ (A ∈ C → (A ∈ B ↔ ⟨A, A⟩ ∈ (I ↾ B)))
16-Nov-2008	divmul2 5729	Relationship between division and multiplication.
⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ (C ∈ ℂ ⋀ C ≠ 0)) → ((A / C) = B ↔ A = (C · B)))
16-Nov-2008	cardsucinf 4861	The cardinality of the successor of an infinite ordinal.
⊢ ((A ∈ On ⋀ ω ⊆ A) → (card ‘suc A) = (card ‘A))
15-Nov-2008	divmul 5727	Relationship between division and multiplication.
⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ (C ∈ ℂ ⋀ C ≠ 0)) → ((A / C) = B ↔ (C · B) = A))
15-Nov-2008	cardsucnn 4842	The cardinality of the successor of a finite ordinal (natural number). This theorem does not hold for infinite ordinals; see cardsucinf 4861.
⊢ (A ∈ ω → (card ‘suc A) = suc (card ‘A))
14-Nov-2008	rpcnne0 6070	A positive real is a nonzero complex number.
⊢ (A ∈ ℝ+ → (A ∈ ℂ ⋀ A ≠ 0))
14-Nov-2008	rprene0 6069	A positive real is a nonzero real number.
⊢ (A ∈ ℝ+ → (A ∈ ℝ ⋀ A ≠ 0))
14-Nov-2008	rpcn 6063	A positive real is a complex number.
⊢ (A ∈ ℝ+ → A ∈ ℂ)
14-Nov-2008	axext4 1467	A bidirectional version of Extensionality. Although this theorem "looks" like it is just a definition of equality, it requires the Axiom of Extensionality for its proof under our axiomatization. See the comments for ax-ext 1464 and df-cleq 1475.
⊢ (x = y ↔ ∀z(z ∈ x ↔ z ∈ y))
13-Nov-2008	rpregt0 6067	A positive real is a positive real number.
⊢ (A ∈ ℝ+ → (A ∈ ℝ ⋀ 0 < A))
12-Nov-2008	modcyc2 6323	The modulo operation is cyclic.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ+ ⋀ N ∈ ℤ) → ((A − (N · B)) mod B) = (A mod B))
12-Nov-2008	elqs 4306	Membership in a quotient set.
⊢ B ∈ V    ⇒   ⊢ (B ∈ (A / R) ↔ ∃x ∈ A B = [x]R)
11-Nov-2008	modfrac 6321	The fractional part of a number is the number modulo 1.
⊢ (A ∈ ℝ → (A mod 1) = (A − (⌊ ‘A)))
10-Nov-2008	modcyc 6322	The modulo operation is cyclic.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ+ ⋀ N ∈ ℤ) → ((A + (N · B)) mod B) = (A mod B))
10-Nov-2008	modval 6320	The value of the modulo operation. The modulo congruence notation of number theory, J≡K( modulo N), can be expressed in our notation as (J mod N) = (K mod N). Definition 1 in Knuth, The Art of Computer Programming, Vol. I (1972), p. 38. Knuth uses "mod" for the operation and "modulo" for the congruence. Unlike Knuth, we restrict the second argument to positive reals to simplify certain theorems. (This also gives us future flexibility to extend it to any one of several different conventions for a zero or negative second argument, should there be an advantage in doing so.)
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ+) → (A mod B) = (A − (B · (⌊ ‘(A / B)))))
10-Nov-2008	eqrdav 1481	Deduce equality of classes from an equivalence of membership that depends on the membership variable.
⊢ ((φ ⋀ x ∈ A) → x ∈ C)    &   ⊢ ((φ ⋀ x ∈ B) → x ∈ C)    &   ⊢ ((φ ⋀ x ∈ C) → (x ∈ A ↔ x ∈ B))    ⇒   ⊢ (φ → A = B)
9-Nov-2008	irrmul 6280	The product of an irrational with a nonzero rational is irrational.
⊢ ((A ∈ (ℝ ∖ ℚ) ⋀ B ∈ ℚ ⋀ B ≠ 0) → (A · B) ∈ (ℝ ∖ ℚ))
8-Nov-2008	indistop 7677	The indiscrete topology on a set A. Part of Example 2 in [Munkres] p. 77. (Contributed by FL, 16-Jul-2006; hypothesis eliminated by Stefan Allan, 6-Nov-2008.)
⊢ {∅, A} ∈ Top
8-Nov-2008	unsnen 4853	Equinumerosity of a set with a new element added.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (¬ B ∈ A → (A ∪ {B}) ≈ suc (card ‘A))
8-Nov-2008	prid2g 2463	An unordered pair contains its second member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
⊢ (B ∈ C → B ∈ {A, B})
8-Nov-2008	prid1g 2462	An unordered pair contains its first member. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by Stefan Allan, 8-Nov-2008.)
⊢ (A ∈ C → A ∈ {A, B})
7-Nov-2008	mulre 6810	A product with a nonzero real multiplier is real iff the multiplicand is real.
⊢ ((A ∈ ℂ ⋀ B ∈ ℝ ⋀ B ≠ 0) → (A ∈ ℝ ↔ (B · A) ∈ ℝ))
7-Nov-2008	qdivcl 6277	Closure of division of rationals.
⊢ ((A ∈ ℚ ⋀ B ∈ ℚ ⋀ B ≠ 0) → (A / B) ∈ ℚ)
5-Nov-2008	quoremnn0ALT 6313	Quotient and remainder of a nonnegative integer divided by a natural number.
⊢ Q = (⌊ ‘(A / B))    &   ⊢ R = (A − (B · Q))    ⇒   ⊢ ((A ∈ ℕ0 ⋀ B ∈ ℕ) → ((Q ∈ ℕ0 ⋀ R ∈ ℕ0) ⋀ (R < B ⋀ A = ((B · Q) + R))))
2-Nov-2008	expnlbnd2 6688	The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound.
⊢ ((A ∈ ℝ+ ⋀ B ∈ ℝ ⋀ 1 < B) → ∃j ∈ ℕ ∀k ∈ ℕ (j ≤ k → (1 / (B↑k)) < A))
2-Nov-2008	jaoa 430	Inference disjoining and conjoining the antecedents of two implications. (Contributed by Stefan Allan, 1-Nov-2008.)
⊢ (φ → (ψ → χ))    &   ⊢ (θ → (τ → χ))    ⇒   ⊢ ((φ ⋁ θ) → ((ψ ⋀ τ) → χ))
1-Nov-2008	iooshf 6364	Shift the arguments of the open interval function.
⊢ (((A ∈ ℝ ⋀ B ∈ ℝ) ⋀ (C ∈ ℝ ⋀ D ∈ ℝ)) → ((A − B) ∈ (C(,)D) ↔ A ∈ ((C + B)(,)(D + B))))
31-Oct-2008	mpgbir 992	Modus ponens on biconditional combined with generalization. (The proof was shortened by Stefan Allan, 28-Oct-2008.)
⊢ (φ ↔ ∀xψ)    &   ⊢ ψ    ⇒   ⊢ φ
31-Oct-2008	mpgbi 991	Modus ponens on biconditional combined with generalization. (The proof was shortened by Stefan Allan, 28-Oct-2008.)
⊢ (∀xφ ↔ ψ)    &   ⊢ φ    ⇒   ⊢ ψ
22-Oct-2008	zdivmul 6223	Property of divisibility: if D divides A then it divides B · A.
⊢ (((D ∈ ℕ ⋀ A ∈ ℤ ⋀ B ∈ ℤ) ⋀ (A / D) ∈ ℤ) → ((B · A) / D) ∈ ℤ)
20-Oct-2008	quoremnn0 6314	Quotient and remainder of a nonnegative integer divided by a natural number.
⊢ Q = (⌊ ‘(A / B))    &   ⊢ R = (A − (B · Q))    ⇒   ⊢ ((A ∈ ℕ0 ⋀ B ∈ ℕ) → ((Q ∈ ℕ0 ⋀ R ∈ ℕ0) ⋀ (R < B ⋀ A = ((B · Q) + R))))
19-Oct-2008	ledivmul2 5886	'Less than or equal to' relationship between division and multiplication.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ ⋀ (C ∈ ℝ ⋀ 0 < C)) → ((A / C) ≤ B ↔ A ≤ (B · C)))
17-Oct-2008	zdivadd 6222	Property of divisibility: if D divides A and B then it divides A + B.
⊢ (((D ∈ ℕ ⋀ A ∈ ℤ ⋀ B ∈ ℤ) ⋀ ((A / D) ∈ ℤ ⋀ (B / D) ∈ ℤ)) → ((A + B) / D) ∈ ℤ)
16-Oct-2008	ledivmul 5881	'Less than or equal to' relationship between division and multiplication.
⊢ ((A ∈ ℝ ⋀ B ∈ ℝ ⋀ (C ∈ ℝ ⋀ 0 < C)) → ((A / C) ≤ B ↔ A ≤ (C · B)))
14-Oct-2008	iunfi 4584	The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This is the indexed union version of unifi 4573. Note that B depends on x, i.e. can be thought of as B(x).
⊢ ((A ∈ Fin ⋀ ∀x ∈ A B ∈ Fin) → ∪x ∈ A B ∈ Fin)
14-Oct-2008	fofi 4583	If a function has a finite domain, its range is finite. Theorem 37 of [Suppes] p. 104.
⊢ ((A ∈ Fin ⋀ F:A–onto→B) → B ∈ Fin)
12-Oct-2008	divass 5758	An associative law for division.
⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ (C ∈ ℂ ⋀ C ≠ 0)) → ((A · B) / C) = (A · (B / C)))
11-Oct-2008	abfii5 4580	Two ways to express the collection of finite intersections of a set A.
⊢ A ∈ V    ⇒   ⊢ ∩{x∣(A ⊆ x ⋀ ∀y ∈ x ∀z ∈ x (y ∩ z) ∈ x)} = {x∣∃y(y ⊆ A ⋀ y ∈ Fin ⋀ x = ∩y)}
10-Oct-2008	fipr 4452	The class of finite sets is a proper class. (Contributed by Jeffrey Hankins, 10-Oct-2008.)
⊢ Fin ∉ V
10-Oct-2008	fiprlem 4451	Lemma for fipr 4452.
⊢ A = {x∣x ≈ 1o}    &   ⊢ F = {⟨x, y⟩∣(x ∈ A ⋀ y = ∪x)}    ⇒   ⊢ F:A–onto→V
9-Oct-2008	om2uzisoi 6503	G (see om2uz0i 6496) is an isomorphism from natural ordinals to upper integers.
⊢ C ∈ ℤ    &   ⊢ G = (rec({⟨x, y⟩∣y = (x + 1)}, C) ↾ ω)    ⇒   ⊢ G Isom E, < (ω, {z ∈ ℤ∣C ≤ z})
8-Oct-2008	fodomfib 4582	Equivalence of an onto mapping and dominance for a non-empty finite set. Unlike fodomb 4817 for arbitrary sets, this theorem does not require the Axiom of Choice for its proof.
⊢ (A ∈ Fin → ((A ≠ ∅ ⋀ ∃f f:A–onto→B) ↔ (∅ ≺ B ⋀ B ≼ A)))
7-Oct-2008	iepiclem 10773	Lemma for isepic 10774.
⊢ O = dom (id ‘T)    &   ⊢ H = (hom ‘T)    &   ⊢ R = (o ‘T)    ⇒   ⊢ ((T ∈ Cat ⋀ (A ∈ O ⋀ B ∈ O) ⋀ F ∈ (H ‘⟨A, B⟩)) → (∀c ∈ O ∀g ∈ (H ‘⟨B, c⟩)∀h ∈ (H ‘⟨B, c⟩)((gRF) = (hRF) → g = h) → (F ∈ dom (dom ‘T) ⋀ ∀g ∈ dom (dom ‘T)∀h ∈ dom (dom ‘T)((((cod ‘T) ‘g) = ((cod ‘T) ‘h) ⋀ ((dom ‘T) ‘g) = ((cod ‘T) ‘F) ⋀ ((dom ‘T) ‘h) = ((cod ‘T) ‘F)) → ((gRF) = (hRF) → g = h)))))
7-Oct-2008	empos 10519	The empty set is a poset.
⊢ ∅ ∈ Poset
7-Oct-2008	int2rel 10504	The intersection of two relations is equivalent to a conjunction of those relations.
⊢ (A(R ∩ S)B ↔ (ARB ⋀ ASB))
7-Oct-2008	domintref 10503	The domain of the intersection of two reflexive relations is the intersection of their domains. Compare with dmin 3334.
⊢ (((Rel R ⋀ ∀x ∈ ∪∪RxRx) ⋀ (Rel S ⋀ ∀x ∈ ∪∪SxSx)) → dom ( R ∩ S) = (dom R ∩ dom S))
7-Oct-2008	domintreflem 10502	Lemma for domintref 10503.
⊢ A ∈ V    ⇒   ⊢ ((Rel R ⋀ ∀x ∈ ∪∪RxRx) → (A ∈ dom R ↔ ⟨A, A⟩ ∈ R))
7-Oct-2008	domfldref 10501	The domain of a reflexive relation is equal to its field .
⊢ ((Rel R ⋀ ∀x ∈ ∪∪RxRx) → dom R = ∪∪R)
7-Oct-2008	domrngref 10500	Domain and range of a reflexive relation are equal.
⊢ ((Rel R ⋀ ∀x ∈ ∪∪RxRx) → dom R = ran R)
7-Oct-2008	intres 10499	Intersection of restricted classes.
⊢ ((C ↾ A) ∩ (C ↾ B)) = (C ↾ (A ∩ B))
6-Oct-2008	cbvcsbv 2014	Change the bound variable of a proper substitution into a class using implicit substitution.
⊢ (x = y → B = C)    ⇒   ⊢ (A ∈ D → [A / x]B = [A / y]C)
5-Oct-2008	abfii4 4579	Two ways to express the collection of finite intersections of a set A. Even though the expressions differ by only one symbol, the proof is not simple.
⊢ A ∈ V    ⇒   ⊢ ∩{x∣(A ⊆ x ⋀ ∀y((y ⊆ x ⋀ y ≠ ∅ ⋀ y ∈ Fin) → ∩y ∈ x))} = ∩{x∣(A ⊆ x ⋀ ∀y((y ⊆ A ⋀ y ≠ ∅ ⋀ y ∈ Fin) → ∩y ∈ x))}
4-Oct-2008	ruALT 4617	Alternate proof of Russell's Paradox ru 1945, simplified using (indirectly) the Axiom of Regularity ax-reg 4608. (Contributed by Alan Sare, 4-Oct-2008.)
⊢ {x∣x ∉ x} ∉ V
4-Oct-2008	ruv 4616	The Russell class is equal to the universe V. Exercise 5 of [TakeutiZaring] p. 22. (Contributed by Alan Sare, 4-Oct-2008.)
⊢ {x∣x ∉ x} = V
4-Oct-2008	ru 1945	Russell's Paradox. Proposition 4.14 of [TakeutiZaring] p. 14. Frege's Axiom of (unrestricted) Comprehension, expressed in our notation as A ∈ V, asserted that any collection of sets A is a set i.e. belongs to the universe V of all sets. In particular, by substituting {x∣x ∉ x} (the "Russell class") for A, it asserted {x∣x ∉ x} ∈ V, meaning that the "collection of all sets which are not members of themselves" is a set. However, here we prove {x∣x ∉ x} ∉ V. This contradiction was discovered by Russell in 1901 (published in 1903), invalidating Comprehension and leading to the collapse of Frege's system. In 1908 Zermelo rectified this fatal flaw by replacing Comprehension with a weaker Subset (or Separation) Axiom ssex 2734 asserting that A is a set only when it is smaller than some other set B. However, Zermelo was then faced with a "chicken and egg" problem of how to show B is a set, leading him to introduce the set-building axioms of Null Set 0ex 2726, Pairing prex 2797, Union uniex 2886, Power Set pwex 2761, and Infinity omex 4644 to give him some starting sets to work with (all of which, before Russell's Paradox, were immediate consequences of Frege's Comprehension). In 1922 Fraenkel strengthened the Subset Axiom with our present Replacement Axiom funimaex 3592 (whose modern formalization is due to Skolem, also in 1922). Thus in a very real sense Russell's Paradox spawned the invention of ZF set theory and completely revised the foundations of mathematics! Another mainstream formalization of set theory, devised by von Neumann, Bernays, and Goedel, uses class variables rather than set variables as its primitives. The axiom system NBG in [Mendelson] p. 225 is suitable for a Metamath encoding. NBG is a conservative extension of ZF in that it proves exactly the same theorems as ZF that are expressible in the language of ZF. An advantage of NBG is that it is finitely axiomatizable - the Axiom of Replacement can be broken down into a finite set of formulas that eliminate its wff metavariable. Finite axiomatizability is required by some proof languages (although not by Metamath). There is a stronger version of NBG called Morse-Kelley (axiom system MK in [Mendelson] p. 287). Russell himself continued in a different direction, avoiding the paradox with his "theory of types." Quine extended Russell's ideas to formulate the very strong New Foundations set theory (axiom system NF of [Quine] p. 331). In NF, the collection of all sets is a set, contradicting ZF and NBG set theories, and it has other bizarre consequences: when sets become too huge (beyond the size of those used in standard mathematics), the Axiom of Choice ac4 4767 and Cantor's Theorem canth 3923 are provably false! (See ncanth 3924 for some intuition behind the latter.) Nonetheless, NF has not been shown to be inconsistent and has its advocates - who's to say which set theory is "right"? NF is finitely axiomatizable and can be encoded in Metamath using the axioms from T. Hailperin, "A set of axioms for logic," J. Symb. Logic 9:1-19 (1944). Under our ZF set theory, every set is a member of the Russell class by elirrv 4613 (derived from the Axiom of Regularity), so for us the Russell class equals the universe V (theorem ruv 4616). See ruALT 4617 for an alternate proof of ru 1945 derived from that fact.
⊢ {x∣x ∉ x} ∉ V
3-Oct-2008	zdiv 6221	Two ways to express "M divides N.
⊢ ((M ∈ ℕ ⋀ N ∈ ℤ) → (∃k ∈ ℤ (M · k) = N ↔ (N / M) ∈ ℤ))
3-Oct-2008	xordi 678	Conjunction distributes over exclusive-or, using ¬ (φ ↔ ψ) to express exclusive-or. This is one way to interpret the distributive law of multiplication over addition in mod 2 arithmetic.
⊢ ((φ ⋀ ¬ (ψ ↔ χ)) ↔ ¬ ((φ ⋀ ψ) ↔ (φ ⋀ χ)))
2-Oct-2008	abfii3 4578	Two ways to express the collection of finite intersections of a set A.
⊢ A ∈ V    ⇒   ⊢ ∩{x∣(A ⊆ x ⋀ ∀y((y ⊆ A ⋀ y ≠ ∅ ⋀ y ∈ Fin) → ∩y ∈ x))} = ∩{x∣∀y((y ⊆ A ⋀ y ≠ ∅ ⋀ y ∈ Fin) → ∩y ∈ x)}
1-Oct-2008	abfii2 4577	Two ways to express the collection of finite intersections of a set A.
⊢ A ∈ V    ⇒   ⊢ {x∣∃y(y ⊆ A ⋀ y ∈ Fin ⋀ x = ∩y)} = ∩{x∣∀y((y ⊆ A ⋀ y ≠ ∅ ⋀ y ∈ Fin) → ∩y ∈ x)}
30-Sep-2008	cbvsbcv 1967	Change the bound variable of a class substitution using implicit substitution.
⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (A ∈ B → ([A / x]φ ↔ [A / y]ψ))
29-Sep-2008	abfii1 4576	Two ways to express the collection of finite intersections of a set A.
⊢ ∩{x∣(A ⊆ x ⋀ ∀y ∈ x ∀z ∈ x (y ∩ z) ∈ x)} = ∩{x∣(A ⊆ x ⋀ ∀y((y ⊆ x ⋀ y ≠ ∅ ⋀ y ∈ Fin) → ∩y ∈ x))}
28-Sep-2008	unifi2 4574	The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144. This version of unifi 4573 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 4565).
⊢ ((A ≺ ω ⋀ ∀x ∈ A x ≺ ω) → ∪A ≺ ω)
27-Sep-2008	0leopj 10139	A projector is a positive operator.
⊢ (T ∈ ran proj → 0hop ≤op T)
26-Sep-2008	unifi 4573	The finite union of finite sets is finite. Exercise 13 of [Enderton] p. 144.
⊢ ((A ∈ Fin ⋀ ∀x ∈ A x ∈ Fin) → ∪A ∈ Fin)
25-Sep-2008	onfin 4539	An ordinal number is finite iff it is a natural number. Proposition 10.32 of [TakeutiZaring] p. 92.
⊢ (A ∈ On → (A ∈ Fin ↔ A ∈ ω))
24-Sep-2008	eupicka 1439	Version of eupick 1438 with closed formulas.
⊢ ((∃!xφ ⋀ ∃x(φ ⋀ ψ)) → ∀x(φ → ψ))
23-Sep-2008	inposet 10518	Inclusion partially orders any set.
⊢ C = {⟨x, y⟩∣x ⊆ y}    ⇒   ⊢ (A ∈ B → (C ∩ (A × A)) ∈ Poset)
23-Sep-2008	inpc 10517	Inclusion is a proper class.
⊢ C = {⟨x, y⟩∣x ⊆ y}    ⇒   ⊢ ¬ C ∈ V
23-Sep-2008	inposetlem 10516	Lemma for inposet 10518. Definition of inclusion of sets using a class.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ C = {⟨x, y⟩∣x ⊆ y}    ⇒   ⊢ (ACB ↔ A ⊆ B)
23-Sep-2008	vxveqv 10498	A theorem about things which don't exist V and (V × V).
⊢ (V × V) ≠ V
22-Sep-2008	dominf 4924	A nonempty set that is a subset of its union is infinite.
⊢ A ∈ V    ⇒   ⊢ ((A ≠ ∅ ⋀ A ⊆ ∪A) → ω ≼ A)
22-Sep-2008	isfinite 4651	A set is strictly dominated by the class of natural numbers iff it is finite. Theorem 42 of [Suppes] p. 151. This theorem provides two equivalent ways to express "A is finite." The Axiom of Infinity is used for the reverse implication.
⊢ (A ≺ ω ↔ A ∈ Fin)
20-Sep-2008	pwfi 4586	The power set of a finite set is finite and vice-versa. Theorem 38 of [Suppes] p. 104 and its converse, Theorem 40 of [Suppes] p. 105.
⊢ (A ∈ Fin ↔ ℘A ∈ Fin)
19-Sep-2008	pwfilem 4585	Lemma for pwfi 4586.
⊢ F = {⟨c, y⟩∣(c ∈ ℘b ⋀ y = (c ∪ {x}))}    ⇒   ⊢ (℘b ∈ Fin → ℘(b ∪ {x}) ∈ Fin)
18-Sep-2008	domfi 4557	A set dominated by a finite set is finite.
⊢ ((A ∈ Fin ⋀ B ≼ A) → B ∈ Fin)
17-Sep-2008	fodomfi 4581	An onto function implies dominance of domain over range, for finite sets. Unlike fodom 4815 for arbitrary sets, this theorem does not require the Axiom of Choice for its proof.
⊢ ((A ∈ Fin ⋀ F:A–onto→B) → B ≼ A)
16-Sep-2008	unctb 7611	The union of two countable sets is countable. (Contributed by FL, 25-Aug-2006.)
⊢ ((A ≼ ω ⋀ B ≼ ω) → (A ∪ B) ≼ ω)
15-Sep-2008	unfi2 4570	The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. This version of unfi 4569 is useful only if we assume the Axiom of Infinity (see comments in fin2inf 4565).
⊢ ((A ≺ ω ⋀ B ≺ ω) → (A ∪ B) ≺ ω)
14-Sep-2008	isfinite1 4550	Omega strictly dominates a finite set. See comment in omsdomnn 4549.
⊢ (A ∈ Fin → (