Theorem brpermmodelcnv

Description: Ordinary membership expressed in terms of the permutation model's membership relation. (Contributed by Eric Schmidt, 6-Nov-2025)

	Ref	Expression
Hypotheses	permmodel.1	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
	permmodel.2	$$⊢R=F^{-1}\circ \mathrm{E}$$
	brpermmodel.3	$$⊢A\in \mathrm{V}$$
	brpermmodel.4	$$⊢B\in \mathrm{V}$$
Assertion	brpermmodelcnv	$$⊢AR{F}^{-1}\left(B\right)\leftrightarrow A\in B$$

Proof

Step	Hyp	Ref	Expression
1		permmodel.1	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
2		permmodel.2	$$⊢R=F^{-1}\circ \mathrm{E}$$
3		brpermmodel.3	$$⊢A\in \mathrm{V}$$
4		brpermmodel.4	$$⊢B\in \mathrm{V}$$
5		fvex	$$⊢F^{-1}\left(B\right)\in \mathrm{V}$$
6	1 2 3 5	brpermmodel	$$⊢AR{F}^{-1}\left(B\right)\leftrightarrow A\in F\left(F^{-1}\left(B\right)\right)$$
7		f1ocnvfv2	$$⊢\left(F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}\wedge B\in \mathrm{V}\right)\to F\left(F^{-1}\left(B\right)\right)=B$$
8	1 4 7	mp2an	$$⊢F\left(F^{-1}\left(B\right)\right)=B$$
9	8	eleq2i	$$⊢A\in F\left(F^{-1}\left(B\right)\right)\leftrightarrow A\in B$$
10	6 9	bitri	$$⊢AR{F}^{-1}\left(B\right)\leftrightarrow A\in B$$