Theorem nregmodel 45531

Description: The Axiom of Regularity ax-reg 9526 is false in the permutation model defined from 𝐹. Since the other axioms of ZFC hold in all permutation models (permaxext 45519 through permac8prim 45528), 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 45507 through wfac8prim 45516), 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 5247	. . 3 ⊢ ∅ ∈ V
2	1	snid 4611	. 2 ⊢ ∅ ∈ {∅}
3		eleq1 2840	. . . . 5 ⊢ (𝑦 = ∅ → (𝑦 ∈ {∅} ↔ ∅ ∈ {∅}))
4	1, 3, 2	ceqsexv2d 3493	. . . 4 ⊢ ∃𝑦 𝑦 ∈ {∅}
5		breq2 5094	. . . . . . . 8 ⊢ (𝑥 = ∅ → (𝑦𝑅𝑥 ↔ 𝑦𝑅∅))
6		nregmodel.1	. . . . . . . . 9 ⊢ 𝐹 = (( I ↾ (V ∖ {∅, {∅}})) ∪ {⟨∅, {∅}⟩, ⟨{∅}, ∅⟩})
7		nregmodel.2	. . . . . . . . 9 ⊢ 𝑅 = (◡𝐹 ∘ E )
8	6, 7	nregmodellem 45530	. . . . . . . 8 ⊢ (𝑦𝑅∅ ↔ 𝑦 ∈ {∅})
9	5, 8	bitrdi 289	. . . . . . 7 ⊢ (𝑥 = ∅ → (𝑦𝑅𝑥 ↔ 𝑦 ∈ {∅}))
10	9	exbidv 1931	. . . . . 6 ⊢ (𝑥 = ∅ → (∃𝑦 𝑦𝑅𝑥 ↔ ∃𝑦 𝑦 ∈ {∅}))
11		breq2 5094	. . . . . . . . . . . 12 ⊢ (𝑥 = ∅ → (𝑧𝑅𝑥 ↔ 𝑧𝑅∅))
12	6, 7	nregmodellem 45530	. . . . . . . . . . . 12 ⊢ (𝑧𝑅∅ ↔ 𝑧 ∈ {∅})
13	11, 12	bitrdi 289	. . . . . . . . . . 11 ⊢ (𝑥 = ∅ → (𝑧𝑅𝑥 ↔ 𝑧 ∈ {∅}))
14	13	notbid 320	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → (¬ 𝑧𝑅𝑥 ↔ ¬ 𝑧 ∈ {∅}))
15	14	imbi2d 342	. . . . . . . . 9 ⊢ (𝑥 = ∅ → ((𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥) ↔ (𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅})))
16	15	albidv 1930	. . . . . . . 8 ⊢ (𝑥 = ∅ → (∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥) ↔ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅})))
17	9, 16	anbi12d 640	. . . . . . 7 ⊢ (𝑥 = ∅ → ((𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥)) ↔ (𝑦 ∈ {∅} ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅}))))
18	17	exbidv 1931	. . . . . 6 ⊢ (𝑥 = ∅ → (∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥)) ↔ ∃𝑦(𝑦 ∈ {∅} ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅}))))
19	10, 18	imbi12d 346	. . . . 5 ⊢ (𝑥 = ∅ → ((∃𝑦 𝑦𝑅𝑥 → ∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥))) ↔ (∃𝑦 𝑦 ∈ {∅} → ∃𝑦(𝑦 ∈ {∅} ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅})))))
20	1, 19	spcv 3555	. . . 4 ⊢ (∀𝑥(∃𝑦 𝑦𝑅𝑥 → ∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥))) → (∃𝑦 𝑦 ∈ {∅} → ∃𝑦(𝑦 ∈ {∅} ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅}))))
21	4, 20	mpi 20	. . 3 ⊢ (∀𝑥(∃𝑦 𝑦𝑅𝑥 → ∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥))) → ∃𝑦(𝑦 ∈ {∅} ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅})))
22		df-ral 3067	. . . . 5 ⊢ (∀𝑧 ∈ {∅} ¬ 𝑧 ∈ {∅} ↔ ∀𝑧(𝑧 ∈ {∅} → ¬ 𝑧 ∈ {∅}))
23		breq2 5094	. . . . . . . . 9 ⊢ (𝑦 = ∅ → (𝑧𝑅𝑦 ↔ 𝑧𝑅∅))
24	23, 12	bitrdi 289	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝑧𝑅𝑦 ↔ 𝑧 ∈ {∅}))
25	24	imbi1d 343	. . . . . . 7 ⊢ (𝑦 = ∅ → ((𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅}) ↔ (𝑧 ∈ {∅} → ¬ 𝑧 ∈ {∅})))
26	25	albidv 1930	. . . . . 6 ⊢ (𝑦 = ∅ → (∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅}) ↔ ∀𝑧(𝑧 ∈ {∅} → ¬ 𝑧 ∈ {∅})))
27	1, 26	rexsn 4631	. . . . 5 ⊢ (∃𝑦 ∈ {∅}∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅}) ↔ ∀𝑧(𝑧 ∈ {∅} → ¬ 𝑧 ∈ {∅}))
28		df-rex 3077	. . . . 5 ⊢ (∃𝑦 ∈ {∅}∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅}) ↔ ∃𝑦(𝑦 ∈ {∅} ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅})))
29	22, 27, 28	3bitr2ri 302	. . . 4 ⊢ (∃𝑦(𝑦 ∈ {∅} ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅})) ↔ ∀𝑧 ∈ {∅} ¬ 𝑧 ∈ {∅})
30		eleq1 2840	. . . . . 6 ⊢ (𝑧 = ∅ → (𝑧 ∈ {∅} ↔ ∅ ∈ {∅}))
31	30	notbid 320	. . . . 5 ⊢ (𝑧 = ∅ → (¬ 𝑧 ∈ {∅} ↔ ¬ ∅ ∈ {∅}))
32	1, 31	ralsn 4630	. . . 4 ⊢ (∀𝑧 ∈ {∅} ¬ 𝑧 ∈ {∅} ↔ ¬ ∅ ∈ {∅})
33	29, 32	bitri 277	. . 3 ⊢ (∃𝑦(𝑦 ∈ {∅} ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ {∅})) ↔ ¬ ∅ ∈ {∅})
34	21, 33	sylib 220	. 2 ⊢ (∀𝑥(∃𝑦 𝑦𝑅𝑥 → ∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥))) → ¬ ∅ ∈ {∅})
35	2, 34	mt2 202	1 ⊢ ¬ ∀𝑥(∃𝑦 𝑦𝑅𝑥 → ∃𝑦(𝑦𝑅𝑥 ∧ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧𝑅𝑥)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398  ∀wal 1548   = wceq 1550  ∃wex 1789   ∈ wcel 2132  ∀wral 3066  ∃wrex 3076  Vcvv 3444   ∖ cdif 3892   ∪ cun 3893  ∅c0 4276  {csn 4572  {cpr 4574  ⟨cop 4578   class class class wbr 5090   I cid 5530   E cep 5535  ^◡ccnv 5635   ↾ cres 5638   ∘ ccom 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pr 5380

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-ral 3067  df-rex 3077  df-reu 3358  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-eprel 5536  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514

This theorem is referenced by: (None)