Theorem nregmodellem

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

	Ref	Expression
Hypotheses	nregmodel.1	⊢ 𝐹 = ( ( I ↾ ( V ∖ { ∅ , { ∅ } } ) ) ∪ { ⟨ ∅ , { ∅ } ⟩ , ⟨ { ∅ } , ∅ ⟩ } )
	nregmodel.2	⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
Assertion	nregmodellem	⊢ ( 𝑥 𝑅 ∅ ↔ 𝑥 ∈ { ∅ } )

Proof

Step	Hyp	Ref	Expression
1		nregmodel.1	⊢ 𝐹 = ( ( I ↾ ( V ∖ { ∅ , { ∅ } } ) ) ∪ { ⟨ ∅ , { ∅ } ⟩ , ⟨ { ∅ } , ∅ ⟩ } )
2		nregmodel.2	⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
3	1	nregmodelf1o	⊢ 𝐹 : V –1-1-onto→ V
4		vex	⊢ 𝑥 ∈ V
5		0ex	⊢ ∅ ∈ V
6	3 2 4 5	brpermmodel	⊢ ( 𝑥 𝑅 ∅ ↔ 𝑥 ∈ ( 𝐹 ‘ ∅ ) )
7		f1ofun	⊢ ( 𝐹 : V –1-1-onto→ V → Fun 𝐹 )
8	3 7	ax-mp	⊢ Fun 𝐹
9		opex	⊢ ⟨ ∅ , { ∅ } ⟩ ∈ V
10	9	prid1	⊢ ⟨ ∅ , { ∅ } ⟩ ∈ { ⟨ ∅ , { ∅ } ⟩ , ⟨ { ∅ } , ∅ ⟩ }
11		elun2	⊢ ( ⟨ ∅ , { ∅ } ⟩ ∈ { ⟨ ∅ , { ∅ } ⟩ , ⟨ { ∅ } , ∅ ⟩ } → ⟨ ∅ , { ∅ } ⟩ ∈ ( ( I ↾ ( V ∖ { ∅ , { ∅ } } ) ) ∪ { ⟨ ∅ , { ∅ } ⟩ , ⟨ { ∅ } , ∅ ⟩ } ) )
12	10 11	ax-mp	⊢ ⟨ ∅ , { ∅ } ⟩ ∈ ( ( I ↾ ( V ∖ { ∅ , { ∅ } } ) ) ∪ { ⟨ ∅ , { ∅ } ⟩ , ⟨ { ∅ } , ∅ ⟩ } )
13	12 1	eleqtrri	⊢ ⟨ ∅ , { ∅ } ⟩ ∈ 𝐹
14		funopfv	⊢ ( Fun 𝐹 → ( ⟨ ∅ , { ∅ } ⟩ ∈ 𝐹 → ( 𝐹 ‘ ∅ ) = { ∅ } ) )
15	8 13 14	mp2	⊢ ( 𝐹 ‘ ∅ ) = { ∅ }
16	15	eleq2i	⊢ ( 𝑥 ∈ ( 𝐹 ‘ ∅ ) ↔ 𝑥 ∈ { ∅ } )
17	6 16	bitri	⊢ ( 𝑥 𝑅 ∅ ↔ 𝑥 ∈ { ∅ } )