Theorem brpermmodel

Description: The membership relation in a permutation model. We use a permutation F of the universe to define a relation R 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 F 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)

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

Proof

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