Theorem nregmodel 45294

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

Hypotheses

Ref	Expression
nregmodel.1	⊢ 𝐹 = (( I ↾ (V ∖ {∅, {∅}})) ∪ {⟨∅, {∅}⟩, ⟨{∅}, ∅⟩})
nregmodel.2	⊢ 𝑅 = (◡𝐹 ∘ E )

Assertion

Ref	Expression
nregmodel	⊢ ¬ ∀𝑥(∃𝑦 𝑦𝑅𝑥 → ∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥)))

Distinct variable groups:   𝑥,𝑦,𝑧   𝑥,𝑅

Allowed substitution hints:   𝑅(𝑦,𝑧)   𝐹(𝑥,𝑦,𝑧)

Proof of Theorem nregmodel

Step	Hyp	Ref	Expression
1		0ex 5253	. . 3 ⊢ ∅ ∈ V
2	1	snid 4620	. 2 ⊢ ∅ ∈ {∅}
3		eleq1 2825	. . . . 5 ⊢ (𝑦 = ∅ → (𝑦 ∈ {∅} ↔ ∅ ∈ {∅}))
4	1, 3, 2	ceqsexv2d 3492	. . . 4 ⊢ ∃𝑦 𝑦 ∈ {∅}
5		breq2 5103	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑦𝑅𝑥 ↔ 𝑦𝑅∅))
6		nregmodel.1	. . . . . . . . 9 ⊢ 𝐹 = (( I ↾ (V ∖ {∅, {∅}})) ∪ {⟨∅, {∅}⟩, ⟨{∅}, ∅⟩})
7		nregmodel.2	. . . . . . . . 9 ⊢ 𝑅 = (◡𝐹 ∘ E )
8	6, 7	nregmodellem 45293	. . . . . . . 8 ⊢ (𝑦𝑅∅ ↔ 𝑦 ∈ {∅})
9	5, 8	bitrdi 287	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝑦𝑅𝑥 ↔ 𝑦 ∈ {∅}))
10	9	exbidv 1923	. . . . . 6 ⊢ (𝑥 = ∅ → (∃𝑦 𝑦𝑅𝑥 ↔ ∃𝑦 𝑦 ∈ {∅}))
11		breq2 5103	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (𝑧𝑅𝑥 ↔ 𝑧𝑅∅))
12	6, 7	nregmodellem 45293	. . . . . . . . . . . 12 ⊢ (𝑧𝑅∅ ↔ 𝑧 ∈ {∅})
13	11, 12	bitrdi 287	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → (𝑧𝑅𝑥 ↔ 𝑧 ∈ {∅}))
14	13	notbid 318	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → (¬ 𝑧𝑅𝑥 ↔ ¬ 𝑧 ∈ {∅}))
15	14	imbi2d 340	. . . . . . . . 9 ⊢ (𝑥 = ∅ → ((𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥) ↔ (𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅})))
16	15	albidv 1922	. . . . . . . 8 ⊢ (𝑥 = ∅ → (∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥) ↔ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅})))
17	9, 16	anbi12d 633	. . . . . . 7 ⊢ (𝑥 = ∅ → ((𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥)) ↔ (𝑦 ∈ {∅} ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅}))))
18	17	exbidv 1923	. . . . . 6 ⊢ (𝑥 = ∅ → (∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥)) ↔ ∃𝑦(𝑦 ∈ {∅} ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅}))))
19	10, 18	imbi12d 344	. . . . 5 ⊢ (𝑥 = ∅ → ((∃𝑦 𝑦𝑅𝑥 → ∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥))) ↔ (∃𝑦 𝑦 ∈ {∅} → ∃𝑦(𝑦 ∈ {∅} ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅})))))
20	1, 19	spcv 3560	. . . 4 ⊢ (∀𝑥(∃𝑦 𝑦𝑅𝑥 → ∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥))) → (∃𝑦 𝑦 ∈ {∅} → ∃𝑦(𝑦 ∈ {∅} ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅}))))
21	4, 20	mpi 20	. . 3 ⊢ (∀𝑥(∃𝑦 𝑦𝑅𝑥 → ∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥))) → ∃𝑦(𝑦 ∈ {∅} ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅})))
22		df-ral 3053	. . . . 5 ⊢ (∀𝑧 ∈ {∅} ¬ 𝑧 ∈ {∅} ↔ ∀𝑧(𝑧 ∈ {∅} → ¬ 𝑧 ∈ {∅}))
23		breq2 5103	. . . . . . . . 9 ⊢ (𝑦 = ∅ → (𝑧𝑅𝑦 ↔ 𝑧𝑅∅))
24	23, 12	bitrdi 287	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝑧𝑅𝑦 ↔ 𝑧 ∈ {∅}))
25	24	imbi1d 341	. . . . . . 7 ⊢ (𝑦 = ∅ → ((𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅}) ↔ (𝑧 ∈ {∅} → ¬ 𝑧 ∈ {∅})))
26	25	albidv 1922	. . . . . 6 ⊢ (𝑦 = ∅ → (∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅}) ↔ ∀𝑧(𝑧 ∈ {∅} → ¬ 𝑧 ∈ {∅})))
27	1, 26	rexsn 4640	. . . . 5 ⊢ (∃𝑦 ∈ {∅}∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅}) ↔ ∀𝑧(𝑧 ∈ {∅} → ¬ 𝑧 ∈ {∅}))
28		df-rex 3062	. . . . 5 ⊢ (∃𝑦 ∈ {∅}∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅}) ↔ ∃𝑦(𝑦 ∈ {∅} ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅})))
29	22, 27, 28	3bitr2ri 300	. . . 4 ⊢ (∃𝑦(𝑦 ∈ {∅} ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅})) ↔ ∀𝑧 ∈ {∅} ¬ 𝑧 ∈ {∅})
30		eleq1 2825	. . . . . 6 ⊢ (𝑧 = ∅ → (𝑧 ∈ {∅} ↔ ∅ ∈ {∅}))
31	30	notbid 318	. . . . 5 ⊢ (𝑧 = ∅ → (¬ 𝑧 ∈ {∅} ↔ ¬ ∅ ∈ {∅}))
32	1, 31	ralsn 4639	. . . 4 ⊢ (∀𝑧 ∈ {∅} ¬ 𝑧 ∈ {∅} ↔ ¬ ∅ ∈ {∅})
33	29, 32	bitri 275	. . 3 ⊢ (∃𝑦(𝑦 ∈ {∅} ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅})) ↔ ¬ ∅ ∈ {∅})
34	21, 33	sylib 218	. 2 ⊢ (∀𝑥(∃𝑦 𝑦𝑅𝑥 → ∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥))) → ¬ ∅ ∈ {∅})
35	2, 34	mt2 200	1 ⊢ ¬ ∀𝑥(∃𝑦 𝑦𝑅𝑥 → ∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∀wral 3052  ∃wrex 3061  Vcvv 3441   ∖ cdif 3899   ∪ cun 3900  ∅c0 4286  {csn 4581  {cpr 4583  ⟨cop 4587   class class class wbr 5099   I cid 5519   E cep 5524  ^◡ccnv 5624   ↾ cres 5627   ∘ ccom 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-eprel 5525  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501

This theorem is referenced by: (None)