Theorem brcup

Description: Binary relation form of the Cup function. (Contributed by Scott Fenton, 14-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	brcup.1	$$⊢A\in \mathrm{V}$$
	brcup.2	$$⊢B\in \mathrm{V}$$
	brcup.3	$$⊢C\in \mathrm{V}$$
Assertion	brcup	$$⊢⟨A,B⟩\mathrm{𝖢𝗎𝗉}C\leftrightarrow C=A\cup B$$

Proof

Step	Hyp	Ref	Expression
1		brcup.1	$$⊢A\in \mathrm{V}$$
2		brcup.2	$$⊢B\in \mathrm{V}$$
3		brcup.3	$$⊢C\in \mathrm{V}$$
4		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
5		df-cup	$$⊢\mathrm{𝖢𝗎𝗉}=\left(\left(\mathrm{V}\times \mathrm{V}\right)\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\left(\mathrm{V}\otimes \mathrm{E}\right)∆\left(\left(\left({1^{st}}^{-1}\circ \mathrm{E}\right)\cup \left({2^{nd}}^{-1}\circ \mathrm{E}\right)\right)\otimes \mathrm{V}\right)\right)$$
6	1 2	opelvv	$$⊢⟨A,B⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
7		brxp	$$⊢⟨A,B⟩\left(\left(\mathrm{V}\times \mathrm{V}\right)\times \mathrm{V}\right)C\leftrightarrow \left(⟨A,B⟩\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge C\in \mathrm{V}\right)$$
8	6 3 7	mpbir2an	$$⊢⟨A,B⟩\left(\left(\mathrm{V}\times \mathrm{V}\right)\times \mathrm{V}\right)C$$
9		epel	$$⊢x\mathrm{E}y\leftrightarrow x\in y$$
10		vex	$$⊢y\in \mathrm{V}$$
11	10 4	brcnv	$$⊢y{1^{st}}^{-1}⟨A,B⟩\leftrightarrow ⟨A,B⟩1^{st}y$$
12	1 2	br1steq	$$⊢⟨A,B⟩1^{st}y\leftrightarrow y=A$$
13	11 12	bitri	$$⊢y{1^{st}}^{-1}⟨A,B⟩\leftrightarrow y=A$$
14	9 13	anbi12ci	$$⊢\left(x\mathrm{E}y\wedge y{1^{st}}^{-1}⟨A,B⟩\right)\leftrightarrow \left(y=A\wedge x\in y\right)$$
15	14	exbii	$$⊢\exists y\left(x\mathrm{E}y\wedge y{1^{st}}^{-1}⟨A,B⟩\right)\leftrightarrow \exists y\left(y=A\wedge x\in y\right)$$
16		vex	$$⊢x\in \mathrm{V}$$
17	16 4	brco	$$⊢x\left({1^{st}}^{-1}\circ \mathrm{E}\right)⟨A,B⟩\leftrightarrow \exists y\left(x\mathrm{E}y\wedge y{1^{st}}^{-1}⟨A,B⟩\right)$$
18	1	clel3	$$⊢x\in A\leftrightarrow \exists y\left(y=A\wedge x\in y\right)$$
19	15 17 18	3bitr4i	$$⊢x\left({1^{st}}^{-1}\circ \mathrm{E}\right)⟨A,B⟩\leftrightarrow x\in A$$
20	10 4	brcnv	$$⊢y{2^{nd}}^{-1}⟨A,B⟩\leftrightarrow ⟨A,B⟩2^{nd}y$$
21	1 2	br2ndeq	$$⊢⟨A,B⟩2^{nd}y\leftrightarrow y=B$$
22	20 21	bitri	$$⊢y{2^{nd}}^{-1}⟨A,B⟩\leftrightarrow y=B$$
23	9 22	anbi12ci	$$⊢\left(x\mathrm{E}y\wedge y{2^{nd}}^{-1}⟨A,B⟩\right)\leftrightarrow \left(y=B\wedge x\in y\right)$$
24	23	exbii	$$⊢\exists y\left(x\mathrm{E}y\wedge y{2^{nd}}^{-1}⟨A,B⟩\right)\leftrightarrow \exists y\left(y=B\wedge x\in y\right)$$
25	16 4	brco	$$⊢x\left({2^{nd}}^{-1}\circ \mathrm{E}\right)⟨A,B⟩\leftrightarrow \exists y\left(x\mathrm{E}y\wedge y{2^{nd}}^{-1}⟨A,B⟩\right)$$
26	2	clel3	$$⊢x\in B\leftrightarrow \exists y\left(y=B\wedge x\in y\right)$$
27	24 25 26	3bitr4i	$$⊢x\left({2^{nd}}^{-1}\circ \mathrm{E}\right)⟨A,B⟩\leftrightarrow x\in B$$
28	19 27	orbi12i	$$⊢\left(x\left({1^{st}}^{-1}\circ \mathrm{E}\right)⟨A,B⟩\vee x\left({2^{nd}}^{-1}\circ \mathrm{E}\right)⟨A,B⟩\right)\leftrightarrow \left(x\in A\vee x\in B\right)$$
29		brun	$$⊢x\left(\left({1^{st}}^{-1}\circ \mathrm{E}\right)\cup \left({2^{nd}}^{-1}\circ \mathrm{E}\right)\right)⟨A,B⟩\leftrightarrow \left(x\left({1^{st}}^{-1}\circ \mathrm{E}\right)⟨A,B⟩\vee x\left({2^{nd}}^{-1}\circ \mathrm{E}\right)⟨A,B⟩\right)$$
30		elun	$$⊢x\in \left(A\cup B\right)\leftrightarrow \left(x\in A\vee x\in B\right)$$
31	28 29 30	3bitr4ri	$$⊢x\in \left(A\cup B\right)\leftrightarrow x\left(\left({1^{st}}^{-1}\circ \mathrm{E}\right)\cup \left({2^{nd}}^{-1}\circ \mathrm{E}\right)\right)⟨A,B⟩$$
32	4 3 5 8 31	brtxpsd3	$$⊢⟨A,B⟩\mathrm{𝖢𝗎𝗉}C\leftrightarrow C=A\cup B$$