Theorem opthhausdorff0

Description: Justification theorem for the ordered pair definition of Felix Hausdorff in "Grundzüge der Mengenlehre" ("Basics of Set Theory"), 1914, p. 32: <. A , B >._H = { { A , O } , { B , T } } . Hausdorff used 1 and 2 instead of O and T , but actually, any two different fixed sets will do (e.g., O = (/) and T = { (/) } , see 0nep0 ). Furthermore, Hausdorff demanded that O and T are both different from A as well as B , which is actually not necessary if all involved classes exist as sets (i.e. are not proper classes), in contrast to opthhausdorff . See df-op for other ordered pair definitions. (Contributed by AV, 12-Jun-2022)

	Ref	Expression
Hypotheses	opthhausdorff0.a	$$⊢A\in \mathrm{V}$$
	opthhausdorff0.b	$$⊢B\in \mathrm{V}$$
	opthhausdorff0.c	$$⊢C\in \mathrm{V}$$
	opthhausdorff0.d	$$⊢D\in \mathrm{V}$$
	opthhausdorff0.1	$$⊢O\in \mathrm{V}$$
	opthhausdorff0.2	$$⊢T\in \mathrm{V}$$
	opthhausdorff0.3	$$⊢O\ne T$$
Assertion	opthhausdorff0	$$⊢\left\{\left\{A,O\right\},\left\{B,T\right\}\right\}=\left\{\left\{C,O\right\},\left\{D,T\right\}\right\}\leftrightarrow \left(A=C\wedge B=D\right)$$

Proof

Step	Hyp	Ref	Expression
1		opthhausdorff0.a	$$⊢A\in \mathrm{V}$$
2		opthhausdorff0.b	$$⊢B\in \mathrm{V}$$
3		opthhausdorff0.c	$$⊢C\in \mathrm{V}$$
4		opthhausdorff0.d	$$⊢D\in \mathrm{V}$$
5		opthhausdorff0.1	$$⊢O\in \mathrm{V}$$
6		opthhausdorff0.2	$$⊢T\in \mathrm{V}$$
7		opthhausdorff0.3	$$⊢O\ne T$$
8		prex	$$⊢\left\{A,O\right\}\in \mathrm{V}$$
9		prex	$$⊢\left\{B,T\right\}\in \mathrm{V}$$
10		prex	$$⊢\left\{C,O\right\}\in \mathrm{V}$$
11		prex	$$⊢\left\{D,T\right\}\in \mathrm{V}$$
12	8 9 10 11	preq12b	$$⊢\left\{\left\{A,O\right\},\left\{B,T\right\}\right\}=\left\{\left\{C,O\right\},\left\{D,T\right\}\right\}\leftrightarrow \left(\left(\left\{A,O\right\}=\left\{C,O\right\}\wedge \left\{B,T\right\}=\left\{D,T\right\}\right)\vee \left(\left\{A,O\right\}=\left\{D,T\right\}\wedge \left\{B,T\right\}=\left\{C,O\right\}\right)\right)$$
13	1 3	preqr1	$$⊢\left\{A,O\right\}=\left\{C,O\right\}\to A=C$$
14	2 4	preqr1	$$⊢\left\{B,T\right\}=\left\{D,T\right\}\to B=D$$
15	13 14	anim12i	$$⊢\left(\left\{A,O\right\}=\left\{C,O\right\}\wedge \left\{B,T\right\}=\left\{D,T\right\}\right)\to \left(A=C\wedge B=D\right)$$
16	1 5 4 6	preq12b	$$⊢\left\{A,O\right\}=\left\{D,T\right\}\leftrightarrow \left(\left(A=D\wedge O=T\right)\vee \left(A=T\wedge O=D\right)\right)$$
17		eqneqall	$$⊢O=T\to \left(O\ne T\to \left(\left\{B,T\right\}=\left\{C,O\right\}\to \left(A=C\wedge B=D\right)\right)\right)$$
18	7 17	mpi	$$⊢O=T\to \left(\left\{B,T\right\}=\left\{C,O\right\}\to \left(A=C\wedge B=D\right)\right)$$
19	18	adantl	$$⊢\left(A=D\wedge O=T\right)\to \left(\left\{B,T\right\}=\left\{C,O\right\}\to \left(A=C\wedge B=D\right)\right)$$
20	2 6 3 5	preq12b	$$⊢\left\{B,T\right\}=\left\{C,O\right\}\leftrightarrow \left(\left(B=C\wedge T=O\right)\vee \left(B=O\wedge T=C\right)\right)$$
21		eqneqall	$$⊢O=T\to \left(O\ne T\to \left(\left(A=T\wedge O=D\right)\to \left(A=C\wedge B=D\right)\right)\right)$$
22	7 21	mpi	$$⊢O=T\to \left(\left(A=T\wedge O=D\right)\to \left(A=C\wedge B=D\right)\right)$$
23	22	eqcoms	$$⊢T=O\to \left(\left(A=T\wedge O=D\right)\to \left(A=C\wedge B=D\right)\right)$$
24	23	adantl	$$⊢\left(B=C\wedge T=O\right)\to \left(\left(A=T\wedge O=D\right)\to \left(A=C\wedge B=D\right)\right)$$
25		simpl	$$⊢\left(A=T\wedge O=D\right)\to A=T$$
26		simpr	$$⊢\left(B=O\wedge T=C\right)\to T=C$$
27	25 26	sylan9eqr	$$⊢\left(\left(B=O\wedge T=C\right)\wedge \left(A=T\wedge O=D\right)\right)\to A=C$$
28		simpl	$$⊢\left(B=O\wedge T=C\right)\to B=O$$
29		simpr	$$⊢\left(A=T\wedge O=D\right)\to O=D$$
30	28 29	sylan9eq	$$⊢\left(\left(B=O\wedge T=C\right)\wedge \left(A=T\wedge O=D\right)\right)\to B=D$$
31	27 30	jca	$$⊢\left(\left(B=O\wedge T=C\right)\wedge \left(A=T\wedge O=D\right)\right)\to \left(A=C\wedge B=D\right)$$
32	31	ex	$$⊢\left(B=O\wedge T=C\right)\to \left(\left(A=T\wedge O=D\right)\to \left(A=C\wedge B=D\right)\right)$$
33	24 32	jaoi	$$⊢\left(\left(B=C\wedge T=O\right)\vee \left(B=O\wedge T=C\right)\right)\to \left(\left(A=T\wedge O=D\right)\to \left(A=C\wedge B=D\right)\right)$$
34	20 33	sylbi	$$⊢\left\{B,T\right\}=\left\{C,O\right\}\to \left(\left(A=T\wedge O=D\right)\to \left(A=C\wedge B=D\right)\right)$$
35	34	com12	$$⊢\left(A=T\wedge O=D\right)\to \left(\left\{B,T\right\}=\left\{C,O\right\}\to \left(A=C\wedge B=D\right)\right)$$
36	19 35	jaoi	$$⊢\left(\left(A=D\wedge O=T\right)\vee \left(A=T\wedge O=D\right)\right)\to \left(\left\{B,T\right\}=\left\{C,O\right\}\to \left(A=C\wedge B=D\right)\right)$$
37	16 36	sylbi	$$⊢\left\{A,O\right\}=\left\{D,T\right\}\to \left(\left\{B,T\right\}=\left\{C,O\right\}\to \left(A=C\wedge B=D\right)\right)$$
38	37	imp	$$⊢\left(\left\{A,O\right\}=\left\{D,T\right\}\wedge \left\{B,T\right\}=\left\{C,O\right\}\right)\to \left(A=C\wedge B=D\right)$$
39	15 38	jaoi	$$⊢\left(\left(\left\{A,O\right\}=\left\{C,O\right\}\wedge \left\{B,T\right\}=\left\{D,T\right\}\right)\vee \left(\left\{A,O\right\}=\left\{D,T\right\}\wedge \left\{B,T\right\}=\left\{C,O\right\}\right)\right)\to \left(A=C\wedge B=D\right)$$
40	12 39	sylbi	$$⊢\left\{\left\{A,O\right\},\left\{B,T\right\}\right\}=\left\{\left\{C,O\right\},\left\{D,T\right\}\right\}\to \left(A=C\wedge B=D\right)$$
41		preq1	$$⊢A=C\to \left\{A,O\right\}=\left\{C,O\right\}$$
42	41	adantr	$$⊢\left(A=C\wedge B=D\right)\to \left\{A,O\right\}=\left\{C,O\right\}$$
43		preq1	$$⊢B=D\to \left\{B,T\right\}=\left\{D,T\right\}$$
44	43	adantl	$$⊢\left(A=C\wedge B=D\right)\to \left\{B,T\right\}=\left\{D,T\right\}$$
45	42 44	preq12d	$$⊢\left(A=C\wedge B=D\right)\to \left\{\left\{A,O\right\},\left\{B,T\right\}\right\}=\left\{\left\{C,O\right\},\left\{D,T\right\}\right\}$$
46	40 45	impbii	$$⊢\left\{\left\{A,O\right\},\left\{B,T\right\}\right\}=\left\{\left\{C,O\right\},\left\{D,T\right\}\right\}\leftrightarrow \left(A=C\wedge B=D\right)$$