Theorem opth

Description: The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of TakeutiZaring p. 16. Note that C and D are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995)

	Ref	Expression
Hypotheses	opth1.1	$$⊢A\in \mathrm{V}$$
	opth1.2	$$⊢B\in \mathrm{V}$$
Assertion	opth	$$⊢⟨A,B⟩=⟨C,D⟩\leftrightarrow \left(A=C\wedge B=D\right)$$

Proof

Step	Hyp	Ref	Expression
1		opth1.1	$$⊢A\in \mathrm{V}$$
2		opth1.2	$$⊢B\in \mathrm{V}$$
3	1 2	opth1	$$⊢⟨A,B⟩=⟨C,D⟩\to A=C$$
4	1 2	opi1	$$⊢\left\{A\right\}\in ⟨A,B⟩$$
5		id	$$⊢⟨A,B⟩=⟨C,D⟩\to ⟨A,B⟩=⟨C,D⟩$$
6	4 5	eleqtrid	$$⊢⟨A,B⟩=⟨C,D⟩\to \left\{A\right\}\in ⟨C,D⟩$$
7		oprcl	$$⊢\left\{A\right\}\in ⟨C,D⟩\to \left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)$$
8	6 7	syl	$$⊢⟨A,B⟩=⟨C,D⟩\to \left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)$$
9	8	simprd	$$⊢⟨A,B⟩=⟨C,D⟩\to D\in \mathrm{V}$$
10	3	opeq1d	$$⊢⟨A,B⟩=⟨C,D⟩\to ⟨A,B⟩=⟨C,B⟩$$
11	10 5	eqtr3d	$$⊢⟨A,B⟩=⟨C,D⟩\to ⟨C,B⟩=⟨C,D⟩$$
12	8	simpld	$$⊢⟨A,B⟩=⟨C,D⟩\to C\in \mathrm{V}$$
13		dfopg	$$⊢\left(C\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to ⟨C,B⟩=\left\{\left\{C\right\},\left\{C,B\right\}\right\}$$
14	12 2 13	sylancl	$$⊢⟨A,B⟩=⟨C,D⟩\to ⟨C,B⟩=\left\{\left\{C\right\},\left\{C,B\right\}\right\}$$
15	11 14	eqtr3d	$$⊢⟨A,B⟩=⟨C,D⟩\to ⟨C,D⟩=\left\{\left\{C\right\},\left\{C,B\right\}\right\}$$
16		dfopg	$$⊢\left(C\in \mathrm{V}\wedge D\in \mathrm{V}\right)\to ⟨C,D⟩=\left\{\left\{C\right\},\left\{C,D\right\}\right\}$$
17	8 16	syl	$$⊢⟨A,B⟩=⟨C,D⟩\to ⟨C,D⟩=\left\{\left\{C\right\},\left\{C,D\right\}\right\}$$
18	15 17	eqtr3d	$$⊢⟨A,B⟩=⟨C,D⟩\to \left\{\left\{C\right\},\left\{C,B\right\}\right\}=\left\{\left\{C\right\},\left\{C,D\right\}\right\}$$
19		prex	$$⊢\left\{C,B\right\}\in \mathrm{V}$$
20		prex	$$⊢\left\{C,D\right\}\in \mathrm{V}$$
21	19 20	preqr2	$$⊢\left\{\left\{C\right\},\left\{C,B\right\}\right\}=\left\{\left\{C\right\},\left\{C,D\right\}\right\}\to \left\{C,B\right\}=\left\{C,D\right\}$$
22	18 21	syl	$$⊢⟨A,B⟩=⟨C,D⟩\to \left\{C,B\right\}=\left\{C,D\right\}$$
23		preq2	$$⊢x=D\to \left\{C,x\right\}=\left\{C,D\right\}$$
24	23	eqeq2d	$$⊢x=D\to \left(\left\{C,B\right\}=\left\{C,x\right\}\leftrightarrow \left\{C,B\right\}=\left\{C,D\right\}\right)$$
25		eqeq2	$$⊢x=D\to \left(B=x\leftrightarrow B=D\right)$$
26	24 25	imbi12d	$$⊢x=D\to \left(\left(\left\{C,B\right\}=\left\{C,x\right\}\to B=x\right)\leftrightarrow \left(\left\{C,B\right\}=\left\{C,D\right\}\to B=D\right)\right)$$
27		vex	$$⊢x\in \mathrm{V}$$
28	2 27	preqr2	$$⊢\left\{C,B\right\}=\left\{C,x\right\}\to B=x$$
29	26 28	vtoclg	$$⊢D\in \mathrm{V}\to \left(\left\{C,B\right\}=\left\{C,D\right\}\to B=D\right)$$
30	9 22 29	sylc	$$⊢⟨A,B⟩=⟨C,D⟩\to B=D$$
31	3 30	jca	$$⊢⟨A,B⟩=⟨C,D⟩\to \left(A=C\wedge B=D\right)$$
32		opeq12	$$⊢\left(A=C\wedge B=D\right)\to ⟨A,B⟩=⟨C,D⟩$$
33	31 32	impbii	$$⊢⟨A,B⟩=⟨C,D⟩\leftrightarrow \left(A=C\wedge B=D\right)$$