Theorem brpermmodel 44966

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

Hypotheses

Ref	Expression
permmodel.1	⊢ 𝐹:V–1-1-onto→V
permmodel.2	⊢ 𝑅 = (◡𝐹 ∘ E )
brpermmodel.3	⊢ 𝐴 ∈ V
brpermmodel.4	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
brpermmodel	⊢ (𝐴𝑅𝐵 ↔ 𝐴 ∈ (𝐹‘𝐵))

Proof of Theorem brpermmodel

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		epel 5534	. . . 4 ⊢ (𝐴 E 𝑥 ↔ 𝐴 ∈ 𝑥)
2		vex 3448	. . . . 5 ⊢ 𝑥 ∈ V
3		brpermmodel.4	. . . . 5 ⊢ 𝐵 ∈ V
4	2, 3	brcnv 5836	. . . 4 ⊢ (𝑥◡𝐹𝐵 ↔ 𝐵𝐹𝑥)
5	1, 4	anbi12i 628	. . 3 ⊢ ((𝐴 E 𝑥 ∧ 𝑥◡𝐹𝐵) ↔ (𝐴 ∈ 𝑥 ∧ 𝐵𝐹𝑥))
6	5	exbii 1848	. 2 ⊢ (∃𝑥(𝐴 E 𝑥 ∧ 𝑥◡𝐹𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝐵𝐹𝑥))
7		permmodel.2	. . . 4 ⊢ 𝑅 = (◡𝐹 ∘ E )
8	7	breqi 5108	. . 3 ⊢ (𝐴𝑅𝐵 ↔ 𝐴(◡𝐹 ∘ E )𝐵)
9		brpermmodel.3	. . . 4 ⊢ 𝐴 ∈ V
10	9, 3	brco 5824	. . 3 ⊢ (𝐴(◡𝐹 ∘ E )𝐵 ↔ ∃𝑥(𝐴 E 𝑥 ∧ 𝑥◡𝐹𝐵))
11	8, 10	bitri 275	. 2 ⊢ (𝐴𝑅𝐵 ↔ ∃𝑥(𝐴 E 𝑥 ∧ 𝑥◡𝐹𝐵))
12		permmodel.1	. . . . 5 ⊢ 𝐹:V–1-1-onto→V
13		f1ofn 6783	. . . . 5 ⊢ (𝐹:V–1-1-onto→V → 𝐹 Fn V)
14	12, 13	ax-mp 5	. . . 4 ⊢ 𝐹 Fn V
15		fneu 6610	. . . 4 ⊢ ((𝐹 Fn V ∧ 𝐵 ∈ V) → ∃!𝑥 𝐵𝐹𝑥)
16	14, 3, 15	mp2an 692	. . 3 ⊢ ∃!𝑥 𝐵𝐹𝑥
17		eleq1 2816	. . . . . . 7 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
18	17	anbi1d 631	. . . . . 6 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝐵𝐹𝑥) ↔ (𝐴 ∈ 𝑥 ∧ 𝐵𝐹𝑥)))
19	18	exbidv 1921	. . . . 5 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝐵𝐹𝑥) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝐵𝐹𝑥)))
20	19	anbi1d 631	. . . 4 ⊢ (𝑦 = 𝐴 → ((∃𝑥(𝑦 ∈ 𝑥 ∧ 𝐵𝐹𝑥) ∧ ∃!𝑥 𝐵𝐹𝑥) ↔ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝐵𝐹𝑥) ∧ ∃!𝑥 𝐵𝐹𝑥)))
21		fv3 6858	. . . 4 ⊢ (𝐹‘𝐵) = {𝑦 ∣ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝐵𝐹𝑥) ∧ ∃!𝑥 𝐵𝐹𝑥)}
22	9, 20, 21	elab2 3646	. . 3 ⊢ (𝐴 ∈ (𝐹‘𝐵) ↔ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝐵𝐹𝑥) ∧ ∃!𝑥 𝐵𝐹𝑥))
23	16, 22	mpbiran2 710	. 2 ⊢ (𝐴 ∈ (𝐹‘𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝐵𝐹𝑥))
24	6, 11, 23	3bitr4i 303	1 ⊢ (𝐴𝑅𝐵 ↔ 𝐴 ∈ (𝐹‘𝐵))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∃!weu 2561  Vcvv 3444   class class class wbr 5102   E cep 5530  ^◡ccnv 5630   ∘ ccom 5635   Fn wfn 6494  –1-1-onto→wf1o 6498  ‘cfv 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-id 5526  df-eprel 5531  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-f1o 6506  df-fv 6507

This theorem is referenced by:  brpermmodelcnv  44967  permaxext  44968  permaxrep  44969  permaxsep  44970  permaxpow  44972  permaxun  44974  permaxinf2lem  44975  permac8prim  44977  nregmodellem  44979