Metamath Proof Explorer

Theorem nregmodel

Description: The Axiom of Regularity ax-reg is false in the permutation model defined from F . Since the other axioms of ZFC hold in all permutation models ( permaxext through permac8prim ), 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 through wfac8prim ), Regularity is neither provable nor disprovable from the other axioms; i.e., it is independent of them. (Contributed by Eric Schmidt, 16-Nov-2025)

Ref Expression
Hypotheses nregmodel.1 ⊢ F = I ↾ V ∖ ∅ ∅ ∪ ∅ ∅ ∅ ∅
nregmodel.2 ⊢ R = F -1 ∘ E
Assertion nregmodel ⊢ ¬ ∀ x ∃ y y R x → ∃ y y R x ∧ ∀ z z R y → ¬ z R x

Proof

Step Hyp Ref Expression
1 nregmodel.1 ⊢ F = I ↾ V ∖ ∅ ∅ ∪ ∅ ∅ ∅ ∅
2 nregmodel.2 ⊢ R = F -1 ∘ E
3 0ex ⊢ ∅ ∈ V
4 3 snid ⊢ ∅ ∈ ∅
5 eleq1 ⊢ y = ∅ → y ∈ ∅ ↔ ∅ ∈ ∅
6 3 5 4 ceqsexv2d ⊢ ∃ y y ∈ ∅
7 breq2 ⊢ x = ∅ → y R x ↔ y R ∅
8 1 2 nregmodellem ⊢ y R ∅ ↔ y ∈ ∅
9 7 8 bitrdi ⊢ x = ∅ → y R x ↔ y ∈ ∅
10 9 exbidv ⊢ x = ∅ → ∃ y y R x ↔ ∃ y y ∈ ∅
11 breq2 ⊢ x = ∅ → z R x ↔ z R ∅
12 1 2 nregmodellem ⊢ z R ∅ ↔ z ∈ ∅
13 11 12 bitrdi ⊢ x = ∅ → z R x ↔ z ∈ ∅
14 13 notbid ⊢ x = ∅ → ¬ z R x ↔ ¬ z ∈ ∅
15 14 imbi2d ⊢ x = ∅ → z R y → ¬ z R x ↔ z R y → ¬ z ∈ ∅
16 15 albidv ⊢ x = ∅ → ∀ z z R y → ¬ z R x ↔ ∀ z z R y → ¬ z ∈ ∅
17 9 16 anbi12d ⊢ x = ∅ → y R x ∧ ∀ z z R y → ¬ z R x ↔ y ∈ ∅ ∧ ∀ z z R y → ¬ z ∈ ∅
18 17 exbidv ⊢ x = ∅ → ∃ y y R x ∧ ∀ z z R y → ¬ z R x ↔ ∃ y y ∈ ∅ ∧ ∀ z z R y → ¬ z ∈ ∅
19 10 18 imbi12d ⊢ x = ∅ → ∃ y y R x → ∃ y y R x ∧ ∀ z z R y → ¬ z R x ↔ ∃ y y ∈ ∅ → ∃ y y ∈ ∅ ∧ ∀ z z R y → ¬ z ∈ ∅
20 3 19 spcv ⊢ ∀ x ∃ y y R x → ∃ y y R x ∧ ∀ z z R y → ¬ z R x → ∃ y y ∈ ∅ → ∃ y y ∈ ∅ ∧ ∀ z z R y → ¬ z ∈ ∅
21 6 20 mpi ⊢ ∀ x ∃ y y R x → ∃ y y R x ∧ ∀ z z R y → ¬ z R x → ∃ y y ∈ ∅ ∧ ∀ z z R y → ¬ z ∈ ∅
22 df-ral ⊢ ∀ z ∈ ∅ ¬ z ∈ ∅ ↔ ∀ z z ∈ ∅ → ¬ z ∈ ∅
23 breq2 ⊢ y = ∅ → z R y ↔ z R ∅
24 23 12 bitrdi ⊢ y = ∅ → z R y ↔ z ∈ ∅
25 24 imbi1d ⊢ y = ∅ → z R y → ¬ z ∈ ∅ ↔ z ∈ ∅ → ¬ z ∈ ∅
26 25 albidv ⊢ y = ∅ → ∀ z z R y → ¬ z ∈ ∅ ↔ ∀ z z ∈ ∅ → ¬ z ∈ ∅
27 3 26 rexsn ⊢ ∃ y ∈ ∅ ∀ z z R y → ¬ z ∈ ∅ ↔ ∀ z z ∈ ∅ → ¬ z ∈ ∅
28 df-rex ⊢ ∃ y ∈ ∅ ∀ z z R y → ¬ z ∈ ∅ ↔ ∃ y y ∈ ∅ ∧ ∀ z z R y → ¬ z ∈ ∅
29 22 27 28 3bitr2ri ⊢ ∃ y y ∈ ∅ ∧ ∀ z z R y → ¬ z ∈ ∅ ↔ ∀ z ∈ ∅ ¬ z ∈ ∅
30 eleq1 ⊢ z = ∅ → z ∈ ∅ ↔ ∅ ∈ ∅
31 30 notbid ⊢ z = ∅ → ¬ z ∈ ∅ ↔ ¬ ∅ ∈ ∅
32 3 31 ralsn ⊢ ∀ z ∈ ∅ ¬ z ∈ ∅ ↔ ¬ ∅ ∈ ∅
33 29 32 bitri ⊢ ∃ y y ∈ ∅ ∧ ∀ z z R y → ¬ z ∈ ∅ ↔ ¬ ∅ ∈ ∅
34 21 33 sylib ⊢ ∀ x ∃ y y R x → ∃ y y R x ∧ ∀ z z R y → ¬ z R x → ¬ ∅ ∈ ∅
35 4 34 mt2 ⊢ ¬ ∀ x ∃ y y R x → ∃ y y R x ∧ ∀ z z R y → ¬ z R x