Theorem 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 \mathrm{V}$$
	snopeqop.b	$$⊢B\in \mathrm{V}$$
	propeqop.c	$$⊢C\in \mathrm{V}$$
	propeqop.d	$$⊢D\in \mathrm{V}$$
	propeqop.e	$$⊢E\in \mathrm{V}$$
	propeqop.f	$$⊢F\in \mathrm{V}$$
Assertion	propssopi	$$⊢\left\{⟨A,B⟩,⟨C,D⟩\right\}\subseteq ⟨E,F⟩\to A=C$$

Proof

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