Theorem bj-elid4

Description: Characterization of the elements of _I . (Contributed by BJ, 22-Jun-2019)

	Ref	Expression
Assertion	bj-elid4	$$⊢A\in \left(V\times W\right)\to \left(A\in \mathrm{I}\leftrightarrow 1^{st}\left(A\right)=2^{nd}\left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		1st2nd2	$$⊢A\in \left(V\times W\right)\to A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩$$
2		eleq1	$$⊢A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\to \left(A\in \mathrm{I}\leftrightarrow ⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\in \mathrm{I}\right)$$
3	2	adantl	$$⊢\left(A\in \left(V\times W\right)\wedge A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\right)\to \left(A\in \mathrm{I}\leftrightarrow ⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\in \mathrm{I}\right)$$
4		fvex	$$⊢2^{nd}\left(A\right)\in \mathrm{V}$$
5	4	inex2	$$⊢1^{st}\left(A\right)\cap 2^{nd}\left(A\right)\in \mathrm{V}$$
6		bj-opelid	$$⊢1^{st}\left(A\right)\cap 2^{nd}\left(A\right)\in \mathrm{V}\to \left(⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\in \mathrm{I}\leftrightarrow 1^{st}\left(A\right)=2^{nd}\left(A\right)\right)$$
7	5 6	mp1i	$$⊢\left(A\in \left(V\times W\right)\wedge A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\right)\to \left(⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\in \mathrm{I}\leftrightarrow 1^{st}\left(A\right)=2^{nd}\left(A\right)\right)$$
8	3 7	bitrd	$$⊢\left(A\in \left(V\times W\right)\wedge A=⟨1^{st}\left(A\right),2^{nd}\left(A\right)⟩\right)\to \left(A\in \mathrm{I}\leftrightarrow 1^{st}\left(A\right)=2^{nd}\left(A\right)\right)$$
9	1 8	mpdan	$$⊢A\in \left(V\times W\right)\to \left(A\in \mathrm{I}\leftrightarrow 1^{st}\left(A\right)=2^{nd}\left(A\right)\right)$$