Theorem nregmodellem

Description: Lemma for nregmodel . (Contributed by Eric Schmidt, 16-Nov-2025)

	Ref	Expression
Hypotheses	nregmodel.1	$$⊢F=\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)}\right)\cup \left\{⟨\varnothing ,\left\{\varnothing \right\}⟩,⟨\left\{\varnothing \right\},\varnothing ⟩\right\}$$
	nregmodel.2	$$⊢R=F^{-1}\circ \mathrm{E}$$
Assertion	nregmodellem	$$⊢xR\varnothing \leftrightarrow x\in \left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		nregmodel.1	$$⊢F=\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)}\right)\cup \left\{⟨\varnothing ,\left\{\varnothing \right\}⟩,⟨\left\{\varnothing \right\},\varnothing ⟩\right\}$$
2		nregmodel.2	$$⊢R=F^{-1}\circ \mathrm{E}$$
3	1	nregmodelf1o	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
4		vex	$$⊢x\in \mathrm{V}$$
5		0ex	$$⊢\varnothing \in \mathrm{V}$$
6	3 2 4 5	brpermmodel	$$⊢xR\varnothing \leftrightarrow x\in F\left(\varnothing \right)$$
7		f1ofun	$$⊢F:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}\to \mathrm{Fun}F$$
8	3 7	ax-mp	$$⊢\mathrm{Fun}F$$
9		opex	$$⊢⟨\varnothing ,\left\{\varnothing \right\}⟩\in \mathrm{V}$$
10	9	prid1	$$⊢⟨\varnothing ,\left\{\varnothing \right\}⟩\in \left\{⟨\varnothing ,\left\{\varnothing \right\}⟩,⟨\left\{\varnothing \right\},\varnothing ⟩\right\}$$
11		elun2	$$⊢⟨\varnothing ,\left\{\varnothing \right\}⟩\in \left\{⟨\varnothing ,\left\{\varnothing \right\}⟩,⟨\left\{\varnothing \right\},\varnothing ⟩\right\}\to ⟨\varnothing ,\left\{\varnothing \right\}⟩\in \left(\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)}\right)\cup \left\{⟨\varnothing ,\left\{\varnothing \right\}⟩,⟨\left\{\varnothing \right\},\varnothing ⟩\right\}\right)$$
12	10 11	ax-mp	$$⊢⟨\varnothing ,\left\{\varnothing \right\}⟩\in \left(\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{V}\setminus \left\{\varnothing ,\left\{\varnothing \right\}\right\}\right)}\right)\cup \left\{⟨\varnothing ,\left\{\varnothing \right\}⟩,⟨\left\{\varnothing \right\},\varnothing ⟩\right\}\right)$$
13	12 1	eleqtrri	$$⊢⟨\varnothing ,\left\{\varnothing \right\}⟩\in F$$
14		funopfv	$$⊢\mathrm{Fun}F\to \left(⟨\varnothing ,\left\{\varnothing \right\}⟩\in F\to F\left(\varnothing \right)=\left\{\varnothing \right\}\right)$$
15	8 13 14	mp2	$$⊢F\left(\varnothing \right)=\left\{\varnothing \right\}$$
16	15	eleq2i	$$⊢x\in F\left(\varnothing \right)\leftrightarrow x\in \left\{\varnothing \right\}$$
17	6 16	bitri	$$⊢xR\varnothing \leftrightarrow x\in \left\{\varnothing \right\}$$