P. 455 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 45401-45500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ssabso 45401*	The notion "𝑥 is a subset of 𝑦 " is absolute for transitive models. Compare Example I.16.3 of [Kunen2] p. 96 and the following discussion. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ ((Tr 𝑀 ∧ 𝐴 ∈ 𝑀) → (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)))
Theorem	disjabso 45402*	Disjointness is absolute for transitive models. Compare Example I.16.3 of [Kunen2] p. 96 and the following discussion. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ ((Tr 𝑀 ∧ 𝐴 ∈ 𝑀) → ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)))
Theorem	n0abso 45403*	Nonemptiness is absolute for transitive models. Compare Example I.16.3 of [Kunen2] p. 96 and the following discussion. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ ((Tr 𝑀 ∧ 𝐴 ∈ 𝑀) → (𝐴 ≠ ∅ ↔ ∃𝑥 ∈ 𝑀 𝑥 ∈ 𝐴))
21.42.7  Lemmas for showing axioms hold in models
Theorem	traxext 45404*	A transitive class models the Axiom of Extensionality ax-ext 2709. Lemma II.2.4(1) of [Kunen2] p. 111. (Contributed by Eric Schmidt, 11-Sep-2025.)
⊢ (Tr 𝑀 → ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦))
Theorem	modelaxreplem1 45405*	Lemma for modelaxrep 45408. We show that 𝑀 is closed under taking subsets. (Contributed by Eric Schmidt, 29-Sep-2025.)
⊢ (𝜓 → 𝑥 ⊆ 𝑀)    &   ⊢ (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀))    &   ⊢ (𝜓 → ∅ ∈ 𝑀)    &   ⊢ (𝜓 → 𝑥 ∈ 𝑀)    &   ⊢ 𝐴 ⊆ 𝑥    ⇒   ⊢ (𝜓 → 𝐴 ∈ 𝑀)
Theorem	modelaxreplem2 45406*	Lemma for modelaxrep 45408. We define a class 𝐹 and show that the antecedent of Replacement implies that 𝐹 is a function. We use Replacement (in the form of funex 7174) to show that 𝐹 exists. Then we show that, under our hypotheses, the range of 𝐹 is a member of 𝑀. (Contributed by Eric Schmidt, 29-Sep-2025.)
⊢ (𝜓 → 𝑥 ⊆ 𝑀)    &   ⊢ (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀))    &   ⊢ (𝜓 → ∅ ∈ 𝑀)    &   ⊢ (𝜓 → 𝑥 ∈ 𝑀)    &   ⊢ Ⅎ𝑤𝜓    &   ⊢ Ⅎ𝑧𝜓    &   ⊢ Ⅎ𝑧𝐹    &   ⊢ 𝐹 = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))}    &   ⊢ (𝜓 → (𝑤 ∈ 𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)))    ⇒   ⊢ (𝜓 → ran 𝐹 ∈ 𝑀)
Theorem	modelaxreplem3 45407*	Lemma for modelaxrep 45408. We show that the consequent of Replacement is satisfied with ran 𝐹 as the value of 𝑦. (Contributed by Eric Schmidt, 29-Sep-2025.)
⊢ (𝜓 → 𝑥 ⊆ 𝑀)    &   ⊢ (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀))    &   ⊢ (𝜓 → ∅ ∈ 𝑀)    &   ⊢ (𝜓 → 𝑥 ∈ 𝑀)    &   ⊢ Ⅎ𝑤𝜓    &   ⊢ Ⅎ𝑧𝜓    &   ⊢ Ⅎ𝑧𝐹    &   ⊢ 𝐹 = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))}    &   ⊢ (𝜓 → (𝑤 ∈ 𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)))    ⇒   ⊢ (𝜓 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)))
Theorem	modelaxrep 45408*	Conditions which guarantee that a class models the Axiom of Replacement ax-rep 5213. Similar to Lemma II.2.4(6) of [Kunen2] p. 111. The first two hypotheses are those in Kunen. The reason for the third hypothesis that our version of Replacement is different from Kunen's (which is zfrep6 5225). If we assumed Regularity, we could eliminate this extra hypothesis, since under Regularity, the empty set is a member of every non-empty transitive class. Note that, to obtain the relativization of an instance of Replacement to 𝑀, the formula ∀𝑦𝜑 would need to be replaced with ∀𝑦 ∈ 𝑀𝜒, where 𝜒 is 𝜑 with all quantifiers relativized to 𝑀. However, we can obtain this by using 𝑦 ∈ 𝑀 ∧ 𝜒 for 𝜑 in this theorem, so it does establish that all instances of Replacement hold in 𝑀. (Contributed by Eric Schmidt, 29-Sep-2025.)
⊢ (𝜓 → Tr 𝑀)    &   ⊢ (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀))    &   ⊢ (𝜓 → ∅ ∈ 𝑀)    ⇒   ⊢ (𝜓 → ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))))
Theorem	ssclaxsep 45409*	A class that is closed under subsets models the Axiom of Separation ax-sep 5232. Lemma II.2.4(3) of [Kunen2] p. 111. Note that, to obtain the relativization of an instance of Separation to 𝑀, the formula 𝜑 would need to be replaced with its relativization to 𝑀. However, this new formula is a valid substitution for 𝜑, so this theorem does establish that all instances of Separation hold in 𝑀. (Contributed by Eric Schmidt, 29-Sep-2025.)
⊢ (∀𝑧 ∈ 𝑀 𝒫 𝑧 ⊆ 𝑀 → ∀𝑧 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))
Theorem	0elaxnul 45410*	A class that contains the empty set models the Null Set Axiom ax-nul 5242. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ (∅ ∈ 𝑀 → ∃𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ¬ 𝑦 ∈ 𝑥)
Theorem	pwclaxpow 45411*	Suppose 𝑀 is a transitive class that is closed under power sets intersected with 𝑀. Then, 𝑀 models the Axiom of Power Sets ax-pow 5308. One direction of Lemma II.2.8 of [Kunen2] p. 113. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ ((Tr 𝑀 ∧ ∀𝑥 ∈ 𝑀 (𝒫 𝑥 ∩ 𝑀) ∈ 𝑀) → ∀𝑥 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
Theorem	prclaxpr 45412*	A class that is closed under the pairing operation models the Axiom of Pairing ax-pr 5376. Lemma II.2.4(4) of [Kunen2] p. 111. (Contributed by Eric Schmidt, 29-Sep-2025.)
⊢ (∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 {𝑥, 𝑦} ∈ 𝑀 → ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∃𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧))
Theorem	uniclaxun 45413*	A class that is closed under the union operation models the Axiom of Union ax-un 7689. Lemma II.2.4(5) of [Kunen2] p. 111. (Contributed by Eric Schmidt, 1-Oct-2025.)
⊢ (∀𝑥 ∈ 𝑀 ∪ 𝑥 ∈ 𝑀 → ∀𝑥 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
Theorem	sswfaxreg 45414*	A subclass of the class of well-founded sets models the Axiom of Regularity ax-reg 9507. Lemma II.2.4(2) of [Kunen2] p. 111. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ (𝑀 ⊆ ∪ (𝑅1 “ On) → ∀𝑥 ∈ 𝑀 (∃𝑦 ∈ 𝑀 𝑦 ∈ 𝑥 → ∃𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥))))
Theorem	omssaxinf2 45415*	A class that contains all ordinals up to and including ω models the Axiom of Infinity ax-inf2 9562. The antecedent of this theorem is not enough to guarantee that the class models the alternate axiom ax-inf 9559. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ ((ω ⊆ 𝑀 ∧ ω ∈ 𝑀) → ∃𝑥 ∈ 𝑀 (∃𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑀 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))))
Theorem	omelaxinf2 45416*	A transitive class that contains ω models the Axiom of Infinity ax-inf2 9562. Lemma II.2.11(7) of [Kunen2] p. 114. Kunen has the additional hypotheses that the Extensionality, Separation, Pairing, and Union axioms are true in 𝑀. This, apparently, is because Kunen's statement of the Axiom of Infinity uses the defined notions ∅ and suc, and these axioms guarantee that these notions are well-defined. When we state the axiom using primitives only, the need for these hypotheses disappears. The antecedent of this theorem is not enough to guarantee that the class models the alternate axiom ax-inf 9559. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ ((Tr 𝑀 ∧ ω ∈ 𝑀) → ∃𝑥 ∈ 𝑀 (∃𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑀 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))))
Theorem	dfac5prim 45417*	dfac5 10051 expanded into primitives. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ (CHOICE ↔ ∀𝑥((∀𝑧(𝑧 ∈ 𝑥 → ∃𝑤 𝑤 ∈ 𝑧) ∧ ∀𝑧∀𝑤((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦(𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑥 → ∃𝑤∀𝑣((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))))
Theorem	ac8prim 45418*	ac8 10414 expanded into primitives. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ ((∀𝑧(𝑧 ∈ 𝑥 → ∃𝑤 𝑤 ∈ 𝑧) ∧ ∀𝑧∀𝑤((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦(𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑥 → ∃𝑤∀𝑣((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))
Theorem	modelac8prim 45419*	If 𝑀 is a transitive class, then the following are equivalent. (1) Every nonempty set 𝑥 ∈ 𝑀 of pairwise disjoint nonempty sets has a choice set in 𝑀. (2) The class 𝑀 models the Axiom of Choice, in the form ac8prim 45418. Lemma II.2.11(7) of [Kunen2] p. 114. Kunen has the additional hypotheses that the Extensionality, Separation, Pairing, and Union axioms are true in 𝑀. This, apparently, is because Kunen's statement of the Axiom of Choice uses defined notions, including ∅ and ∩, and these axioms guarantee that these notions are well-defined. When we state the axiom using primitives only, the need for these hypotheses disappears. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ (Tr 𝑀 → (∀𝑥 ∈ 𝑀 ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ∀𝑥 ∈ 𝑀 ((∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))))
21.42.8  The class of well-founded sets is a model for ZFC
Theorem	wfaxext 45420*	The class of well-founded sets models the Axiom of Extensionality ax-ext 2709. Part of Corollary II.2.5 of [Kunen2] p. 112. This is the first of a series of theorems showing that all the axioms of ZFC hold in the class of well-founded sets, which we here denote by 𝑊. More precisely, for each axiom of ZFC, we obtain a provable statement if we restrict all quantifiers to 𝑊 (including implicit universal quantifiers on free variables). None of these proofs use the Axiom of Regularity. In particular, the Axiom of Regularity itself is proved to hold in 𝑊 without using Regularity. Further, the Axiom of Choice is used only in the proof that Choice holds in 𝑊. This has the consequence that any theorem of ZF (possibly proved using Regularity) can be proved, without using Regularity, to hold in 𝑊. This gives us a relative consistency result: If ZF without Regularity is consistent, so is ZF itself. Similarly, if ZFC without Regularity is consistent, so is ZFC itself. These consistency results are metatheorems and are part of Theorem II.2.13 of [Kunen2] p. 114. (Contributed by Eric Schmidt, 11-Sep-2025.) (Revised by Eric Schmidt, 29-Sep-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 (∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)
Theorem	wfaxrep 45421*	The class of well-founded sets models the Axiom of Replacement ax-rep 5213. Actually, our statement is stronger, since it is an instance of Replacement only when all quantifiers in ∀𝑦𝜑 are relativized to 𝑊. Essentially part of Corollary II.2.5 of [Kunen2] p. 112, but note that our Replacement is different from Kunen's. (Contributed by Eric Schmidt, 29-Sep-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 (∀𝑤 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑊 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)))
Theorem	wfaxsep 45422*	The class of well-founded sets models the Axiom of Separation ax-sep 5232. Actually, our statement is stronger, since it is an instance of Separation only when all quantifiers in 𝜑 are relativized to 𝑊. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 29-Sep-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∀𝑧 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑥 ∈ 𝑊 (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))
Theorem	wfaxnul 45423*	The class of well-founded sets models the Null Set Axiom ax-nul 5242. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∃𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 ¬ 𝑦 ∈ 𝑥
Theorem	wfaxpow 45424*	The class of well-founded sets models the Axioms of Power Sets. Part of Corollary II.2.9 of [Kunen2] p. 113. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (∀𝑤 ∈ 𝑊 (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	wfaxpr 45425*	The class of well-founded sets models the Axiom of Pairing ax-pr 5376. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 29-Sep-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 ∃𝑧 ∈ 𝑊 ∀𝑤 ∈ 𝑊 ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)
Theorem	wfaxun 45426*	The class of well-founded sets models the Axiom of Union ax-un 7689. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (∃𝑤 ∈ 𝑊 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	wfaxreg 45427*	The class of well-founded sets models the Axiom of Regularity ax-reg 9507. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 (∃𝑦 ∈ 𝑊 𝑦 ∈ 𝑥 → ∃𝑦 ∈ 𝑊 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)))
Theorem	wfaxinf2 45428*	The class of well-founded sets models the Axiom of Infinity ax-inf2 9562. Part of Corollary II.2.12 of [Kunen2] p. 114. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∃𝑥 ∈ 𝑊 (∃𝑦 ∈ 𝑊 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑊 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑊 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑊 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))))
Theorem	wfac8prim 45429*	The class of well-founded sets 𝑊 models the Axiom of Choice. Since the previous theorems show that all the ZF axioms hold in 𝑊, we may use any statement that ZF proves is equivalent to Choice to prove this. We use ac8prim 45418. Part of Corollary II.2.12 of [Kunen2] p. 114. (Contributed by Eric Schmidt, 19-Oct-2025.)
⊢ 𝑊 = ∪ (𝑅1 “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ((∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑊 ∀𝑤 ∈ 𝑊 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑊 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 ∀𝑣 ∈ 𝑊 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))
21.42.9  Permutation models
Theorem	brpermmodel 45430	The membership relation in a permutation model. We use a permutation 𝐹 of the universe to define a relation 𝑅 that serves as the membership relation in our model. The conclusion of this theorem is Definition II.9.1 of [Kunen2] p. 148. All the axioms of ZFC except for Regularity hold in permutation models, and Regularity will be false if 𝐹 is chosen appropriately. Thus, permutation models can be used to show that Regularity does not follow from the other axioms (with the usual proviso that the axioms are consistent). (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴𝑅𝐵 ↔ 𝐴 ∈ (𝐹‘𝐵))
Theorem	brpermmodelcnv 45431	Ordinary membership expressed in terms of the permutation model's membership relation. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴𝑅(◡𝐹‘𝐵) ↔ 𝐴 ∈ 𝐵)
Theorem	permaxext 45432*	The Axiom of Extensionality ax-ext 2709 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ (∀𝑧(𝑧𝑅𝑥 ↔ 𝑧𝑅𝑦) → 𝑥 = 𝑦)
Theorem	permaxrep 45433*	The Axiom of Replacement ax-rep 5213 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. Note that, to prove that an instance of Replacement holds in the model, 𝜑 would need have all instances of ∈ replaced with 𝑅. But this still results in an instance of this theorem, so we do establish that Replacement holds. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧𝑅𝑦 ↔ ∃𝑤(𝑤𝑅𝑥 ∧ ∀𝑦𝜑)))
Theorem	permaxsep 45434*	The Axiom of Separation ax-sep 5232 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. Note that, to prove that an instance of Separation holds in the model, 𝜑 would need have all instances of ∈ replaced with 𝑅. But this still results in an instance of this theorem, so we do establish that Separation holds. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ ∃𝑦∀𝑥(𝑥𝑅𝑦 ↔ (𝑥𝑅𝑧 ∧ 𝜑))
Theorem	permaxnul 45435*	The Null Set Axiom ax-nul 5242 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ ∃𝑥∀𝑦 ¬ 𝑦𝑅𝑥
Theorem	permaxpow 45436*	The Axiom of Power Sets ax-pow 5308 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ ∃𝑦∀𝑧(∀𝑤(𝑤𝑅𝑧 → 𝑤𝑅𝑥) → 𝑧𝑅𝑦)
Theorem	permaxpr 45437*	The Axiom of Pairing ax-pr 5376 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤𝑅𝑧)
Theorem	permaxun 45438*	The Axiom of Union ax-un 7689 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ ∃𝑦∀𝑧(∃𝑤(𝑧𝑅𝑤 ∧ 𝑤𝑅𝑥) → 𝑧𝑅𝑦)
Theorem	permaxinf2lem 45439*	Lemma for permaxinf2 45440. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    &   ⊢ 𝑍 = (rec((𝑣 ∈ V ↦ (◡𝐹‘((𝐹‘𝑣) ∪ {𝑣}))), (◡𝐹‘∅)) “ ω)    ⇒   ⊢ ∃𝑥(∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧 ¬ 𝑧𝑅𝑦) ∧ ∀𝑦(𝑦𝑅𝑥 → ∃𝑧(𝑧𝑅𝑥 ∧ ∀𝑤(𝑤𝑅𝑧 ↔ (𝑤𝑅𝑦 ∨ 𝑤 = 𝑦)))))
Theorem	permaxinf2 45440*	The Axiom of Infinity ax-inf2 9562 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. (Contributed by Eric Schmidt, 6-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ ∃𝑥(∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧 ¬ 𝑧𝑅𝑦) ∧ ∀𝑦(𝑦𝑅𝑥 → ∃𝑧(𝑧𝑅𝑥 ∧ ∀𝑤(𝑤𝑅𝑧 ↔ (𝑤𝑅𝑦 ∨ 𝑤 = 𝑦)))))
Theorem	permac8prim 45441*	The Axiom of Choice ac8prim 45418 holds in permutation models. Part of Exercise II.9.3 of [Kunen2] p. 149. Note that ax-ac 10381 requires Regularity for its derivation from the usual Axiom of Choice and does not necessarily hold in permutation models. (Contributed by Eric Schmidt, 16-Nov-2025.)
⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ ((∀𝑧(𝑧𝑅𝑥 → ∃𝑤 𝑤𝑅𝑧) ∧ ∀𝑧∀𝑤((𝑧𝑅𝑥 ∧ 𝑤𝑅𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦(𝑦𝑅𝑧 → ¬ 𝑦𝑅𝑤)))) → ∃𝑦∀𝑧(𝑧𝑅𝑥 → ∃𝑤∀𝑣((𝑣𝑅𝑧 ∧ 𝑣𝑅𝑦) ↔ 𝑣 = 𝑤)))
Theorem	nregmodelf1o 45442	Define a permutation 𝐹 used to produce a model in which ax-reg 9507 is false. The permutation swaps ∅ and {∅} and leaves the rest of 𝑉 fixed. This is an example given after Exercise II.9.2 of [Kunen2] p. 148. (Contributed by Eric Schmidt, 16-Nov-2025.)
⊢ 𝐹 = (( I ↾ (V ∖ {∅, {∅}})) ∪ {⟨∅, {∅}⟩, ⟨{∅}, ∅⟩})    ⇒   ⊢ 𝐹:V–1-1-onto→V
Theorem	nregmodellem 45443	Lemma for nregmodel 45444. (Contributed by Eric Schmidt, 16-Nov-2025.)
⊢ 𝐹 = (( I ↾ (V ∖ {∅, {∅}})) ∪ {⟨∅, {∅}⟩, ⟨{∅}, ∅⟩})    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ (𝑥𝑅∅ ↔ 𝑥 ∈ {∅})
Theorem	nregmodel 45444*	The Axiom of Regularity ax-reg 9507 is false in the permutation model defined from 𝐹. Since the other axioms of ZFC hold in all permutation models (permaxext 45432 through permac8prim 45441), we can conclude that Regularity does not follow from those axioms, assuming ZFC is consistent. (If we could prove Regularity from the other axioms, we could prove it in the permutation model and thus obtain a contradiction with this theorem.) Since we also know that Regularity is consistent with the other axioms (wfaxext 45420 through wfac8prim 45429), Regularity is neither provable nor disprovable from the other axioms; i.e., it is independent of them. (Contributed by Eric Schmidt, 16-Nov-2025.)
⊢ 𝐹 = (( I ↾ (V ∖ {∅, {∅}})) ∪ {⟨∅, {∅}⟩, ⟨{∅}, ∅⟩})    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ ¬ ∀𝑥(∃𝑦 𝑦𝑅𝑥 → ∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥)))
Theorem	nregmodelaxext 45445*	The Axiom of Extensionality ax-ext 2709 is true in the permutation model defined from 𝐹. This theorem is an immediate consequence of the fact that ax-ext 2709 holds in all permutation models and is provided as an illustration. (Contributed by Eric Schmidt, 16-Nov-2025.)
⊢ 𝐹 = (( I ↾ (V ∖ {∅, {∅}})) ∪ {⟨∅, {∅}⟩, ⟨{∅}, ∅⟩})    &   ⊢ 𝑅 = (◡𝐹 ∘ E )    ⇒   ⊢ (∀𝑧(𝑧𝑅𝑥 ↔ 𝑧𝑅𝑦) → 𝑥 = 𝑦)
21.43  Mathbox for Glauco Siliprandi
21.43.1  Miscellanea
Theorem	evth2f 45446*	A version of evth2 24927 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑦𝐹    &   ⊢ Ⅎ𝑥𝑋    &   ⊢ Ⅎ𝑦𝑋    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑥) ≤ (𝐹‘𝑦))
Theorem	elunif 45447*	A version of eluni 4854 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 ∈ ∪ 𝐵 ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵))
Theorem	rzalf 45448	A version of rzal 4435 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥 𝐴 = ∅    ⇒   ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)
Theorem	fvelrnbf 45449	A version of fvelrnb 6901 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐹    ⇒   ⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵))
Theorem	rfcnpre1 45450	If F is a continuous function with respect to the standard topology, then the preimage A of the values greater than a given extended real B is an open set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐴 = {𝑥 ∈ 𝑋 ∣ 𝐵 < (𝐹‘𝑥)}    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐽)
Theorem	ubelsupr 45451*	If U belongs to A and U is an upper bound, then U is the sup of A. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝑈 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑈) → 𝑈 = sup(𝐴, ℝ, < ))
Theorem	fsumcnf 45452*	A finite sum of functions to complex numbers from a common topological space is continuous, without disjoint var constraint x ph. The class expression for B normally contains free variables k and x to index it. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn 𝐾))
Theorem	mulltgt0 45453	The product of a negative and a positive number is negative. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐴 < 0) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (𝐴 · 𝐵) < 0)
Theorem	rspcegf 45454	A version of rspcev 3565 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → ∃𝑥 ∈ 𝐵 𝜑)
Theorem	rabexgf 45455	A version of rabexg 5279 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V)
Theorem	fcnre 45456	A function continuous with respect to the standard topology, is a real mapping. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐶)    ⇒   ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)
Theorem	sumsnd 45457*	A sum of a singleton is the term. The deduction version of sumsn 15708. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ (𝜑 → Ⅎ𝑘𝐵)    &   ⊢ Ⅎ𝑘𝜑    &   ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ {𝑀}𝐴 = 𝐵)
Theorem	evthf 45458*	A version of evth 24926 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑦𝐹    &   ⊢ Ⅎ𝑥𝑋    &   ⊢ Ⅎ𝑦𝑋    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑋 ≠ ∅)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥))
Theorem	cnfex 45459	The class of continuous functions between two topologies is a set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 Cn 𝐾) ∈ V)
Theorem	fnchoice 45460*	For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ (𝐴 ∈ Fin → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 ≠ ∅ → (𝑓‘𝑥) ∈ 𝑥)))
Theorem	refsumcn 45461*	A finite sum of continuous real functions, from a common topological space, is continuous. The class expression for B normally contains free variables k and x to index it. See fsumcn 24837 for the analogous theorem on continuous complex functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn 𝐾))
Theorem	rfcnpre2 45462	If 𝐹 is a continuous function with respect to the standard topology, then the preimage A of the values smaller than a given extended real 𝐵, is an open set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐴 = {𝑥 ∈ 𝑋 ∣ (𝐹‘𝑥) < 𝐵}    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → 𝐴 ∈ 𝐽)
Theorem	cncmpmax 45463*	When the hypothesis for the extreme value theorem hold, then the sup of the range of the function belongs to the range, it is real and it an upper bound of the range. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑇 ≠ ∅)    ⇒   ⊢ (𝜑 → (sup(ran 𝐹, ℝ, < ) ∈ ran 𝐹 ∧ sup(ran 𝐹, ℝ, < ) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) ≤ sup(ran 𝐹, ℝ, < )))
Theorem	rfcnpre3 45464*	If F is a continuous function with respect to the standard topology, then the preimage A of the values greater than or equal to a given real B is a closed set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐴 = {𝑡 ∈ 𝑇 ∣ 𝐵 ≤ (𝐹‘𝑡)}    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽))
Theorem	rfcnpre4 45465*	If F is a continuous function with respect to the standard topology, then the preimage A of the values less than or equal to a given real B is a closed set. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ 𝐴 = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ 𝐵}    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽))
Theorem	sumpair 45466*	Sum of two distinct complex values. The class expression for 𝐴 and 𝐵 normally contain free variable 𝑘 to index it. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ (𝜑 → Ⅎ𝑘𝐷)    &   ⊢ (𝜑 → Ⅎ𝑘𝐸)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐸 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝐴) → 𝐶 = 𝐷)    &   ⊢ ((𝜑 ∧ 𝑘 = 𝐵) → 𝐶 = 𝐸)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ {𝐴, 𝐵}𝐶 = (𝐷 + 𝐸))
Theorem	rfcnnnub 45467*	Given a real continuous function 𝐹 defined on a compact topological space, there is always a positive integer that is a strict upper bound of its range. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑡𝐹    &   ⊢ Ⅎ𝑡𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    &   ⊢ 𝑇 = ∪ 𝐽    &   ⊢ (𝜑 → 𝑇 ≠ ∅)    &   ⊢ 𝐶 = (𝐽 Cn 𝐾)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑡 ∈ 𝑇 (𝐹‘𝑡) < 𝑛)
Theorem	refsum2cnlem1 45468*	This is the core Lemma for refsum2cn 45469: the sum of two continuous real functions (from a common topological space) is continuous. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐺    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐴 = (𝑘 ∈ {1, 2} ↦ if(𝑘 = 1, 𝐹, 𝐺))    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) + (𝐺‘𝑥))) ∈ (𝐽 Cn 𝐾))
Theorem	refsum2cn 45469*	The sum of two continuus real functions (from a common topological space) is continuous. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐺    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ 𝐾 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝐹‘𝑥) + (𝐺‘𝑥))) ∈ (𝐽 Cn 𝐾))
Theorem	adantlllr 45470	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	3adantlr3 45471	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜂)) ∧ 𝜃) → 𝜏)
Theorem	3adantll2 45472	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜂 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	3adantll3 45473	Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜂) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	ssnel 45474	If not element of a set, then not element of a subset. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝐴 ⊆ 𝐵 ∧ ¬ 𝐶 ∈ 𝐵) → ¬ 𝐶 ∈ 𝐴)
Theorem	sncldre 45475	A singleton is closed w.r.t. the standard topology on the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝐴 ∈ ℝ → {𝐴} ∈ (Clsd‘(topGen‘ran (,))))
Theorem	n0p 45476	A polynomial with a nonzero coefficient is not the zero polynomial. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ ((𝑃 ∈ (Poly‘ℤ) ∧ 𝑁 ∈ ℕ0 ∧ ((coeff‘𝑃)‘𝑁) ≠ 0) → 𝑃 ≠ 0𝑝)
Theorem	pm2.65ni 45477	Inference rule for proof by contradiction. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (¬ 𝜑 → 𝜓)    &   ⊢ (¬ 𝜑 → ¬ 𝜓)    ⇒   ⊢ 𝜑
Theorem	iuneq2df 45478	Equality deduction for indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
Theorem	nnfoctb 45479*	There exists a mapping from ℕ onto any (nonempty) countable set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝐴 ≼ ω ∧ 𝐴 ≠ ∅) → ∃𝑓 𝑓:ℕ–onto→𝐴)
Theorem	elpwinss 45480	An element of the powerset of 𝐵 intersected with anything, is a subset of 𝐵. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ⊆ 𝐵)
Theorem	unidmex 45481	If 𝐹 is a set, then ∪ dom 𝐹 is a set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ 𝑋 = ∪ dom 𝐹    ⇒   ⊢ (𝜑 → 𝑋 ∈ V)
Theorem	ndisj2 45482*	A non-disjointness condition. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ (¬ Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 ∧ (𝐵 ∩ 𝐶) ≠ ∅))
Theorem	zenom 45483	The set of integer numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ℤ ≈ ω
Theorem	uzwo4 45484*	Well-ordering principle: any nonempty subset of an upper set of integers has the least element. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑗𝜓    &   ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ ∃𝑗 ∈ 𝑆 𝜑) → ∃𝑗 ∈ 𝑆 (𝜑 ∧ ∀𝑘 ∈ 𝑆 (𝑘 < 𝑗 → ¬ 𝜓)))
Theorem	unisn0 45485	The union of the singleton of the empty set is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ∪ {∅} = ∅
Theorem	ssin0 45486	If two classes are disjoint, two respective subclasses are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (((𝐴 ∩ 𝐵) = ∅ ∧ 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) → (𝐶 ∩ 𝐷) = ∅)
Theorem	inabs3 45487	Absorption law for intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐶 ⊆ 𝐵 → ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ 𝐶))
Theorem	pwpwuni 45488	Relationship between power class and union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝒫 𝒫 𝐵 ↔ ∪ 𝐴 ∈ 𝒫 𝐵))
Theorem	disjiun2 45489*	In a disjoint collection, an indexed union is disjoint from an additional term. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐷 ∈ (𝐴 ∖ 𝐶))    &   ⊢ (𝑥 = 𝐷 → 𝐵 = 𝐸)    ⇒   ⊢ (𝜑 → (∪ 𝑥 ∈ 𝐶 𝐵 ∩ 𝐸) = ∅)
Theorem	0pwfi 45490	The empty set is in any power set, and it's finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ∅ ∈ (𝒫 𝐴 ∩ Fin)
Theorem	ssinss2d 45491	Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝜑 → 𝐵 ⊆ 𝐶)    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐵) ⊆ 𝐶)
Theorem	zct 45492	The set of integer numbers is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ℤ ≼ ω
Theorem	pwfin0 45493	A finite set always belongs to a power class. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ (𝒫 𝐴 ∩ Fin) ≠ ∅
Theorem	uzct 45494	An upper integer set is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ 𝑍 = (ℤ≥‘𝑁)    ⇒   ⊢ 𝑍 ≼ ω
Theorem	iunxsnf 45495*	A singleton index picks out an instance of an indexed union's argument. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝐶    &   ⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ {𝐴}𝐵 = 𝐶
Theorem	fiiuncl 45496*	If a set is closed under the union of two sets, then it is closed under finite indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷) → (𝑦 ∪ 𝑧) ∈ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷)
Theorem	iunp1 45497*	The addition of the next set to a union indexed by a finite set of sequential integers. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ Ⅎ𝑘𝐵    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ (𝑀...(𝑁 + 1))𝐴 = (∪ 𝑘 ∈ (𝑀...𝑁)𝐴 ∪ 𝐵))
Theorem	fiunicl 45498*	If a set is closed under the union of two sets, then it is closed under finite union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∪ 𝑦) ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → ∪ 𝐴 ∈ 𝐴)
Theorem	ixpeq2d 45499	Equality theorem for infinite Cartesian product. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶)
Theorem	disjxp1 45500*	The sets of a cartesian product are disjoint if the sets in the first argument are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)    ⇒   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 (𝐵 × 𝐶))