Theorem bj-imdiridlem

Description: Lemma for bj-imdirid and bj-iminvid . (Contributed by BJ, 26-May-2024)

	Ref	Expression
Hypothesis	bj-imdiridlem.1	$$⊢\left(x\subseteq A\wedge y\subseteq A\right)\to \left(\phi \leftrightarrow x=y\right)$$
Assertion	bj-imdiridlem	$$⊢\left\{⟨x,y⟩|\left(\left(x\subseteq A\wedge y\subseteq A\right)\wedge \phi \right)\right\}={\mathrm{I}\upharpoonright }_{𝒫A}$$

Proof

Step	Hyp	Ref	Expression
1		bj-imdiridlem.1	$$⊢\left(x\subseteq A\wedge y\subseteq A\right)\to \left(\phi \leftrightarrow x=y\right)$$
2	1	biimp3a	$$⊢\left(x\subseteq A\wedge y\subseteq A\wedge \phi \right)\to x=y$$
3	2	3expib	$$⊢x\subseteq A\to \left(\left(y\subseteq A\wedge \phi \right)\to x=y\right)$$
4		equcomi	$$⊢x=y\to y=x$$
5	4	sseq1d	$$⊢x=y\to \left(y\subseteq A\leftrightarrow x\subseteq A\right)$$
6	5	biimparc	$$⊢\left(x\subseteq A\wedge x=y\right)\to y\subseteq A$$
7		simpr	$$⊢\left(\left(x\subseteq A\wedge x=y\right)\wedge y\subseteq A\right)\to y\subseteq A$$
8	1	biimpar	$$⊢\left(\left(x\subseteq A\wedge y\subseteq A\right)\wedge x=y\right)\to \phi$$
9	8	an32s	$$⊢\left(\left(x\subseteq A\wedge x=y\right)\wedge y\subseteq A\right)\to \phi$$
10	7 9	jca	$$⊢\left(\left(x\subseteq A\wedge x=y\right)\wedge y\subseteq A\right)\to \left(y\subseteq A\wedge \phi \right)$$
11	6 10	mpdan	$$⊢\left(x\subseteq A\wedge x=y\right)\to \left(y\subseteq A\wedge \phi \right)$$
12	11	ex	$$⊢x\subseteq A\to \left(x=y\to \left(y\subseteq A\wedge \phi \right)\right)$$
13	3 12	impbid	$$⊢x\subseteq A\to \left(\left(y\subseteq A\wedge \phi \right)\leftrightarrow x=y\right)$$
14	13	pm5.32i	$$⊢\left(x\subseteq A\wedge \left(y\subseteq A\wedge \phi \right)\right)\leftrightarrow \left(x\subseteq A\wedge x=y\right)$$
15		anass	$$⊢\left(\left(x\subseteq A\wedge y\subseteq A\right)\wedge \phi \right)\leftrightarrow \left(x\subseteq A\wedge \left(y\subseteq A\wedge \phi \right)\right)$$
16		velpw	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$
17		vex	$$⊢y\in \mathrm{V}$$
18	17	ideq	$$⊢x\mathrm{I}y\leftrightarrow x=y$$
19	16 18	anbi12i	$$⊢\left(x\in 𝒫A\wedge x\mathrm{I}y\right)\leftrightarrow \left(x\subseteq A\wedge x=y\right)$$
20	14 15 19	3bitr4i	$$⊢\left(\left(x\subseteq A\wedge y\subseteq A\right)\wedge \phi \right)\leftrightarrow \left(x\in 𝒫A\wedge x\mathrm{I}y\right)$$
21	20	opabbii	$$⊢\left\{⟨x,y⟩|\left(\left(x\subseteq A\wedge y\subseteq A\right)\wedge \phi \right)\right\}=\left\{⟨x,y⟩|\left(x\in 𝒫A\wedge x\mathrm{I}y\right)\right\}$$
22		dfres2	$$⊢{\mathrm{I}\upharpoonright }_{𝒫A}=\left\{⟨x,y⟩|\left(x\in 𝒫A\wedge x\mathrm{I}y\right)\right\}$$
23	21 22	eqtr4i	$$⊢\left\{⟨x,y⟩|\left(\left(x\subseteq A\wedge y\subseteq A\right)\wedge \phi \right)\right\}={\mathrm{I}\upharpoonright }_{𝒫A}$$