propssopi

Description: If a pair of ordered pairs is a subset of an ordered pair, their first components are equal. (Contributed by AV, 20-Sep-2020) (Proof shortened by AV, 16-Jun-2022) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	snopeqop.a	$⊢ A \in V$
	snopeqop.b	$⊢ B \in V$
	propeqop.c	$⊢ C \in V$
	propeqop.d	$⊢ D \in V$
	propeqop.e	$⊢ E \in V$
	propeqop.f	$⊢ F \in V$
Assertion	propssopi	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} \subseteq ⟨E, F⟩ \to A = C$

Proof

Step	Hyp	Ref	Expression
1		snopeqop.a	$⊢ A \in V$
2		snopeqop.b	$⊢ B \in V$
3		propeqop.c	$⊢ C \in V$
4		propeqop.d	$⊢ D \in V$
5		propeqop.e	$⊢ E \in V$
6		propeqop.f	$⊢ F \in V$
7	5 6	dfop	$⊢ ⟨E, F⟩ = \{\{E\}, \{E, F\}\}$
8	7	sseq2i	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} \subseteq ⟨E, F⟩ \leftrightarrow \{⟨A, B⟩, ⟨C, D⟩\} \subseteq \{\{E\}, \{E, F\}\}$
9		sspr	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} \subseteq \{\{E\}, \{E, F\}\} \leftrightarrow ((\{⟨A, B⟩, ⟨C, D⟩\} = \emptyset \lor \{⟨A, B⟩, ⟨C, D⟩\} = \{\{E\}\}) \lor (\{⟨A, B⟩, ⟨C, D⟩\} = \{\{E, F\}\} \lor \{⟨A, B⟩, ⟨C, D⟩\} = \{\{E\}, \{E, F\}\}))$
10		opex	$⊢ ⟨A, B⟩ \in V$
11	10	prnz	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} \neq \emptyset$
12		eqneqall	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} = \emptyset \to (\{⟨A, B⟩, ⟨C, D⟩\} \neq \emptyset \to A = C)$
13	11 12	mpi	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} = \emptyset \to A = C$
14		opex	$⊢ ⟨C, D⟩ \in V$
15	10 14	preqsn	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} = \{\{E\}\} \leftrightarrow (⟨A, B⟩ = ⟨C, D⟩ \land ⟨C, D⟩ = \{E\})$
16	1 2	opth	$⊢ ⟨A, B⟩ = ⟨C, D⟩ \leftrightarrow (A = C \land B = D)$
17		simpl	$⊢ (A = C \land B = D) \to A = C$
18	16 17	sylbi	$⊢ ⟨A, B⟩ = ⟨C, D⟩ \to A = C$
19	18	adantr	$⊢ (⟨A, B⟩ = ⟨C, D⟩ \land ⟨C, D⟩ = \{E\}) \to A = C$
20	15 19	sylbi	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} = \{\{E\}\} \to A = C$
21	13 20	jaoi	$⊢ (\{⟨A, B⟩, ⟨C, D⟩\} = \emptyset \lor \{⟨A, B⟩, ⟨C, D⟩\} = \{\{E\}\}) \to A = C$
22	10 14	preqsn	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} = \{\{E, F\}\} \leftrightarrow (⟨A, B⟩ = ⟨C, D⟩ \land ⟨C, D⟩ = \{E, F\})$
23	17	a1d	$⊢ (A = C \land B = D) \to (⟨C, D⟩ = \{E, F\} \to A = C)$
24	16 23	sylbi	$⊢ ⟨A, B⟩ = ⟨C, D⟩ \to (⟨C, D⟩ = \{E, F\} \to A = C)$
25	24	imp	$⊢ (⟨A, B⟩ = ⟨C, D⟩ \land ⟨C, D⟩ = \{E, F\}) \to A = C$
26	22 25	sylbi	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} = \{\{E, F\}\} \to A = C$
27	7	eqcomi	$⊢ \{\{E\}, \{E, F\}\} = ⟨E, F⟩$
28	27	eqeq2i	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} = \{\{E\}, \{E, F\}\} \leftrightarrow \{⟨A, B⟩, ⟨C, D⟩\} = ⟨E, F⟩$
29	1 2 3 4 5 6	propeqop	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} = ⟨E, F⟩ \leftrightarrow ((A = C \land E = \{A\}) \land ((A = B \land F = \{A, D\}) \lor (A = D \land F = \{A, B\})))$
30	28 29	bitri	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} = \{\{E\}, \{E, F\}\} \leftrightarrow ((A = C \land E = \{A\}) \land ((A = B \land F = \{A, D\}) \lor (A = D \land F = \{A, B\})))$
31		simpll	$⊢ ((A = C \land E = \{A\}) \land ((A = B \land F = \{A, D\}) \lor (A = D \land F = \{A, B\}))) \to A = C$
32	30 31	sylbi	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} = \{\{E\}, \{E, F\}\} \to A = C$
33	26 32	jaoi	$⊢ (\{⟨A, B⟩, ⟨C, D⟩\} = \{\{E, F\}\} \lor \{⟨A, B⟩, ⟨C, D⟩\} = \{\{E\}, \{E, F\}\}) \to A = C$
34	21 33	jaoi	$⊢ ((\{⟨A, B⟩, ⟨C, D⟩\} = \emptyset \lor \{⟨A, B⟩, ⟨C, D⟩\} = \{\{E\}\}) \lor (\{⟨A, B⟩, ⟨C, D⟩\} = \{\{E, F\}\} \lor \{⟨A, B⟩, ⟨C, D⟩\} = \{\{E\}, \{E, F\}\})) \to A = C$
35	9 34	sylbi	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} \subseteq \{\{E\}, \{E, F\}\} \to A = C$
36	8 35	sylbi	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} \subseteq ⟨E, F⟩ \to A = C$

Metamath Proof Explorer

Theorem propssopi

Proof