Theorem propssopi 4971

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.)

Hypotheses

Ref	Expression
snopeqop.a	|- A e. _V
snopeqop.b	|- B e. _V
snopeqop.c	|- C e. _V
snopeqop.d	|- D e. _V
propeqop.e	|- E e. _V
propeqop.f	|- F e. _V

Assertion

Ref	Expression
propssopi	|- ( { <. A , B >. , <. C , D >. } C_ <. E , F >. -> A = C )

Proof of Theorem propssopi

Step	Hyp	Ref	Expression
1		propeqop.e	. . . 4 |- E e. _V
2		propeqop.f	. . . 4 |- F e. _V
3	1, 2	dfop 4401	. . 3 |- <. E , F >. = { { E } , { E , F } }
4	3	sseq2i 3630	. 2 |- ( { <. A , B >. , <. C , D >. } C_ <. E , F >. <-> { <. A , B >. , <. C , D >. } C_ { { E } , { E , F } } )
5		sspr 4366	. . 3 |- ( { <. A , B >. , <. C , D >. } C_ { { E } , { E , F } } <-> ( ( { <. A , B >. , <. C , D >. } = (/) \/ { <. A , B >. , <. C , D >. } = { { E } } ) \/ ( { <. A , B >. , <. C , D >. } = { { E , F } } \/ { <. A , B >. , <. C , D >. } = { { E } , { E , F } } ) ) )
6		opex 4932	. . . . . . 7 |- <. A , B >. e. _V
7	6	prnz 4310	. . . . . 6 |- { <. A , B >. , <. C , D >. } =/= (/)
8		eqneqall 2805	. . . . . 6 |- ( { <. A , B >. , <. C , D >. } = (/) -> ( { <. A , B >. , <. C , D >. } =/= (/) -> A = C ) )
9	7, 8	mpi 20	. . . . 5 |- ( { <. A , B >. , <. C , D >. } = (/) -> A = C )
10		opex 4932	. . . . . . 7 |- <. C , D >. e. _V
11		snex 4908	. . . . . . 7 |- { E } e. _V
12	6, 10, 11	preqsn 4393	. . . . . 6 |- ( { <. A , B >. , <. C , D >. } = { { E } } <-> ( <. A , B >. = <. C , D >. /\ <. C , D >. = { E } ) )
13		snopeqop.a	. . . . . . . . 9 |- A e. _V
14		snopeqop.b	. . . . . . . . 9 |- B e. _V
15	13, 14	opth 4945	. . . . . . . 8 |- ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) )
16		simpl 473	. . . . . . . 8 |- ( ( A = C /\ B = D ) -> A = C )
17	15, 16	sylbi 207	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> A = C )
18	17	adantr 481	. . . . . 6 |- ( ( <. A , B >. = <. C , D >. /\ <. C , D >. = { E } ) -> A = C )
19	12, 18	sylbi 207	. . . . 5 |- ( { <. A , B >. , <. C , D >. } = { { E } } -> A = C )
20	9, 19	jaoi 394	. . . 4 |- ( ( { <. A , B >. , <. C , D >. } = (/) \/ { <. A , B >. , <. C , D >. } = { { E } } ) -> A = C )
21		prex 4909	. . . . . . 7 |- { E , F } e. _V
22	6, 10, 21	preqsn 4393	. . . . . 6 |- ( { <. A , B >. , <. C , D >. } = { { E , F } } <-> ( <. A , B >. = <. C , D >. /\ <. C , D >. = { E , F } ) )
23	16	a1d 25	. . . . . . . 8 |- ( ( A = C /\ B = D ) -> ( <. C , D >. = { E , F } -> A = C ) )
24	15, 23	sylbi 207	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> ( <. C , D >. = { E , F } -> A = C ) )
25	24	imp 445	. . . . . 6 |- ( ( <. A , B >. = <. C , D >. /\ <. C , D >. = { E , F } ) -> A = C )
26	22, 25	sylbi 207	. . . . 5 |- ( { <. A , B >. , <. C , D >. } = { { E , F } } -> A = C )
27	3	eqcomi 2631	. . . . . . . 8 |- { { E } , { E , F } } = <. E , F >.
28	27	eqeq2i 2634	. . . . . . 7 |- ( { <. A , B >. , <. C , D >. } = { { E } , { E , F } } <-> { <. A , B >. , <. C , D >. } = <. E , F >. )
29		snopeqop.c	. . . . . . . 8 |- C e. _V
30		snopeqop.d	. . . . . . . 8 |- D e. _V
31	13, 14, 29, 30, 1, 2	propeqop 4970	. . . . . . 7 |- ( { <. A , B >. , <. C , D >. } = <. E , F >. <-> ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) )
32	28, 31	bitri 264	. . . . . 6 |- ( { <. A , B >. , <. C , D >. } = { { E } , { E , F } } <-> ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) )
33		simpll 790	. . . . . 6 |- ( ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) -> A = C )
34	32, 33	sylbi 207	. . . . 5 |- ( { <. A , B >. , <. C , D >. } = { { E } , { E , F } } -> A = C )
35	26, 34	jaoi 394	. . . 4 |- ( ( { <. A , B >. , <. C , D >. } = { { E , F } } \/ { <. A , B >. , <. C , D >. } = { { E } , { E , F } } ) -> A = C )
36	20, 35	jaoi 394	. . 3 |- ( ( ( { <. A , B >. , <. C , D >. } = (/) \/ { <. A , B >. , <. C , D >. } = { { E } } ) \/ ( { <. A , B >. , <. C , D >. } = { { E , F } } \/ { <. A , B >. , <. C , D >. } = { { E } , { E , F } } ) ) -> A = C )
37	5, 36	sylbi 207	. 2 |- ( { <. A , B >. , <. C , D >. } C_ { { E } , { E , F } } -> A = C )
38	4, 37	sylbi 207	1 |- ( { <. A , B >. , <. C , D >. } C_ <. E , F >. -> A = C )

Syntax hints:   -> wi 4   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   _Vcvv 3200   C_ wss 3574   (/)c0 3915   {csn 4177   {cpr 4179   <.cop 4183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184

This theorem is referenced by:  iunopeqop  4981