Theorem brpermmodel 44986

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 5543	. . . 4 ⊢ (𝐴 E 𝑥 ↔ 𝐴 ∈ 𝑥)
2		vex 3454	. . . . 5 ⊢ 𝑥 ∈ V
3		brpermmodel.4	. . . . 5 ⊢ 𝐵 ∈ V
4	2, 3	brcnv 5848	. . . 4 ⊢ (𝑥◡𝐹𝐵 ↔ 𝐵𝐹𝑥)
5	1, 4	anbi12i 628	. . 3 ⊢ ((𝐴 E 𝑥 ∧ 𝑥◡𝐹𝐵) ↔ (𝐴 ∈ 𝑥 ∧ 𝐵𝐹𝑥))
6	5	exbii 1848	. 2 ⊢ (∃𝑥(𝐴 E 𝑥 ∧ 𝑥◡𝐹𝐵) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝐵𝐹𝑥))
7		permmodel.2	. . . 4 ⊢ 𝑅 = (◡𝐹 ∘ E )
8	7	breqi 5115	. . 3 ⊢ (𝐴𝑅𝐵 ↔ 𝐴(◡𝐹 ∘ E )𝐵)
9		brpermmodel.3	. . . 4 ⊢ 𝐴 ∈ V
10	9, 3	brco 5836	. . 3 ⊢ (𝐴(◡𝐹 ∘ E )𝐵 ↔ ∃𝑥(𝐴 E 𝑥 ∧ 𝑥◡𝐹𝐵))
11	8, 10	bitri 275	. 2 ⊢ (𝐴𝑅𝐵 ↔ ∃𝑥(𝐴 E 𝑥 ∧ 𝑥◡𝐹𝐵))
12		permmodel.1	. . . . 5 ⊢ 𝐹:V–1-1-onto→V
13		f1ofn 6803	. . . . 5 ⊢ (𝐹:V–1-1-onto→V → 𝐹 Fn V)
14	12, 13	ax-mp 5	. . . 4 ⊢ 𝐹 Fn V
15		fneu 6630	. . . 4 ⊢ ((𝐹 Fn V ∧ 𝐵 ∈ V) → ∃!𝑥 𝐵𝐹𝑥)
16	14, 3, 15	mp2an 692	. . 3 ⊢ ∃!𝑥 𝐵𝐹𝑥
17		eleq1 2817	. . . . . . 7 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
18	17	anbi1d 631	. . . . . 6 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝑥 ∧ 𝐵𝐹𝑥) ↔ (𝐴 ∈ 𝑥 ∧ 𝐵𝐹𝑥)))
19	18	exbidv 1921	. . . . 5 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝐵𝐹𝑥) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝐵𝐹𝑥)))
20	19	anbi1d 631	. . . 4 ⊢ (𝑦 = 𝐴 → ((∃𝑥(𝑦 ∈ 𝑥 ∧ 𝐵𝐹𝑥) ∧ ∃!𝑥 𝐵𝐹𝑥) ↔ (∃𝑥(𝐴 ∈ 𝑥 ∧ 𝐵𝐹𝑥) ∧ ∃!𝑥 𝐵𝐹𝑥)))
21		fv3 6878	. . . 4 ⊢ (𝐹‘𝐵) = {𝑦 ∣ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝐵𝐹𝑥) ∧ ∃!𝑥 𝐵𝐹𝑥)}
22	9, 20, 21	elab2 3651	. . 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 2562  Vcvv 3450   class class class wbr 5109   E cep 5539  ^◡ccnv 5639   ∘ ccom 5644   Fn wfn 6508  –1-1-onto→wf1o 6512  ‘cfv 6513

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 2702  ax-sep 5253  ax-nul 5263  ax-pr 5389

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-id 5535  df-eprel 5540  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-f1 6518  df-f1o 6520  df-fv 6521

This theorem is referenced by:  brpermmodelcnv  44987  permaxext  44988  permaxrep  44989  permaxsep  44990  permaxpow  44992  permaxun  44994  permaxinf2lem  44995  permac8prim  44997  nregmodellem  44999