opthprc

Description: Justification theorem for an ordered pair definition that works for any classes, including proper classes. This is a possible definition implied by the footnote in Jech p. 78, which says, "The sophisticated reader will not object to our use of a pair of classes." (Contributed by NM, 28-Sep-2003)

		Ref	Expression
	Assertion	opthprc	$⊢ (A \times \{\emptyset\}) \cup (B \times \{\{\emptyset\}\}) = (C \times \{\emptyset\}) \cup (D \times \{\{\emptyset\}\}) \leftrightarrow (A = C \land B = D)$

Proof

Step	Hyp	Ref	Expression
1		eleq2	$⊢ (A \times \{\emptyset\}) \cup (B \times \{\{\emptyset\}\}) = (C \times \{\emptyset\}) \cup (D \times \{\{\emptyset\}\}) \to (⟨x, \emptyset⟩ \in ((A \times \{\emptyset\}) \cup (B \times \{\{\emptyset\}\})) \leftrightarrow ⟨x, \emptyset⟩ \in ((C \times \{\emptyset\}) \cup (D \times \{\{\emptyset\}\})))$
2		0ex	$⊢ \emptyset \in V$
3	2	snid	$⊢ \emptyset \in \{\emptyset\}$
4		opelxp	$⊢ ⟨x, \emptyset⟩ \in (A \times \{\emptyset\}) \leftrightarrow (x \in A \land \emptyset \in \{\emptyset\})$
5	3 4	mpbiran2	$⊢ ⟨x, \emptyset⟩ \in (A \times \{\emptyset\}) \leftrightarrow x \in A$
6		opelxp	$⊢ ⟨x, \emptyset⟩ \in (B \times \{\{\emptyset\}\}) \leftrightarrow (x \in B \land \emptyset \in \{\{\emptyset\}\})$
7		0nep0	$⊢ \emptyset \neq \{\emptyset\}$
8	2	elsn	$⊢ \emptyset \in \{\{\emptyset\}\} \leftrightarrow \emptyset = \{\emptyset\}$
9	7 8	nemtbir	$⊢ \neg \emptyset \in \{\{\emptyset\}\}$
10	9	bianfi	$⊢ \emptyset \in \{\{\emptyset\}\} \leftrightarrow (x \in B \land \emptyset \in \{\{\emptyset\}\})$
11	6 10	bitr4i	$⊢ ⟨x, \emptyset⟩ \in (B \times \{\{\emptyset\}\}) \leftrightarrow \emptyset \in \{\{\emptyset\}\}$
12	5 11	orbi12i	$⊢ (⟨x, \emptyset⟩ \in (A \times \{\emptyset\}) \lor ⟨x, \emptyset⟩ \in (B \times \{\{\emptyset\}\})) \leftrightarrow (x \in A \lor \emptyset \in \{\{\emptyset\}\})$
13		elun	$⊢ ⟨x, \emptyset⟩ \in ((A \times \{\emptyset\}) \cup (B \times \{\{\emptyset\}\})) \leftrightarrow (⟨x, \emptyset⟩ \in (A \times \{\emptyset\}) \lor ⟨x, \emptyset⟩ \in (B \times \{\{\emptyset\}\}))$
14	9	biorfi	$⊢ x \in A \leftrightarrow (x \in A \lor \emptyset \in \{\{\emptyset\}\})$
15	12 13 14	3bitr4ri	$⊢ x \in A \leftrightarrow ⟨x, \emptyset⟩ \in ((A \times \{\emptyset\}) \cup (B \times \{\{\emptyset\}\}))$
16		opelxp	$⊢ ⟨x, \emptyset⟩ \in (C \times \{\emptyset\}) \leftrightarrow (x \in C \land \emptyset \in \{\emptyset\})$
17	3 16	mpbiran2	$⊢ ⟨x, \emptyset⟩ \in (C \times \{\emptyset\}) \leftrightarrow x \in C$
18		opelxp	$⊢ ⟨x, \emptyset⟩ \in (D \times \{\{\emptyset\}\}) \leftrightarrow (x \in D \land \emptyset \in \{\{\emptyset\}\})$
19	9	bianfi	$⊢ \emptyset \in \{\{\emptyset\}\} \leftrightarrow (x \in D \land \emptyset \in \{\{\emptyset\}\})$
20	18 19	bitr4i	$⊢ ⟨x, \emptyset⟩ \in (D \times \{\{\emptyset\}\}) \leftrightarrow \emptyset \in \{\{\emptyset\}\}$
21	17 20	orbi12i	$⊢ (⟨x, \emptyset⟩ \in (C \times \{\emptyset\}) \lor ⟨x, \emptyset⟩ \in (D \times \{\{\emptyset\}\})) \leftrightarrow (x \in C \lor \emptyset \in \{\{\emptyset\}\})$
22		elun	$⊢ ⟨x, \emptyset⟩ \in ((C \times \{\emptyset\}) \cup (D \times \{\{\emptyset\}\})) \leftrightarrow (⟨x, \emptyset⟩ \in (C \times \{\emptyset\}) \lor ⟨x, \emptyset⟩ \in (D \times \{\{\emptyset\}\}))$
23	9	biorfi	$⊢ x \in C \leftrightarrow (x \in C \lor \emptyset \in \{\{\emptyset\}\})$
24	21 22 23	3bitr4ri	$⊢ x \in C \leftrightarrow ⟨x, \emptyset⟩ \in ((C \times \{\emptyset\}) \cup (D \times \{\{\emptyset\}\}))$
25	1 15 24	3bitr4g	$⊢ (A \times \{\emptyset\}) \cup (B \times \{\{\emptyset\}\}) = (C \times \{\emptyset\}) \cup (D \times \{\{\emptyset\}\}) \to (x \in A \leftrightarrow x \in C)$
26	25	eqrdv	$⊢ (A \times \{\emptyset\}) \cup (B \times \{\{\emptyset\}\}) = (C \times \{\emptyset\}) \cup (D \times \{\{\emptyset\}\}) \to A = C$
27		eleq2	$⊢ (A \times \{\emptyset\}) \cup (B \times \{\{\emptyset\}\}) = (C \times \{\emptyset\}) \cup (D \times \{\{\emptyset\}\}) \to (⟨x, \{\emptyset\}⟩ \in ((A \times \{\emptyset\}) \cup (B \times \{\{\emptyset\}\})) \leftrightarrow ⟨x, \{\emptyset\}⟩ \in ((C \times \{\emptyset\}) \cup (D \times \{\{\emptyset\}\})))$
28		opelxp	$⊢ ⟨x, \{\emptyset\}⟩ \in (A \times \{\emptyset\}) \leftrightarrow (x \in A \land \{\emptyset\} \in \{\emptyset\})$
29		snex	$⊢ \{\emptyset\} \in V$
30	29	elsn	$⊢ \{\emptyset\} \in \{\emptyset\} \leftrightarrow \{\emptyset\} = \emptyset$
31		eqcom	$⊢ \{\emptyset\} = \emptyset \leftrightarrow \emptyset = \{\emptyset\}$
32	30 31	bitri	$⊢ \{\emptyset\} \in \{\emptyset\} \leftrightarrow \emptyset = \{\emptyset\}$
33	7 32	nemtbir	$⊢ \neg \{\emptyset\} \in \{\emptyset\}$
34	33	bianfi	$⊢ \{\emptyset\} \in \{\emptyset\} \leftrightarrow (x \in A \land \{\emptyset\} \in \{\emptyset\})$
35	28 34	bitr4i	$⊢ ⟨x, \{\emptyset\}⟩ \in (A \times \{\emptyset\}) \leftrightarrow \{\emptyset\} \in \{\emptyset\}$
36	29	snid	$⊢ \{\emptyset\} \in \{\{\emptyset\}\}$
37		opelxp	$⊢ ⟨x, \{\emptyset\}⟩ \in (B \times \{\{\emptyset\}\}) \leftrightarrow (x \in B \land \{\emptyset\} \in \{\{\emptyset\}\})$
38	36 37	mpbiran2	$⊢ ⟨x, \{\emptyset\}⟩ \in (B \times \{\{\emptyset\}\}) \leftrightarrow x \in B$
39	35 38	orbi12i	$⊢ (⟨x, \{\emptyset\}⟩ \in (A \times \{\emptyset\}) \lor ⟨x, \{\emptyset\}⟩ \in (B \times \{\{\emptyset\}\})) \leftrightarrow (\{\emptyset\} \in \{\emptyset\} \lor x \in B)$
40		elun	$⊢ ⟨x, \{\emptyset\}⟩ \in ((A \times \{\emptyset\}) \cup (B \times \{\{\emptyset\}\})) \leftrightarrow (⟨x, \{\emptyset\}⟩ \in (A \times \{\emptyset\}) \lor ⟨x, \{\emptyset\}⟩ \in (B \times \{\{\emptyset\}\}))$
41		biorf	$⊢ \neg \{\emptyset\} \in \{\emptyset\} \to (x \in B \leftrightarrow (\{\emptyset\} \in \{\emptyset\} \lor x \in B))$
42	33 41	ax-mp	$⊢ x \in B \leftrightarrow (\{\emptyset\} \in \{\emptyset\} \lor x \in B)$
43	39 40 42	3bitr4ri	$⊢ x \in B \leftrightarrow ⟨x, \{\emptyset\}⟩ \in ((A \times \{\emptyset\}) \cup (B \times \{\{\emptyset\}\}))$
44		opelxp	$⊢ ⟨x, \{\emptyset\}⟩ \in (C \times \{\emptyset\}) \leftrightarrow (x \in C \land \{\emptyset\} \in \{\emptyset\})$
45	33	bianfi	$⊢ \{\emptyset\} \in \{\emptyset\} \leftrightarrow (x \in C \land \{\emptyset\} \in \{\emptyset\})$
46	44 45	bitr4i	$⊢ ⟨x, \{\emptyset\}⟩ \in (C \times \{\emptyset\}) \leftrightarrow \{\emptyset\} \in \{\emptyset\}$
47		opelxp	$⊢ ⟨x, \{\emptyset\}⟩ \in (D \times \{\{\emptyset\}\}) \leftrightarrow (x \in D \land \{\emptyset\} \in \{\{\emptyset\}\})$
48	36 47	mpbiran2	$⊢ ⟨x, \{\emptyset\}⟩ \in (D \times \{\{\emptyset\}\}) \leftrightarrow x \in D$
49	46 48	orbi12i	$⊢ (⟨x, \{\emptyset\}⟩ \in (C \times \{\emptyset\}) \lor ⟨x, \{\emptyset\}⟩ \in (D \times \{\{\emptyset\}\})) \leftrightarrow (\{\emptyset\} \in \{\emptyset\} \lor x \in D)$
50		elun	$⊢ ⟨x, \{\emptyset\}⟩ \in ((C \times \{\emptyset\}) \cup (D \times \{\{\emptyset\}\})) \leftrightarrow (⟨x, \{\emptyset\}⟩ \in (C \times \{\emptyset\}) \lor ⟨x, \{\emptyset\}⟩ \in (D \times \{\{\emptyset\}\}))$
51		biorf	$⊢ \neg \{\emptyset\} \in \{\emptyset\} \to (x \in D \leftrightarrow (\{\emptyset\} \in \{\emptyset\} \lor x \in D))$
52	33 51	ax-mp	$⊢ x \in D \leftrightarrow (\{\emptyset\} \in \{\emptyset\} \lor x \in D)$
53	49 50 52	3bitr4ri	$⊢ x \in D \leftrightarrow ⟨x, \{\emptyset\}⟩ \in ((C \times \{\emptyset\}) \cup (D \times \{\{\emptyset\}\}))$
54	27 43 53	3bitr4g	$⊢ (A \times \{\emptyset\}) \cup (B \times \{\{\emptyset\}\}) = (C \times \{\emptyset\}) \cup (D \times \{\{\emptyset\}\}) \to (x \in B \leftrightarrow x \in D)$
55	54	eqrdv	$⊢ (A \times \{\emptyset\}) \cup (B \times \{\{\emptyset\}\}) = (C \times \{\emptyset\}) \cup (D \times \{\{\emptyset\}\}) \to B = D$
56	26 55	jca	$⊢ (A \times \{\emptyset\}) \cup (B \times \{\{\emptyset\}\}) = (C \times \{\emptyset\}) \cup (D \times \{\{\emptyset\}\}) \to (A = C \land B = D)$
57		xpeq1	$⊢ A = C \to A \times \{\emptyset\} = C \times \{\emptyset\}$
58		xpeq1	$⊢ B = D \to B \times \{\{\emptyset\}\} = D \times \{\{\emptyset\}\}$
59		uneq12	$⊢ (A \times \{\emptyset\} = C \times \{\emptyset\} \land B \times \{\{\emptyset\}\} = D \times \{\{\emptyset\}\}) \to (A \times \{\emptyset\}) \cup (B \times \{\{\emptyset\}\}) = (C \times \{\emptyset\}) \cup (D \times \{\{\emptyset\}\})$
60	57 58 59	syl2an	$⊢ (A = C \land B = D) \to (A \times \{\emptyset\}) \cup (B \times \{\{\emptyset\}\}) = (C \times \{\emptyset\}) \cup (D \times \{\{\emptyset\}\})$
61	56 60	impbii	$⊢ (A \times \{\emptyset\}) \cup (B \times \{\{\emptyset\}\}) = (C \times \{\emptyset\}) \cup (D \times \{\{\emptyset\}\}) \leftrightarrow (A = C \land B = D)$

Metamath Proof Explorer

Theorem opthprc

Proof