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	$⊢ A \in V$
	opthhausdorff.b	$⊢ B \in V$
	opthhausdorff.o	$⊢ A \neq O$
	opthhausdorff.n	$⊢ B \neq O$
	opthhausdorff.t	$⊢ B \neq T$
	opthhausdorff.1	$⊢ O \in V$
	opthhausdorff.2	$⊢ T \in V$
	opthhausdorff.3	$⊢ O \neq T$
Assertion	opthhausdorff	$⊢ \{\{A, O\}, \{B, T\}\} = \{\{C, O\}, \{D, T\}\} \leftrightarrow (A = C \land B = D)$

Proof

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

Metamath Proof Explorer

Theorem opthhausdorff

Proof