Theorem elintima

Description: Element of intersection of images. (Contributed by RP, 13-Apr-2020)

	Ref	Expression
Assertion	elintima	$$⊢y\in \bigcap \left\{x|\exists a\in Ax=a\left[B\right]\right\}\leftrightarrow \forall a\in A\exists b\in B⟨b,y⟩\in a$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢y\in \mathrm{V}$$
2	1	elint2	$$⊢y\in \bigcap \left\{x|\exists a\in Ax=a\left[B\right]\right\}\leftrightarrow \forall z\in \left\{x|\exists a\in Ax=a\left[B\right]\right\}y\in z$$
3		elequ2	$$⊢z=x\to \left(y\in z\leftrightarrow y\in x\right)$$
4	3	ralab2	$$⊢\forall z\in \left\{x|\exists a\in Ax=a\left[B\right]\right\}y\in z\leftrightarrow \forall x\left(\exists a\in Ax=a\left[B\right]\to y\in x\right)$$
5		df-rex	$$⊢\exists a\in Ax=a\left[B\right]\leftrightarrow \exists a\left(a\in A\wedge x=a\left[B\right]\right)$$
6	5	imbi1i	$$⊢\left(\exists a\in Ax=a\left[B\right]\to y\in x\right)\leftrightarrow \left(\exists a\left(a\in A\wedge x=a\left[B\right]\right)\to y\in x\right)$$
7		19.23v	$$⊢\forall a\left(\left(a\in A\wedge x=a\left[B\right]\right)\to y\in x\right)\leftrightarrow \left(\exists a\left(a\in A\wedge x=a\left[B\right]\right)\to y\in x\right)$$
8		simpr	$$⊢\left(a\in A\wedge x=a\left[B\right]\right)\to x=a\left[B\right]$$
9	8	eleq2d	$$⊢\left(a\in A\wedge x=a\left[B\right]\right)\to \left(y\in x\leftrightarrow y\in a\left[B\right]\right)$$
10	9	pm5.74i	$$⊢\left(\left(a\in A\wedge x=a\left[B\right]\right)\to y\in x\right)\leftrightarrow \left(\left(a\in A\wedge x=a\left[B\right]\right)\to y\in a\left[B\right]\right)$$
11	1	elima	$$⊢y\in a\left[B\right]\leftrightarrow \exists b\in Bbay$$
12		df-br	$$⊢bay\leftrightarrow ⟨b,y⟩\in a$$
13	12	rexbii	$$⊢\exists b\in Bbay\leftrightarrow \exists b\in B⟨b,y⟩\in a$$
14	11 13	bitri	$$⊢y\in a\left[B\right]\leftrightarrow \exists b\in B⟨b,y⟩\in a$$
15	14	imbi2i	$$⊢\left(\left(a\in A\wedge x=a\left[B\right]\right)\to y\in a\left[B\right]\right)\leftrightarrow \left(\left(a\in A\wedge x=a\left[B\right]\right)\to \exists b\in B⟨b,y⟩\in a\right)$$
16	10 15	bitri	$$⊢\left(\left(a\in A\wedge x=a\left[B\right]\right)\to y\in x\right)\leftrightarrow \left(\left(a\in A\wedge x=a\left[B\right]\right)\to \exists b\in B⟨b,y⟩\in a\right)$$
17	16	albii	$$⊢\forall a\left(\left(a\in A\wedge x=a\left[B\right]\right)\to y\in x\right)\leftrightarrow \forall a\left(\left(a\in A\wedge x=a\left[B\right]\right)\to \exists b\in B⟨b,y⟩\in a\right)$$
18	6 7 17	3bitr2i	$$⊢\left(\exists a\in Ax=a\left[B\right]\to y\in x\right)\leftrightarrow \forall a\left(\left(a\in A\wedge x=a\left[B\right]\right)\to \exists b\in B⟨b,y⟩\in a\right)$$
19	18	albii	$$⊢\forall x\left(\exists a\in Ax=a\left[B\right]\to y\in x\right)\leftrightarrow \forall x\forall a\left(\left(a\in A\wedge x=a\left[B\right]\right)\to \exists b\in B⟨b,y⟩\in a\right)$$
20		19.23v	$$⊢\forall x\left(\left(a\in A\wedge x=a\left[B\right]\right)\to \exists b\in B⟨b,y⟩\in a\right)\leftrightarrow \left(\exists x\left(a\in A\wedge x=a\left[B\right]\right)\to \exists b\in B⟨b,y⟩\in a\right)$$
21		vex	$$⊢a\in \mathrm{V}$$
22	21	imaex	$$⊢a\left[B\right]\in \mathrm{V}$$
23	22	isseti	$$⊢\exists xx=a\left[B\right]$$
24		19.42v	$$⊢\exists x\left(a\in A\wedge x=a\left[B\right]\right)\leftrightarrow \left(a\in A\wedge \exists xx=a\left[B\right]\right)$$
25	23 24	mpbiran2	$$⊢\exists x\left(a\in A\wedge x=a\left[B\right]\right)\leftrightarrow a\in A$$
26	25	imbi1i	$$⊢\left(\exists x\left(a\in A\wedge x=a\left[B\right]\right)\to \exists b\in B⟨b,y⟩\in a\right)\leftrightarrow \left(a\in A\to \exists b\in B⟨b,y⟩\in a\right)$$
27	20 26	bitri	$$⊢\forall x\left(\left(a\in A\wedge x=a\left[B\right]\right)\to \exists b\in B⟨b,y⟩\in a\right)\leftrightarrow \left(a\in A\to \exists b\in B⟨b,y⟩\in a\right)$$
28	27	albii	$$⊢\forall a\forall x\left(\left(a\in A\wedge x=a\left[B\right]\right)\to \exists b\in B⟨b,y⟩\in a\right)\leftrightarrow \forall a\left(a\in A\to \exists b\in B⟨b,y⟩\in a\right)$$
29		alcom	$$⊢\forall x\forall a\left(\left(a\in A\wedge x=a\left[B\right]\right)\to \exists b\in B⟨b,y⟩\in a\right)\leftrightarrow \forall a\forall x\left(\left(a\in A\wedge x=a\left[B\right]\right)\to \exists b\in B⟨b,y⟩\in a\right)$$
30		df-ral	$$⊢\forall a\in A\exists b\in B⟨b,y⟩\in a\leftrightarrow \forall a\left(a\in A\to \exists b\in B⟨b,y⟩\in a\right)$$
31	28 29 30	3bitr4i	$$⊢\forall x\forall a\left(\left(a\in A\wedge x=a\left[B\right]\right)\to \exists b\in B⟨b,y⟩\in a\right)\leftrightarrow \forall a\in A\exists b\in B⟨b,y⟩\in a$$
32	19 31	bitri	$$⊢\forall x\left(\exists a\in Ax=a\left[B\right]\to y\in x\right)\leftrightarrow \forall a\in A\exists b\in B⟨b,y⟩\in a$$
33	4 32	bitri	$$⊢\forall z\in \left\{x|\exists a\in Ax=a\left[B\right]\right\}y\in z\leftrightarrow \forall a\in A\exists b\in B⟨b,y⟩\in a$$
34	2 33	bitri	$$⊢y\in \bigcap \left\{x|\exists a\in Ax=a\left[B\right]\right\}\leftrightarrow \forall a\in A\exists b\in B⟨b,y⟩\in a$$