Theorem opthhausdorff

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 in full extent ( A =/= T is not required). This definition is meaningful only for classes A and B that exist as sets (i.e., are not proper classes): If A and C were different proper classes ( A =/= C ), then { { A , O } , { B , T } } = { { C , O } , { D , T } <-> { { O } , { B , T } } = { { O } , { D , T } is true if B = D , but ( A = C /\ B = D ) would be false. See df-op for other ordered pair definitions. (Contributed by AV, 14-Jun-2022)

	Ref	Expression
Hypotheses	opthhausdorff.a	⊢ 𝐴 ∈ V
	opthhausdorff.b	⊢ 𝐵 ∈ V
	opthhausdorff.o	⊢ 𝐴 ≠ 𝑂
	opthhausdorff.n	⊢ 𝐵 ≠ 𝑂
	opthhausdorff.t	⊢ 𝐵 ≠ 𝑇
	opthhausdorff.1	⊢ 𝑂 ∈ V
	opthhausdorff.2	⊢ 𝑇 ∈ V
	opthhausdorff.3	⊢ 𝑂 ≠ 𝑇
Assertion	opthhausdorff	⊢ ( { { 𝐴 , 𝑂 } , { 𝐵 , 𝑇 } } = { { 𝐶 , 𝑂 } , { 𝐷 , 𝑇 } } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		opthhausdorff.a	⊢ 𝐴 ∈ V
2		opthhausdorff.b	⊢ 𝐵 ∈ V
3		opthhausdorff.o	⊢ 𝐴 ≠ 𝑂
4		opthhausdorff.n	⊢ 𝐵 ≠ 𝑂
5		opthhausdorff.t	⊢ 𝐵 ≠ 𝑇
6		opthhausdorff.1	⊢ 𝑂 ∈ V
7		opthhausdorff.2	⊢ 𝑇 ∈ V
8		opthhausdorff.3	⊢ 𝑂 ≠ 𝑇
9		prex	⊢ { 𝐴 , 𝑂 } ∈ V
10		prex	⊢ { 𝐵 , 𝑇 } ∈ V
11	1 6	pm3.2i	⊢ ( 𝐴 ∈ V ∧ 𝑂 ∈ V )
12	2 7	pm3.2i	⊢ ( 𝐵 ∈ V ∧ 𝑇 ∈ V )
13	11 12	pm3.2i	⊢ ( ( 𝐴 ∈ V ∧ 𝑂 ∈ V ) ∧ ( 𝐵 ∈ V ∧ 𝑇 ∈ V ) )
14	4	necomi	⊢ 𝑂 ≠ 𝐵
15	14 8	pm3.2i	⊢ ( 𝑂 ≠ 𝐵 ∧ 𝑂 ≠ 𝑇 )
16	15	olci	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝑇 ) ∨ ( 𝑂 ≠ 𝐵 ∧ 𝑂 ≠ 𝑇 ) )
17		prneimg	⊢ ( ( ( 𝐴 ∈ V ∧ 𝑂 ∈ V ) ∧ ( 𝐵 ∈ V ∧ 𝑇 ∈ V ) ) → ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝑇 ) ∨ ( 𝑂 ≠ 𝐵 ∧ 𝑂 ≠ 𝑇 ) ) → { 𝐴 , 𝑂 } ≠ { 𝐵 , 𝑇 } ) )
18	13 16 17	mp2	⊢ { 𝐴 , 𝑂 } ≠ { 𝐵 , 𝑇 }
19		preq12nebg	⊢ ( ( { 𝐴 , 𝑂 } ∈ V ∧ { 𝐵 , 𝑇 } ∈ V ∧ { 𝐴 , 𝑂 } ≠ { 𝐵 , 𝑇 } ) → ( { { 𝐴 , 𝑂 } , { 𝐵 , 𝑇 } } = { { 𝐶 , 𝑂 } , { 𝐷 , 𝑇 } } ↔ ( ( { 𝐴 , 𝑂 } = { 𝐶 , 𝑂 } ∧ { 𝐵 , 𝑇 } = { 𝐷 , 𝑇 } ) ∨ ( { 𝐴 , 𝑂 } = { 𝐷 , 𝑇 } ∧ { 𝐵 , 𝑇 } = { 𝐶 , 𝑂 } ) ) ) )
20	9 10 18 19	mp3an	⊢ ( { { 𝐴 , 𝑂 } , { 𝐵 , 𝑇 } } = { { 𝐶 , 𝑂 } , { 𝐷 , 𝑇 } } ↔ ( ( { 𝐴 , 𝑂 } = { 𝐶 , 𝑂 } ∧ { 𝐵 , 𝑇 } = { 𝐷 , 𝑇 } ) ∨ ( { 𝐴 , 𝑂 } = { 𝐷 , 𝑇 } ∧ { 𝐵 , 𝑇 } = { 𝐶 , 𝑂 } ) ) )
21		preq12nebg	⊢ ( ( 𝐴 ∈ V ∧ 𝑂 ∈ V ∧ 𝐴 ≠ 𝑂 ) → ( { 𝐴 , 𝑂 } = { 𝐶 , 𝑂 } ↔ ( ( 𝐴 = 𝐶 ∧ 𝑂 = 𝑂 ) ∨ ( 𝐴 = 𝑂 ∧ 𝑂 = 𝐶 ) ) ) )
22	1 6 3 21	mp3an	⊢ ( { 𝐴 , 𝑂 } = { 𝐶 , 𝑂 } ↔ ( ( 𝐴 = 𝐶 ∧ 𝑂 = 𝑂 ) ∨ ( 𝐴 = 𝑂 ∧ 𝑂 = 𝐶 ) ) )
23		preq12nebg	⊢ ( ( 𝐵 ∈ V ∧ 𝑇 ∈ V ∧ 𝐵 ≠ 𝑇 ) → ( { 𝐵 , 𝑇 } = { 𝐷 , 𝑇 } ↔ ( ( 𝐵 = 𝐷 ∧ 𝑇 = 𝑇 ) ∨ ( 𝐵 = 𝑇 ∧ 𝑇 = 𝐷 ) ) ) )
24	2 7 5 23	mp3an	⊢ ( { 𝐵 , 𝑇 } = { 𝐷 , 𝑇 } ↔ ( ( 𝐵 = 𝐷 ∧ 𝑇 = 𝑇 ) ∨ ( 𝐵 = 𝑇 ∧ 𝑇 = 𝐷 ) ) )
25		simpl	⊢ ( ( 𝐴 = 𝐶 ∧ 𝑂 = 𝑂 ) → 𝐴 = 𝐶 )
26		simpl	⊢ ( ( 𝐵 = 𝐷 ∧ 𝑇 = 𝑇 ) → 𝐵 = 𝐷 )
27	25 26	anim12i	⊢ ( ( ( 𝐴 = 𝐶 ∧ 𝑂 = 𝑂 ) ∧ ( 𝐵 = 𝐷 ∧ 𝑇 = 𝑇 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
28		eqneqall	⊢ ( 𝐴 = 𝑂 → ( 𝐴 ≠ 𝑂 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
29	3 28	mpi	⊢ ( 𝐴 = 𝑂 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
30	29	adantr	⊢ ( ( 𝐴 = 𝑂 ∧ 𝑂 = 𝐶 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
31		eqneqall	⊢ ( 𝐵 = 𝑇 → ( 𝐵 ≠ 𝑇 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
32	5 31	mpi	⊢ ( 𝐵 = 𝑇 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
33	32	adantr	⊢ ( ( 𝐵 = 𝑇 ∧ 𝑇 = 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
34	27 30 33	ccase2	⊢ ( ( ( ( 𝐴 = 𝐶 ∧ 𝑂 = 𝑂 ) ∨ ( 𝐴 = 𝑂 ∧ 𝑂 = 𝐶 ) ) ∧ ( ( 𝐵 = 𝐷 ∧ 𝑇 = 𝑇 ) ∨ ( 𝐵 = 𝑇 ∧ 𝑇 = 𝐷 ) ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
35	22 24 34	syl2anb	⊢ ( ( { 𝐴 , 𝑂 } = { 𝐶 , 𝑂 } ∧ { 𝐵 , 𝑇 } = { 𝐷 , 𝑇 } ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
36		preq12nebg	⊢ ( ( 𝐴 ∈ V ∧ 𝑂 ∈ V ∧ 𝐴 ≠ 𝑂 ) → ( { 𝐴 , 𝑂 } = { 𝐷 , 𝑇 } ↔ ( ( 𝐴 = 𝐷 ∧ 𝑂 = 𝑇 ) ∨ ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) ) ) )
37	1 6 3 36	mp3an	⊢ ( { 𝐴 , 𝑂 } = { 𝐷 , 𝑇 } ↔ ( ( 𝐴 = 𝐷 ∧ 𝑂 = 𝑇 ) ∨ ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) ) )
38		preq12nebg	⊢ ( ( 𝐵 ∈ V ∧ 𝑇 ∈ V ∧ 𝐵 ≠ 𝑇 ) → ( { 𝐵 , 𝑇 } = { 𝐶 , 𝑂 } ↔ ( ( 𝐵 = 𝐶 ∧ 𝑇 = 𝑂 ) ∨ ( 𝐵 = 𝑂 ∧ 𝑇 = 𝐶 ) ) ) )
39	2 7 5 38	mp3an	⊢ ( { 𝐵 , 𝑇 } = { 𝐶 , 𝑂 } ↔ ( ( 𝐵 = 𝐶 ∧ 𝑇 = 𝑂 ) ∨ ( 𝐵 = 𝑂 ∧ 𝑇 = 𝐶 ) ) )
40		eqneqall	⊢ ( 𝑂 = 𝑇 → ( 𝑂 ≠ 𝑇 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
41	8 40	mpi	⊢ ( 𝑂 = 𝑇 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
42	41	adantl	⊢ ( ( 𝐴 = 𝐷 ∧ 𝑂 = 𝑇 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
43	42	a1d	⊢ ( ( 𝐴 = 𝐷 ∧ 𝑂 = 𝑇 ) → ( ( ( 𝐵 = 𝐶 ∧ 𝑇 = 𝑂 ) ∨ ( 𝐵 = 𝑂 ∧ 𝑇 = 𝐶 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
44	8	necomi	⊢ 𝑇 ≠ 𝑂
45		eqneqall	⊢ ( 𝑇 = 𝑂 → ( 𝑇 ≠ 𝑂 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
46	44 45	mpi	⊢ ( 𝑇 = 𝑂 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
47	46	adantl	⊢ ( ( 𝐵 = 𝐶 ∧ 𝑇 = 𝑂 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
48	47	a1d	⊢ ( ( 𝐵 = 𝐶 ∧ 𝑇 = 𝑂 ) → ( ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
49		eqneqall	⊢ ( 𝐵 = 𝑂 → ( 𝐵 ≠ 𝑂 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
50	4 49	mpi	⊢ ( 𝐵 = 𝑂 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
51	50	adantr	⊢ ( ( 𝐵 = 𝑂 ∧ 𝑇 = 𝐶 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
52	51	a1d	⊢ ( ( 𝐵 = 𝑂 ∧ 𝑇 = 𝐶 ) → ( ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
53	48 52	jaoi	⊢ ( ( ( 𝐵 = 𝐶 ∧ 𝑇 = 𝑂 ) ∨ ( 𝐵 = 𝑂 ∧ 𝑇 = 𝐶 ) ) → ( ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
54	53	com12	⊢ ( ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) → ( ( ( 𝐵 = 𝐶 ∧ 𝑇 = 𝑂 ) ∨ ( 𝐵 = 𝑂 ∧ 𝑇 = 𝐶 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
55	43 54	jaoi	⊢ ( ( ( 𝐴 = 𝐷 ∧ 𝑂 = 𝑇 ) ∨ ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) ) → ( ( ( 𝐵 = 𝐶 ∧ 𝑇 = 𝑂 ) ∨ ( 𝐵 = 𝑂 ∧ 𝑇 = 𝐶 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
56	55	imp	⊢ ( ( ( ( 𝐴 = 𝐷 ∧ 𝑂 = 𝑇 ) ∨ ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) ) ∧ ( ( 𝐵 = 𝐶 ∧ 𝑇 = 𝑂 ) ∨ ( 𝐵 = 𝑂 ∧ 𝑇 = 𝐶 ) ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
57	37 39 56	syl2anb	⊢ ( ( { 𝐴 , 𝑂 } = { 𝐷 , 𝑇 } ∧ { 𝐵 , 𝑇 } = { 𝐶 , 𝑂 } ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
58	35 57	jaoi	⊢ ( ( ( { 𝐴 , 𝑂 } = { 𝐶 , 𝑂 } ∧ { 𝐵 , 𝑇 } = { 𝐷 , 𝑇 } ) ∨ ( { 𝐴 , 𝑂 } = { 𝐷 , 𝑇 } ∧ { 𝐵 , 𝑇 } = { 𝐶 , 𝑂 } ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
59	20 58	sylbi	⊢ ( { { 𝐴 , 𝑂 } , { 𝐵 , 𝑇 } } = { { 𝐶 , 𝑂 } , { 𝐷 , 𝑇 } } → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
60		preq1	⊢ ( 𝐴 = 𝐶 → { 𝐴 , 𝑂 } = { 𝐶 , 𝑂 } )
61	60	adantr	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → { 𝐴 , 𝑂 } = { 𝐶 , 𝑂 } )
62		preq1	⊢ ( 𝐵 = 𝐷 → { 𝐵 , 𝑇 } = { 𝐷 , 𝑇 } )
63	62	adantl	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → { 𝐵 , 𝑇 } = { 𝐷 , 𝑇 } )
64	61 63	preq12d	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → { { 𝐴 , 𝑂 } , { 𝐵 , 𝑇 } } = { { 𝐶 , 𝑂 } , { 𝐷 , 𝑇 } } )
65	59 64	impbii	⊢ ( { { 𝐴 , 𝑂 } , { 𝐵 , 𝑇 } } = { { 𝐶 , 𝑂 } , { 𝐷 , 𝑇 } } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )