P. 450 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

sspwimpVD 44901

The following User's Proof is a Virtual Deduction proof (see wvd1 44552) using conjunction-form virtual hypothesis collections. It was completed manually, but has the potential to be completed automatically by a tools program which would invoke Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sspwimp 44900 is sspwimpVD 44901 without virtual deductions and was derived from sspwimpVD 44901. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ (   𝐴 ⊆ 𝐵   ▶   𝐴 ⊆ 𝐵   )
2::	⊢ (   .............. 𝑥 ∈ 𝒫 𝐴    ▶   𝑥 ∈ 𝒫 𝐴   )
3:2:	⊢ (   .............. 𝑥 ∈ 𝒫 𝐴    ▶   𝑥 ⊆ 𝐴   )
4:3,1:	⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ⊆ 𝐵   )
5::	⊢ 𝑥 ∈ V
6:4,5:	⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ∈ 𝒫 𝐵    )
7:6:	⊢ (   𝐴 ⊆ 𝐵   ▶   (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)    )
8:7:	⊢ (   𝐴 ⊆ 𝐵   ▶   ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)   )
9:8:	⊢ (   𝐴 ⊆ 𝐵   ▶   𝒫 𝐴 ⊆ 𝒫 𝐵   )
qed:9:	⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

sspwimpcf 44902

If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of [TakeutiZaring] p. 18. sspwimpcf 44902, using conventional notation, was translated from its virtual deduction form, sspwimpcfVD 44903, using a translation program. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

sspwimpcfVD 44903

The following User's Proof is a Virtual Deduction proof (see wvd1 44552) using conjunction-form virtual hypothesis collections. It was completed automatically by a tools program which would invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sspwimpcf 44902 is sspwimpcfVD 44903 without virtual deductions and was derived from sspwimpcfVD 44903. The version of completeusersproof.cmd used is capable of only generating conjunction-form unification theorems, not unification deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ (   𝐴 ⊆ 𝐵   ▶   𝐴 ⊆ 𝐵   )
2::	⊢ (   ........... 𝑥 ∈ 𝒫 𝐴    ▶   𝑥 ∈ 𝒫 𝐴   )
3:2:	⊢ (   ........... 𝑥 ∈ 𝒫 𝐴    ▶   𝑥 ⊆ 𝐴   )
4:3,1:	⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ⊆ 𝐵   )
5::	⊢ 𝑥 ∈ V
6:4,5:	⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ∈ 𝒫 𝐵    )
7:6:	⊢ (   𝐴 ⊆ 𝐵   ▶   (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)    )
8:7:	⊢ (   𝐴 ⊆ 𝐵   ▶   ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)   )
9:8:	⊢ (   𝐴 ⊆ 𝐵   ▶   𝒫 𝐴 ⊆ 𝒫 𝐵   )
qed:9:	⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

suctrALTcf 44904

The successor of a transitive class is transitive. suctrALTcf 44904, using conventional notation, was translated from virtual deduction form, suctrALTcfVD 44905, using a translation program. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (Tr 𝐴 → Tr suc 𝐴)

Theorem

suctrALTcfVD 44905

The following User's Proof is a Virtual Deduction proof (see wvd1 44552) using conjunction-form virtual hypothesis collections. The conjunction-form version of completeusersproof.cmd. It allows the User to avoid superflous virtual hypotheses. This proof was completed automatically by a tools program which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. suctrALTcf 44904 is suctrALTcfVD 44905 without virtual deductions and was derived automatically from suctrALTcfVD 44905. The version of completeusersproof.cmd used is capable of only generating conjunction-form unification theorems, not unification deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ (   Tr 𝐴   ▶   Tr 𝐴   )
2::	⊢ (   ......... (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   )
3:2:	⊢ (   ......... (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   𝑧 ∈ 𝑦   )
4::	⊢ (   ................................... ....... 𝑦 ∈ 𝐴   ▶   𝑦 ∈ 𝐴   )
5:1,3,4:	⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 ∈ 𝐴   )   ▶   𝑧 ∈ 𝐴   )
6::	⊢ 𝐴 ⊆ suc 𝐴
7:5,6:	⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 ∈ 𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
8:7:	⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)    )   ▶   (𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴)   )
9::	⊢ (   ................................... ...... 𝑦 = 𝐴   ▶   𝑦 = 𝐴   )
10:3,9:	⊢ (   ........ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴), 𝑦 = 𝐴   )   ▶   𝑧 ∈ 𝐴   )
11:10,6:	⊢ (   ........ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴), 𝑦 = 𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
12:11:	⊢ (   .......... (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴)   )
13:2:	⊢ (   .......... (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   𝑦 ∈ suc 𝐴   )
14:13:	⊢ (   .......... (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)   )
15:8,12,14:	⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)    )   ▶   𝑧 ∈ suc 𝐴   )
16:15:	⊢ (   Tr 𝐴   ▶   ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
17:16:	⊢ (   Tr 𝐴   ▶   ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
18:17:	⊢ (   Tr 𝐴   ▶   Tr suc 𝐴   )
qed:18:	⊢ (Tr 𝐴 → Tr suc 𝐴)

⊢ (Tr 𝐴 → Tr suc 𝐴)

21.41.10  Theorems with a VD proof in conventional notation derived from a VD proof

Theorem

suctrALT3 44906

The successor of a transitive class is transitive. suctrALT3 44906 is the completed proof in conventional notation of the Virtual Deduction proof https://us.metamath.org/other/completeusersproof/suctralt3vd.html 44906. It was completed manually. The potential for automated derivation from the VD proof exists. See wvd1 44552 for a description of Virtual Deduction. Some sub-theorems of the proof were completed using a unification deduction (e.g., the sub-theorem whose assertion is step 19 used jaoded 44549). Unification deductions employ Mario Carneiro's metavariable concept. Some sub-theorems were completed using a unification theorem (e.g., the sub-theorem whose assertion is step 24 used dftr2 5218) . (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (Tr 𝐴 → Tr suc 𝐴)

Theorem

sspwimpALT 44907

If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of [TakeutiZaring] p. 18. sspwimpALT 44907 is the completed proof in conventional notation of the Virtual Deduction proof https://us.metamath.org/other/completeusersproof/sspwimpaltvd.html 44907. It was completed manually. The potential for automated derivation from the VD proof exists. See wvd1 44552 for a description of Virtual Deduction. Some sub-theorems of the proof were completed using a unification deduction (e.g., the sub-theorem whose assertion is step 9 used elpwgded 44547). Unification deductions employ Mario Carneiro's metavariable concept. Some sub-theorems were completed using a unification theorem (e.g., the sub-theorem whose assertion is step 5 used elpwi 4572). (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

unisnALT 44908

A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. The User manually input on a mmj2 Proof Worksheet, without labels, all steps of unisnALT 44908 except 1, 11, 15, 21, and 30. With execution of the mmj2 unification command, mmj2 could find labels for all steps except for 2, 12, 16, 22, and 31 (and the then non-existing steps 1, 11, 15, 21, and 30). mmj2 could not find reference theorems for those five steps because the hypothesis field of each of these steps was empty and none of those steps unifies with a theorem in set.mm. Each of these five steps is a semantic variation of a theorem in set.mm and is 2-step provable. mmj2 does not have the ability to automatically generate the semantic variation in set.mm of a theorem in a mmj2 Proof Worksheet unless the theorem in the Proof Worksheet is labeled with a 1-hypothesis deduction whose hypothesis is a theorem in set.mm which unifies with the theorem in the Proof Worksheet. The stepprover.c program, which invokes mmj2, has this capability. stepprover.c automatically generated steps 1, 11, 15, 21, and 30, labeled all steps, and generated the RPN proof of unisnALT 44908. Roughly speaking, stepprover.c added to the Proof Worksheet a labeled duplicate step of each non-unifying theorem for each label in a text file, labels.txt, containing a list of labels provided by the User. Upon mmj2 unification, stepprover.c identified a label for each of the five theorems which 2-step proves it. For unisnALT 44908, the label list is a list of all 1-hypothesis propositional calculus deductions in set.mm. stepproverp.c is the same as stepprover.c except that it intermittently pauses during execution, allowing the User to observe the changes to a text file caused by the execution of particular statements of the program. (Contributed by Alan Sare, 19-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝐴 ∈ V    ⇒   ⊢ ∪ {𝐴} = 𝐴

21.41.11  Theorems with a proof in conventional notation derived from a VD proof

Theorems with a proof in conventional notation automatically derived by completeusersproof.c from a Virtual Deduction User's Proof.

Theorem

notnotrALT2 44909

Converse of double negation. Theorem *2.14 of [WhiteheadRussell] p. 102. Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (¬ ¬ 𝜑 → 𝜑)

Theorem

sspwimpALT2 44910

If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of [TakeutiZaring] p. 18. Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in https://us.metamath.org/other/completeusersproof/sspwimpaltvd.html. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

e2ebindALT 44911

Absorption of an existential quantifier of a double existential quantifier of non-distinct variables. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in e2ebindVD 44894. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑))

Theorem

ax6e2ndALT 44912*

If at least two sets exist (dtru 5398), then the same is true expressed in an alternate form similar to the form of ax6e 2382. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in ax6e2ndVD 44890. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Theorem

ax6e2ndeqALT 44913*

"At least two sets exist" expressed in the form of dtru 5398 is logically equivalent to the same expressed in a form similar to ax6e 2382 if dtru 5398 is false implies 𝑢 = 𝑣. Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in ax6e2ndeqVD 44891. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Theorem

2sb5ndALT 44914*

Equivalence for double substitution 2sb5 2278 without distinct 𝑥, 𝑦 requirement. 2sb5nd 44543 is derived from 2sb5ndVD 44892. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in 2sb5ndVD 44892. (Contributed by Alan Sare, 19-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))

Theorem

chordthmALT 44915*

The intersecting chords theorem. If points A, B, C, and D lie on a circle (with center Q, say), and the point P is on the interior of the segments AB and CD, then the two products of lengths PA · PB and PC · PD are equal. The Euclidean plane is identified with the complex plane, and the fact that P is on AB and on CD is expressed by the hypothesis that the angles APB and CPD are equal to π. The result is proven by using chordthmlem5 26752 twice to show that PA · PB and PC · PD both equal BQ ² − PQ ² . This is similar to the proof of the theorem given in Euclid's Elements, where it is Proposition III.35. Proven by David Moews on 28-Feb-2017 as chordthm 26753. https://us.metamath.org/other/completeusersproof/chordthmaltvd.html 26753 is a Virtual Deduction User's Proof transcription of chordthm 26753. That VD User's Proof was input into completeusersproof, automatically generating this chordthmALT 44915 Metamath proof. (Contributed by Alan Sare, 19-Sep-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑃 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝑃)    &   ⊢ (𝜑 → 𝐵 ≠ 𝑃)    &   ⊢ (𝜑 → 𝐶 ≠ 𝑃)    &   ⊢ (𝜑 → 𝐷 ≠ 𝑃)    &   ⊢ (𝜑 → ((𝐴 − 𝑃)𝐹(𝐵 − 𝑃)) = π)    &   ⊢ (𝜑 → ((𝐶 − 𝑃)𝐹(𝐷 − 𝑃)) = π)    &   ⊢ (𝜑 → 𝑄 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐵 − 𝑄)))    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐶 − 𝑄)))    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐷 − 𝑄)))    ⇒   ⊢ (𝜑 → ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = ((abs‘(𝑃 − 𝐶)) · (abs‘(𝑃 − 𝐷))))

Theorem

isosctrlem1ALT 44916

Lemma for isosctr 26737. This proof was automatically derived by completeusersproof from its Virtual Deduction proof counterpart https://us.metamath.org/other/completeusersproof/isosctrlem1altvd.html 26737. As it is verified by the Metamath program, isosctrlem1ALT 44916 verifies https://us.metamath.org/other/completeusersproof/isosctrlem1altvd.html 44916. (Contributed by Alan Sare, 22-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) ≠ π)

Theorem

iunconnlem2 44917*

The indexed union of connected overlapping subspaces sharing a common point is connected. This proof was automatically derived by completeusersproof from its Virtual Deduction proof counterpart https://us.metamath.org/other/completeusersproof/iunconlem2vd.html. As it is verified by the Metamath program, iunconnlem2 44917 verifies https://us.metamath.org/other/completeusersproof/iunconlem2vd.html 44917. (Contributed by Alan Sare, 22-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜓 ↔ ((((((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐽) ∧ (𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅) ∧ (𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅) ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵)) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾_t 𝐵) ∈ Conn)    ⇒   ⊢ (𝜑 → (𝐽 ↾_t ∪ 𝑘 ∈ 𝐴 𝐵) ∈ Conn)

Theorem

iunconnALT 44918*

The indexed union of connected overlapping subspaces sharing a common point is connected. This proof was automatically derived by completeusersproof from its Virtual Deduction proof counterpart https://us.metamath.org/other/completeusersproof/iunconaltvd.html. As it is verified by the Metamath program, iunconnALT 44918 verifies https://us.metamath.org/other/completeusersproof/iunconaltvd.html 44918. (Contributed by Alan Sare, 22-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾_t 𝐵) ∈ Conn)    ⇒   ⊢ (𝜑 → (𝐽 ↾_t ∪ 𝑘 ∈ 𝐴 𝐵) ∈ Conn)

Theorem

sineq0ALT 44919

A complex number whose sine is zero is an integer multiple of π. The Virtual Deduction form of the proof is https://us.metamath.org/other/completeusersproof/sineq0altvd.html. The Metamath form of the proof is sineq0ALT 44919. The Virtual Deduction proof is based on Mario Carneiro's revision of Norm Megill's proof of sineq0 26439. The Virtual Deduction proof is verified by automatically transforming it into the Metamath form of the proof using completeusersproof, which is verified by the Metamath program. The proof of https://us.metamath.org/other/completeusersproof/sineq0altro.html 26439 is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 13-Jun-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ∈ ℂ → ((sin‘𝐴) = 0 ↔ (𝐴 / π) ∈ ℤ))

21.42  Mathbox for Eric Schmidt

21.42.1  Miscellany

Theorem

rspesbcd 44920*

Restricted quantifier version of spesbcd 3848. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → [𝐴 / 𝑥]𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)

Theorem

rext0 44921*

Nonempty existential quantification of a theorem is true. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ 𝜑    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 ≠ ∅)

21.42.2  Study of dfbi1ALT

Theorem

dfbi1ALTa 44922

Version of dfbi1ALT 214 using ⊤ for step 2 and shortened using a1i 11, a2i 14, and con4i 114. (Contributed by Eric Schmidt, 22-Oct-2025.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))

Theorem

simprimi 44923

Inference associated with simprim 166. Proved exactly as step 11 is obtained from step 4 in dfbi1ALTa 44922. (Contributed by Eric Schmidt, 22-Oct-2025.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ ¬ (𝜑 → ¬ 𝜓)    ⇒   ⊢ 𝜓

Theorem

dfbi1ALTb 44924

Further shorten dfbi1ALTa 44922 using simprimi 44923. (Contributed by Eric Schmidt, 22-Oct-2025.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))

21.42.3  Relation-preserving functions

Syntax

wrelp 44925

Extend the definition of a wff to include the relation-preserving property. (Contributed by Eric Schmidt, 11-Oct-2025.)

wff 𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵)

Definition

df-relp 44926*

Define the relation-preserving predicate. This is a viable notion of "homomorphism" corresponding to df-isom 6522. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ (𝐻:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))))

Theorem

relpeq1 44927

Equality theorem for relation-preserving functions. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝐻 = 𝐺 → (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ 𝐺 RelPres 𝑅, 𝑆(𝐴, 𝐵)))

Theorem

relpeq2 44928

Equality theorem for relation-preserving functions. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝑅 = 𝑇 → (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ 𝐻 RelPres 𝑇, 𝑆(𝐴, 𝐵)))

Theorem

relpeq3 44929

Equality theorem for relation-preserving functions. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝑆 = 𝑇 → (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ 𝐻 RelPres 𝑅, 𝑇(𝐴, 𝐵)))

Theorem

relpeq4 44930

Equality theorem for relation-preserving functions. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝐴 = 𝐶 → (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ 𝐻 RelPres 𝑅, 𝑆(𝐶, 𝐵)))

Theorem

relpeq5 44931

Equality theorem for relation-preserving functions. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝐵 = 𝐶 → (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ 𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐶)))

Theorem

nfrelp 44932

Bound-variable hypothesis builder for a relation-preserving function. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ Ⅎ𝑥𝐻    &   ⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝑆    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵)

Theorem

relpf 44933

A relation-preserving function is a function. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) → 𝐻:𝐴⟶𝐵)

Theorem

relprel 44934

A relation-preserving function preserves the relation. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ ((𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶𝑅𝐷 → (𝐻‘𝐶)𝑆(𝐻‘𝐷)))

Theorem

relpmin 44935

A preimage of a minimal element under a relation-preserving function is minimal. Essentially one half of isomin 7314. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ ((𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (((𝐻 “ 𝐶) ∩ (^◡𝑆 “ {(𝐻‘𝐷)})) = ∅ → (𝐶 ∩ (^◡𝑅 “ {𝐷})) = ∅))

Theorem

relpfrlem 44936*

Lemma for relpfr 44937. Proved without using the Axiom of Replacement. This is isofrlem 7317 with weaker hypotheses. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝜑 → 𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵))    &   ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)    ⇒   ⊢ (𝜑 → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))

Theorem

relpfr 44937

If the image of a set under a relation-preserving function is well-founded, so is the set. See isofr 7319 for a bidirectional statement. A more general version of Lemma I.9.9 of [Kunen2] p. 47. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))

21.42.4  Orbits

Theorem

orbitex 44938

Orbits exist. Given a set 𝐴 and a function 𝐹, the orbit of 𝐴 under 𝐹 is the smallest set 𝑍 such that 𝐴 ∈ 𝑍 and 𝑍 is closed under 𝐹. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ (rec(𝐹, 𝐴) “ ω) ∈ V

Theorem

orbitinit 44939

A set is contained in its orbit. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ (rec(𝐹, 𝐴) “ ω))

Theorem

orbitcl 44940

The orbit under a function is closed under the function. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ (𝐵 ∈ (rec(𝐹, 𝐴) “ ω) → (𝐹‘𝐵) ∈ (rec(𝐹, 𝐴) “ ω))

Theorem

orbitclmpt 44941

Version of orbitcl 44940 using maps-to notation. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ 𝑍 = (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) “ ω)    &   ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝐵 ∈ 𝑍 ∧ 𝐷 ∈ 𝑉) → 𝐷 ∈ 𝑍)

21.42.5  Well-founded sets

Theorem

trwf 44942

The class of well-founded sets is transitive. (Contributed by Eric Schmidt, 9-Sep-2025.)

⊢ Tr ∪ (𝑅₁ “ On)

Theorem

rankrelp 44943

The rank function preserves ∈. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ rank RelPres E , E (∪ (𝑅₁ “ On), On)

Theorem

wffr 44944

The class of well-founded sets is well-founded. Lemma I.9.24(2) of [Kunen2] p. 53. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ E Fr ∪ (𝑅₁ “ On)

Theorem

trfr 44945

A transitive class well-founded by ∈ is a subclass of the class of well-founded sets. Part of Lemma I.9.21 of [Kunen2] p. 53. (Contributed by Eric Schmidt, 26-Oct-2025.)

⊢ ((Tr 𝐴 ∧ E Fr 𝐴) → 𝐴 ⊆ ∪ (𝑅₁ “ On))

Theorem

tcfr 44946

A set is well-founded if and only if its transitive closure is well-founded by ∈. This characterization of well-founded sets is that in Definition I.9.20 of [Kunen2] p. 53. (Contributed by Eric Schmidt, 26-Oct-2025.)

⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∪ (𝑅₁ “ On) ↔ E Fr (TC‘𝐴))

Theorem

xpwf 44947

The Cartesian product of two well-founded sets is well-founded. (Contributed by Eric Schmidt, 12-Sep-2025.)

⊢ ((𝐴 ∈ ∪ (𝑅₁ “ On) ∧ 𝐵 ∈ ∪ (𝑅₁ “ On)) → (𝐴 × 𝐵) ∈ ∪ (𝑅₁ “ On))

Theorem

dmwf 44948

The domain of a well-founded set is well-founded. (Contributed by Eric Schmidt, 12-Sep-2025.)

⊢ (𝐴 ∈ ∪ (𝑅₁ “ On) → dom 𝐴 ∈ ∪ (𝑅₁ “ On))

Theorem

rnwf 44949

The range of a well-founded set is well-founded. (Contributed by Eric Schmidt, 12-Sep-2025.)

⊢ (𝐴 ∈ ∪ (𝑅₁ “ On) → ran 𝐴 ∈ ∪ (𝑅₁ “ On))

Theorem

relwf 44950

A relation is a well-founded set iff its domain and range are. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (Rel 𝑅 → (𝑅 ∈ ∪ (𝑅₁ “ On) ↔ (dom 𝑅 ∈ ∪ (𝑅₁ “ On) ∧ ran 𝑅 ∈ ∪ (𝑅₁ “ On))))

21.42.6  Absoluteness in transitive models

Theorem

ralabso 44951*

Simplification of restricted quantification in a transitive class. When 𝜑 is quantifier-free, this shows that the formula ∀𝑥 ∈ 𝑦𝜑 is absolute for transitive models, which is a particular case of Lemma I.16.2 of [Kunen2] p. 95. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((Tr 𝑀 ∧ 𝐴 ∈ 𝑀) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 → 𝜑)))

Theorem

rexabso 44952*

Simplification of restricted quantification in a transitive class. When 𝜑 is quantifier-free, this shows that the formula ∃𝑥 ∈ 𝑦𝜑 is absolute for transitive models, which is a particular case of Lemma I.16.2 of [Kunen2] p. 95. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((Tr 𝑀 ∧ 𝐴 ∈ 𝑀) → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 ∧ 𝜑)))

Theorem

ralabsod 44953*

Deduction form of ralabso 44951. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (𝜑 → Tr 𝑀)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑀) → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 → 𝜓)))

Theorem

rexabsod 44954*

Deduction form of rexabso 44952. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (𝜑 → Tr 𝑀)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑀) → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 ∧ 𝜓)))

Theorem

ralabsobidv 44955*

Formula-building lemma for proving absoluteness results. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (𝜑 → Tr 𝑀)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑀) → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 → 𝜒)))

Theorem

rexabsobidv 44956*

Formula-building lemma for proving absoluteness results. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (𝜑 → Tr 𝑀)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑀) → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 ∧ 𝜒)))

Theorem

ssabso 44957*

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 44958*

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 44959*

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 44960*

A transitive class models the Axiom of Extensionality ax-ext 2702. Lemma II.2.4(1) of [Kunen2] p. 111. (Contributed by Eric Schmidt, 11-Sep-2025.)

⊢ (Tr 𝑀 → ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦))

Theorem

modelaxreplem1 44961*

Lemma for modelaxrep 44964. We show that 𝑀 is closed under taking subsets. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (𝜓 → 𝑥 ⊆ 𝑀)    &   ⊢ (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀))    &   ⊢ (𝜓 → ∅ ∈ 𝑀)    &   ⊢ (𝜓 → 𝑥 ∈ 𝑀)    &   ⊢ 𝐴 ⊆ 𝑥    ⇒   ⊢ (𝜓 → 𝐴 ∈ 𝑀)

Theorem

modelaxreplem2 44962*

Lemma for modelaxrep 44964. We define a class 𝐹 and show that the antecedent of Replacement implies that 𝐹 is a function. We use Replacement (in the form of funex 7195) 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 44963*

Lemma for modelaxrep 44964. 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 44964*

Conditions which guarantee that a class models the Axiom of Replacement ax-rep 5236. 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 7935). 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 44965*

A class that is closed under subsets models the Axiom of Separation ax-sep 5253. 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 44966*

A class that contains the empty set models the Null Set Axiom ax-nul 5263. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (∅ ∈ 𝑀 → ∃𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ¬ 𝑦 ∈ 𝑥)

Theorem

pwclaxpow 44967*

Suppose 𝑀 is a transitive class that is closed under power sets intersected with 𝑀. Then, 𝑀 models the Axiom of Power Sets ax-pow 5322. One direction of Lemma II.2.8 of [Kunen2] p. 113. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((Tr 𝑀 ∧ ∀𝑥 ∈ 𝑀 (𝒫 𝑥 ∩ 𝑀) ∈ 𝑀) → ∀𝑥 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))

Theorem

prclaxpr 44968*

A class that is closed under the pairing operation models the Axiom of Pairing ax-pr 5389. Lemma II.2.4(4) of [Kunen2] p. 111. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 {𝑥, 𝑦} ∈ 𝑀 → ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∃𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧))

Theorem

uniclaxun 44969*

A class that is closed under the union operation models the Axiom of Union ax-un 7713. Lemma II.2.4(5) of [Kunen2] p. 111. (Contributed by Eric Schmidt, 1-Oct-2025.)

⊢ (∀𝑥 ∈ 𝑀 ∪ 𝑥 ∈ 𝑀 → ∀𝑥 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))

Theorem

sswfaxreg 44970*

A subclass of the class of well-founded sets models the Axiom of Regularity ax-reg 9551. Lemma II.2.4(2) of [Kunen2] p. 111. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (𝑀 ⊆ ∪ (𝑅₁ “ On) → ∀𝑥 ∈ 𝑀 (∃𝑦 ∈ 𝑀 𝑦 ∈ 𝑥 → ∃𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥))))

Theorem

omssaxinf2 44971*

A class that contains all ordinals up to and including ω models the Axiom of Infinity ax-inf2 9600. The antecedent of this theorem is not enough to guarantee that the class models the alternate axiom ax-inf 9597. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((ω ⊆ 𝑀 ∧ ω ∈ 𝑀) → ∃𝑥 ∈ 𝑀 (∃𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑀 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))))

Theorem

omelaxinf2 44972*

A transitive class that contains ω models the Axiom of Infinity ax-inf2 9600. 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 9597. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((Tr 𝑀 ∧ ω ∈ 𝑀) → ∃𝑥 ∈ 𝑀 (∃𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑀 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))))

Theorem

dfac5prim 44973*

dfac5 10088 expanded into primitives. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (CHOICE ↔ ∀𝑥((∀𝑧(𝑧 ∈ 𝑥 → ∃𝑤 𝑤 ∈ 𝑧) ∧ ∀𝑧∀𝑤((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦(𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑥 → ∃𝑤∀𝑣((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))))

Theorem

ac8prim 44974*

ac8 10451 expanded into primitives. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((∀𝑧(𝑧 ∈ 𝑥 → ∃𝑤 𝑤 ∈ 𝑧) ∧ ∀𝑧∀𝑤((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦(𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑥 → ∃𝑤∀𝑣((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))

Theorem

modelac8prim 44975*

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 44974.

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 44976*

The class of well-founded sets models the Axiom of Extensionality ax-ext 2702. 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.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 (∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)

Theorem

wfaxrep 44977*

The class of well-founded sets models the Axiom of Replacement ax-rep 5236. 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.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 (∀𝑤 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑊 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)))

Theorem

wfaxsep 44978*

The class of well-founded sets models the Axiom of Separation ax-sep 5253. 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.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∀𝑧 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑥 ∈ 𝑊 (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))

Theorem

wfaxnul 44979*

The class of well-founded sets models the Null Set Axiom ax-nul 5263. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∃𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 ¬ 𝑦 ∈ 𝑥

Theorem

wfaxpow 44980*

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.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (∀𝑤 ∈ 𝑊 (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)

Theorem

wfaxpr 44981*

The class of well-founded sets models the Axiom of Pairing ax-pr 5389. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 ∃𝑧 ∈ 𝑊 ∀𝑤 ∈ 𝑊 ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)

Theorem

wfaxun 44982*

The class of well-founded sets models the Axiom of Union ax-un 7713. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (∃𝑤 ∈ 𝑊 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)

Theorem

wfaxreg 44983*

The class of well-founded sets models the Axiom of Regularity ax-reg 9551. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 (∃𝑦 ∈ 𝑊 𝑦 ∈ 𝑥 → ∃𝑦 ∈ 𝑊 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)))

Theorem

wfaxinf2 44984*

The class of well-founded sets models the Axiom of Infinity ax-inf2 9600. Part of Corollary II.2.12 of [Kunen2] p. 114. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∃𝑥 ∈ 𝑊 (∃𝑦 ∈ 𝑊 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑊 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑊 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑊 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))))

Theorem

wfac8prim 44985*

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 44974. Part of Corollary II.2.12 of [Kunen2] p. 114. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ((∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑊 ∀𝑤 ∈ 𝑊 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑊 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 ∀𝑣 ∈ 𝑊 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))

21.42.9  Permutation models

Theorem

brpermmodel 44986

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 44987

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 44988*

The Axiom of Extensionality ax-ext 2702 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 44989*

The Axiom of Replacement ax-rep 5236 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 44990*

The Axiom of Separation ax-sep 5253 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 44991*

The Null Set Axiom ax-nul 5263 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 44992*

The Axiom of Power Sets ax-pow 5322 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 44993*

The Axiom of Pairing ax-pr 5389 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 44994*

The Axiom of Union ax-un 7713 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 44995*

Lemma for permaxinf2 44996. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (^◡𝐹 ∘ E )    &   ⊢ 𝑍 = (rec((𝑣 ∈ V ↦ (^◡𝐹‘((𝐹‘𝑣) ∪ {𝑣}))), (^◡𝐹‘∅)) “ ω)    ⇒   ⊢ ∃𝑥(∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧 ¬ 𝑧𝑅𝑦) ∧ ∀𝑦(𝑦𝑅𝑥 → ∃𝑧(𝑧𝑅𝑥 ∧ ∀𝑤(𝑤𝑅𝑧 ↔ (𝑤𝑅𝑦 ∨ 𝑤 = 𝑦)))))

Theorem

permaxinf2 44996*

The Axiom of Infinity ax-inf2 9600 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 44997*

The Axiom of Choice ac8prim 44974 holds in permutation models. Part of Exercise II.9.3 of [Kunen2] p. 149. Note that ax-ac 10418 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 44998

Define a permutation 𝐹 used to produce a model in which ax-reg 9551 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 44999

Lemma for nregmodel 45000. (Contributed by Eric Schmidt, 16-Nov-2025.)

⊢ 𝐹 = (( I ↾ (V ∖ {∅, {∅}})) ∪ {⟨∅, {∅}⟩, ⟨{∅}, ∅⟩})    &   ⊢ 𝑅 = (^◡𝐹 ∘ E )    ⇒   ⊢ (𝑥𝑅∅ ↔ 𝑥 ∈ {∅})

Theorem

nregmodel 45000*

The Axiom of Regularity ax-reg 9551 is false in the permutation model defined from 𝐹. Since the other axioms of ZFC hold in all permutation models (permaxext 44988 through permac8prim 44997), 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 44976 through wfac8prim 44985), 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 )    ⇒   ⊢ ¬ ∀𝑥(∃𝑦 𝑦𝑅𝑥 → ∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥)))