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	⊢ 𝐴 ∈ V
	opthhausdorff0.b	⊢ 𝐵 ∈ V
	opthhausdorff0.c	⊢ 𝐶 ∈ V
	opthhausdorff0.d	⊢ 𝐷 ∈ V
	opthhausdorff0.1	⊢ 𝑂 ∈ V
	opthhausdorff0.2	⊢ 𝑇 ∈ V
	opthhausdorff0.3	⊢ 𝑂 ≠ 𝑇
Assertion	opthhausdorff0	⊢ ( { { 𝐴 , 𝑂 } , { 𝐵 , 𝑇 } } = { { 𝐶 , 𝑂 } , { 𝐷 , 𝑇 } } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		opthhausdorff0.a	⊢ 𝐴 ∈ V
2		opthhausdorff0.b	⊢ 𝐵 ∈ V
3		opthhausdorff0.c	⊢ 𝐶 ∈ V
4		opthhausdorff0.d	⊢ 𝐷 ∈ V
5		opthhausdorff0.1	⊢ 𝑂 ∈ V
6		opthhausdorff0.2	⊢ 𝑇 ∈ V
7		opthhausdorff0.3	⊢ 𝑂 ≠ 𝑇
8		prex	⊢ { 𝐴 , 𝑂 } ∈ V
9		prex	⊢ { 𝐵 , 𝑇 } ∈ V
10		prex	⊢ { 𝐶 , 𝑂 } ∈ V
11		prex	⊢ { 𝐷 , 𝑇 } ∈ V
12	8 9 10 11	preq12b	⊢ ( { { 𝐴 , 𝑂 } , { 𝐵 , 𝑇 } } = { { 𝐶 , 𝑂 } , { 𝐷 , 𝑇 } } ↔ ( ( { 𝐴 , 𝑂 } = { 𝐶 , 𝑂 } ∧ { 𝐵 , 𝑇 } = { 𝐷 , 𝑇 } ) ∨ ( { 𝐴 , 𝑂 } = { 𝐷 , 𝑇 } ∧ { 𝐵 , 𝑇 } = { 𝐶 , 𝑂 } ) ) )
13	1 3	preqr1	⊢ ( { 𝐴 , 𝑂 } = { 𝐶 , 𝑂 } → 𝐴 = 𝐶 )
14	2 4	preqr1	⊢ ( { 𝐵 , 𝑇 } = { 𝐷 , 𝑇 } → 𝐵 = 𝐷 )
15	13 14	anim12i	⊢ ( ( { 𝐴 , 𝑂 } = { 𝐶 , 𝑂 } ∧ { 𝐵 , 𝑇 } = { 𝐷 , 𝑇 } ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
16	1 5 4 6	preq12b	⊢ ( { 𝐴 , 𝑂 } = { 𝐷 , 𝑇 } ↔ ( ( 𝐴 = 𝐷 ∧ 𝑂 = 𝑇 ) ∨ ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) ) )
17		eqneqall	⊢ ( 𝑂 = 𝑇 → ( 𝑂 ≠ 𝑇 → ( { 𝐵 , 𝑇 } = { 𝐶 , 𝑂 } → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) )
18	7 17	mpi	⊢ ( 𝑂 = 𝑇 → ( { 𝐵 , 𝑇 } = { 𝐶 , 𝑂 } → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
19	18	adantl	⊢ ( ( 𝐴 = 𝐷 ∧ 𝑂 = 𝑇 ) → ( { 𝐵 , 𝑇 } = { 𝐶 , 𝑂 } → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
20	2 6 3 5	preq12b	⊢ ( { 𝐵 , 𝑇 } = { 𝐶 , 𝑂 } ↔ ( ( 𝐵 = 𝐶 ∧ 𝑇 = 𝑂 ) ∨ ( 𝐵 = 𝑂 ∧ 𝑇 = 𝐶 ) ) )
21		eqneqall	⊢ ( 𝑂 = 𝑇 → ( 𝑂 ≠ 𝑇 → ( ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) )
22	7 21	mpi	⊢ ( 𝑂 = 𝑇 → ( ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
23	22	eqcoms	⊢ ( 𝑇 = 𝑂 → ( ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
24	23	adantl	⊢ ( ( 𝐵 = 𝐶 ∧ 𝑇 = 𝑂 ) → ( ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
25		simpl	⊢ ( ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) → 𝐴 = 𝑇 )
26		simpr	⊢ ( ( 𝐵 = 𝑂 ∧ 𝑇 = 𝐶 ) → 𝑇 = 𝐶 )
27	25 26	sylan9eqr	⊢ ( ( ( 𝐵 = 𝑂 ∧ 𝑇 = 𝐶 ) ∧ ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) ) → 𝐴 = 𝐶 )
28		simpl	⊢ ( ( 𝐵 = 𝑂 ∧ 𝑇 = 𝐶 ) → 𝐵 = 𝑂 )
29		simpr	⊢ ( ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) → 𝑂 = 𝐷 )
30	28 29	sylan9eq	⊢ ( ( ( 𝐵 = 𝑂 ∧ 𝑇 = 𝐶 ) ∧ ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) ) → 𝐵 = 𝐷 )
31	27 30	jca	⊢ ( ( ( 𝐵 = 𝑂 ∧ 𝑇 = 𝐶 ) ∧ ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
32	31	ex	⊢ ( ( 𝐵 = 𝑂 ∧ 𝑇 = 𝐶 ) → ( ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
33	24 32	jaoi	⊢ ( ( ( 𝐵 = 𝐶 ∧ 𝑇 = 𝑂 ) ∨ ( 𝐵 = 𝑂 ∧ 𝑇 = 𝐶 ) ) → ( ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
34	20 33	sylbi	⊢ ( { 𝐵 , 𝑇 } = { 𝐶 , 𝑂 } → ( ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
35	34	com12	⊢ ( ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) → ( { 𝐵 , 𝑇 } = { 𝐶 , 𝑂 } → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
36	19 35	jaoi	⊢ ( ( ( 𝐴 = 𝐷 ∧ 𝑂 = 𝑇 ) ∨ ( 𝐴 = 𝑇 ∧ 𝑂 = 𝐷 ) ) → ( { 𝐵 , 𝑇 } = { 𝐶 , 𝑂 } → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
37	16 36	sylbi	⊢ ( { 𝐴 , 𝑂 } = { 𝐷 , 𝑇 } → ( { 𝐵 , 𝑇 } = { 𝐶 , 𝑂 } → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
38	37	imp	⊢ ( ( { 𝐴 , 𝑂 } = { 𝐷 , 𝑇 } ∧ { 𝐵 , 𝑇 } = { 𝐶 , 𝑂 } ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
39	15 38	jaoi	⊢ ( ( ( { 𝐴 , 𝑂 } = { 𝐶 , 𝑂 } ∧ { 𝐵 , 𝑇 } = { 𝐷 , 𝑇 } ) ∨ ( { 𝐴 , 𝑂 } = { 𝐷 , 𝑇 } ∧ { 𝐵 , 𝑇 } = { 𝐶 , 𝑂 } ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
40	12 39	sylbi	⊢ ( { { 𝐴 , 𝑂 } , { 𝐵 , 𝑇 } } = { { 𝐶 , 𝑂 } , { 𝐷 , 𝑇 } } → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
41		preq1	⊢ ( 𝐴 = 𝐶 → { 𝐴 , 𝑂 } = { 𝐶 , 𝑂 } )
42	41	adantr	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → { 𝐴 , 𝑂 } = { 𝐶 , 𝑂 } )
43		preq1	⊢ ( 𝐵 = 𝐷 → { 𝐵 , 𝑇 } = { 𝐷 , 𝑇 } )
44	43	adantl	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → { 𝐵 , 𝑇 } = { 𝐷 , 𝑇 } )
45	42 44	preq12d	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → { { 𝐴 , 𝑂 } , { 𝐵 , 𝑇 } } = { { 𝐶 , 𝑂 } , { 𝐷 , 𝑇 } } )
46	40 45	impbii	⊢ ( { { 𝐴 , 𝑂 } , { 𝐵 , 𝑇 } } = { { 𝐶 , 𝑂 } , { 𝐷 , 𝑇 } } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )