Metamath Proof Explorer

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 ⊢ F : V ⟶ 1-1 onto V
permmodel.2 ⊢ R = F -1 ∘ E
brpermmodel.3 ⊢ A ∈ V
brpermmodel.4 ⊢ B ∈ V
Assertion brpermmodel ⊢ A R B ↔ A ∈ F ⁡ B

Proof

Step Hyp Ref Expression
1 permmodel.1 ⊢ F : V ⟶ 1-1 onto V
2 permmodel.2 ⊢ R = F -1 ∘ E
3 brpermmodel.3 ⊢ A ∈ V
4 brpermmodel.4 ⊢ B ∈ V
5 epel ⊢ A E x ↔ A ∈ x
6 vex ⊢ x ∈ V
7 6 4 brcnv ⊢ x F -1 B ↔ B F x
8 5 7 anbi12i ⊢ A E x ∧ x F -1 B ↔ A ∈ x ∧ B F x
9 8 exbii ⊢ ∃ x A E x ∧ x F -1 B ↔ ∃ x A ∈ x ∧ B F x
10 2 breqi ⊢ A R B ↔ A F -1 ∘ E B
11 3 4 brco ⊢ A F -1 ∘ E B ↔ ∃ x A E x ∧ x F -1 B
12 10 11 bitri ⊢ A R B ↔ ∃ x A E x ∧ x F -1 B
13 f1ofn ⊢ F : V ⟶ 1-1 onto V → F Fn V
14 1 13 ax-mp ⊢ F Fn V
15 fneu ⊢ F Fn V ∧ B ∈ V → ∃! x B F x
16 14 4 15 mp2an ⊢ ∃! x B F x
17 eleq1 ⊢ y = A → y ∈ x ↔ A ∈ x
18 17 anbi1d ⊢ y = A → y ∈ x ∧ B F x ↔ A ∈ x ∧ B F x
19 18 exbidv ⊢ y = A → ∃ x y ∈ x ∧ B F x ↔ ∃ x A ∈ x ∧ B F x
20 19 anbi1d ⊢ y = A → ∃ x y ∈ x ∧ B F x ∧ ∃! x B F x ↔ ∃ x A ∈ x ∧ B F x ∧ ∃! x B F x
21 fv3 ⊢ F ⁡ B = y | ∃ x y ∈ x ∧ B F x ∧ ∃! x B F x
22 3 20 21 elab2 ⊢ A ∈ F ⁡ B ↔ ∃ x A ∈ x ∧ B F x ∧ ∃! x B F x
23 16 22 mpbiran2 ⊢ A ∈ F ⁡ B ↔ ∃ x A ∈ x ∧ B F x
24 9 12 23 3bitr4i ⊢ A R B ↔ A ∈ F ⁡ B