Theorem eloprabi

Description: A consequence of membership in an operation class abstraction, using ordered pair extractors. (Contributed by NM, 6-Nov-2006) (Revised by David Abernethy, 19-Jun-2012)

	Ref	Expression
Hypotheses	eloprabi.1	$$⊢x=1^{st}\left(1^{st}\left(A\right)\right)\to \left(\phi \leftrightarrow \psi \right)$$
	eloprabi.2	$$⊢y=2^{nd}\left(1^{st}\left(A\right)\right)\to \left(\psi \leftrightarrow \chi \right)$$
	eloprabi.3	$$⊢z=2^{nd}\left(A\right)\to \left(\chi \leftrightarrow \theta \right)$$
Assertion	eloprabi	$$⊢A\in \left\{⟨⟨x,y⟩,z⟩|\phi \right\}\to \theta$$

Proof

Step	Hyp	Ref	Expression
1		eloprabi.1	$$⊢x=1^{st}\left(1^{st}\left(A\right)\right)\to \left(\phi \leftrightarrow \psi \right)$$
2		eloprabi.2	$$⊢y=2^{nd}\left(1^{st}\left(A\right)\right)\to \left(\psi \leftrightarrow \chi \right)$$
3		eloprabi.3	$$⊢z=2^{nd}\left(A\right)\to \left(\chi \leftrightarrow \theta \right)$$
4		eqeq1	$$⊢w=A\to \left(w=⟨⟨x,y⟩,z⟩\leftrightarrow A=⟨⟨x,y⟩,z⟩\right)$$
5	4	anbi1d	$$⊢w=A\to \left(\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)\leftrightarrow \left(A=⟨⟨x,y⟩,z⟩\wedge \phi \right)\right)$$
6	5	3exbidv	$$⊢w=A\to \left(\exists x\exists y\exists z\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\exists z\left(A=⟨⟨x,y⟩,z⟩\wedge \phi \right)\right)$$
7		df-oprab	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{w|\exists x\exists y\exists z\left(w=⟨⟨x,y⟩,z⟩\wedge \phi \right)\right\}$$
8	6 7	elab2g	$$⊢A\in \left\{⟨⟨x,y⟩,z⟩|\phi \right\}\to \left(A\in \left\{⟨⟨x,y⟩,z⟩|\phi \right\}\leftrightarrow \exists x\exists y\exists z\left(A=⟨⟨x,y⟩,z⟩\wedge \phi \right)\right)$$
9	8	ibi	$$⊢A\in \left\{⟨⟨x,y⟩,z⟩|\phi \right\}\to \exists x\exists y\exists z\left(A=⟨⟨x,y⟩,z⟩\wedge \phi \right)$$
10		opex	$$⊢⟨x,y⟩\in \mathrm{V}$$
11		vex	$$⊢z\in \mathrm{V}$$
12	10 11	op1std	$$⊢A=⟨⟨x,y⟩,z⟩\to 1^{st}\left(A\right)=⟨x,y⟩$$
13	12	fveq2d	$$⊢A=⟨⟨x,y⟩,z⟩\to 1^{st}\left(1^{st}\left(A\right)\right)=1^{st}\left(⟨x,y⟩\right)$$
14		vex	$$⊢x\in \mathrm{V}$$
15		vex	$$⊢y\in \mathrm{V}$$
16	14 15	op1st	$$⊢1^{st}\left(⟨x,y⟩\right)=x$$
17	13 16	eqtr2di	$$⊢A=⟨⟨x,y⟩,z⟩\to x=1^{st}\left(1^{st}\left(A\right)\right)$$
18	17 1	syl	$$⊢A=⟨⟨x,y⟩,z⟩\to \left(\phi \leftrightarrow \psi \right)$$
19	12	fveq2d	$$⊢A=⟨⟨x,y⟩,z⟩\to 2^{nd}\left(1^{st}\left(A\right)\right)=2^{nd}\left(⟨x,y⟩\right)$$
20	14 15	op2nd	$$⊢2^{nd}\left(⟨x,y⟩\right)=y$$
21	19 20	eqtr2di	$$⊢A=⟨⟨x,y⟩,z⟩\to y=2^{nd}\left(1^{st}\left(A\right)\right)$$
22	21 2	syl	$$⊢A=⟨⟨x,y⟩,z⟩\to \left(\psi \leftrightarrow \chi \right)$$
23	10 11	op2ndd	$$⊢A=⟨⟨x,y⟩,z⟩\to 2^{nd}\left(A\right)=z$$
24	23	eqcomd	$$⊢A=⟨⟨x,y⟩,z⟩\to z=2^{nd}\left(A\right)$$
25	24 3	syl	$$⊢A=⟨⟨x,y⟩,z⟩\to \left(\chi \leftrightarrow \theta \right)$$
26	18 22 25	3bitrd	$$⊢A=⟨⟨x,y⟩,z⟩\to \left(\phi \leftrightarrow \theta \right)$$
27	26	biimpa	$$⊢\left(A=⟨⟨x,y⟩,z⟩\wedge \phi \right)\to \theta$$
28	27	exlimiv	$$⊢\exists z\left(A=⟨⟨x,y⟩,z⟩\wedge \phi \right)\to \theta$$
29	28	exlimiv	$$⊢\exists y\exists z\left(A=⟨⟨x,y⟩,z⟩\wedge \phi \right)\to \theta$$
30	29	exlimiv	$$⊢\exists x\exists y\exists z\left(A=⟨⟨x,y⟩,z⟩\wedge \phi \right)\to \theta$$
31	9 30	syl	$$⊢A\in \left\{⟨⟨x,y⟩,z⟩|\phi \right\}\to \theta$$