Theorem sspr 3144

Description: The subsets of a pair.

Assertion

Ref	Expression
sspr	|- (A C_ {B, C} <-> ((A = (/) \/ A = {B}) \/ (A = {C} \/ A = {B, C})))

Proof of Theorem sspr

Step	Hyp	Ref	Expression
1		simpll 448	. . . . . . 7 |- (((A C_ {B, C} /\ -. (A = (/) \/ A = {B})) /\ -. A = {C}) -> A C_ {B, C})
2		difsn 3125	. . . . . . . . . . . . . . . 16 |- (-. B e. A -> (A \ {B}) = A)
3	2	adantl 424	. . . . . . . . . . . . . . 15 |- ((A C_ {B, C} /\ -. B e. A) -> (A \ {B}) = A)
4		ssdif 2740	. . . . . . . . . . . . . . . . 17 |- (A C_ {B, C} -> (A \ {B}) C_ ({B, C} \ {B}))
5		difprsn 3127	. . . . . . . . . . . . . . . . . 18 |- ({B, C} \ {B}) C_ {C}
6	5	a1i 8	. . . . . . . . . . . . . . . . 17 |- (A C_ {B, C} -> ({B, C} \ {B}) C_ {C})
7	4, 6	sstrd 2627	. . . . . . . . . . . . . . . 16 |- (A C_ {B, C} -> (A \ {B}) C_ {C})
8	7	adantr 425	. . . . . . . . . . . . . . 15 |- ((A C_ {B, C} /\ -. B e. A) -> (A \ {B}) C_ {C})
9	3, 8	eqsstr3d 2652	. . . . . . . . . . . . . 14 |- ((A C_ {B, C} /\ -. B e. A) -> A C_ {C})
10	9	ex 402	. . . . . . . . . . . . 13 |- (A C_ {B, C} -> (-. B e. A -> A C_ {C}))
11		sssn 3142	. . . . . . . . . . . . 13 |- (A C_ {C} <-> (A = (/) \/ A = {C}))
12	10, 11	syl6ib 229	. . . . . . . . . . . 12 |- (A C_ {B, C} -> (-. B e. A -> (A = (/) \/ A = {C})))
13	12	con1d 109	. . . . . . . . . . 11 |- (A C_ {B, C} -> (-. (A = (/) \/ A = {C}) -> B e. A))
14	13	imp 377	. . . . . . . . . 10 |- ((A C_ {B, C} /\ -. (A = (/) \/ A = {C})) -> B e. A)
15		pm2.45 299	. . . . . . . . . . . 12 |- (-. (A = (/) \/ A = {B}) -> -. A = (/))
16	15	anim1i 361	. . . . . . . . . . 11 |- ((-. (A = (/) \/ A = {B}) /\ -. A = {C}) -> (-. A = (/) /\ -. A = {C}))
17		ioran 331	. . . . . . . . . . 11 |- (-. (A = (/) \/ A = {C}) <-> (-. A = (/) /\ -. A = {C}))
18	16, 17	sylibr 217	. . . . . . . . . 10 |- ((-. (A = (/) \/ A = {B}) /\ -. A = {C}) -> -. (A = (/) \/ A = {C}))
19	14, 18	sylan2 500	. . . . . . . . 9 |- ((A C_ {B, C} /\ (-. (A = (/) \/ A = {B}) /\ -. A = {C})) -> B e. A)
20	19	anassrs 489	. . . . . . . 8 |- (((A C_ {B, C} /\ -. (A = (/) \/ A = {B})) /\ -. A = {C}) -> B e. A)
21		difsn 3125	. . . . . . . . . . . . . . 15 |- (-. C e. A -> (A \ {C}) = A)
22	21	adantl 424	. . . . . . . . . . . . . 14 |- ((A C_ {B, C} /\ -. C e. A) -> (A \ {C}) = A)
23		prcom 3097	. . . . . . . . . . . . . . . . . 18 |- {B, C} = {C, B}
24	23	sseq2i 2642	. . . . . . . . . . . . . . . . 17 |- (A C_ {B, C} <-> A C_ {C, B})
25		ssdif 2740	. . . . . . . . . . . . . . . . 17 |- (A C_ {C, B} -> (A \ {C}) C_ ({C, B} \ {C}))
26	24, 25	sylbi 216	. . . . . . . . . . . . . . . 16 |- (A C_ {B, C} -> (A \ {C}) C_ ({C, B} \ {C}))
27	26	adantr 425	. . . . . . . . . . . . . . 15 |- ((A C_ {B, C} /\ -. C e. A) -> (A \ {C}) C_ ({C, B} \ {C}))
28		difprsn 3127	. . . . . . . . . . . . . . . 16 |- ({C, B} \ {C}) C_ {B}
29	28	a1i 8	. . . . . . . . . . . . . . 15 |- ((A C_ {B, C} /\ -. C e. A) -> ({C, B} \ {C}) C_ {B})
30	27, 29	sstrd 2627	. . . . . . . . . . . . . 14 |- ((A C_ {B, C} /\ -. C e. A) -> (A \ {C}) C_ {B})
31	22, 30	eqsstr3d 2652	. . . . . . . . . . . . 13 |- ((A C_ {B, C} /\ -. C e. A) -> A C_ {B})
32	31	ex 402	. . . . . . . . . . . 12 |- (A C_ {B, C} -> (-. C e. A -> A C_ {B}))
33		sssn 3142	. . . . . . . . . . . 12 |- (A C_ {B} <-> (A = (/) \/ A = {B}))
34	32, 33	syl6ib 229	. . . . . . . . . . 11 |- (A C_ {B, C} -> (-. C e. A -> (A = (/) \/ A = {B})))
35	34	con1d 109	. . . . . . . . . 10 |- (A C_ {B, C} -> (-. (A = (/) \/ A = {B}) -> C e. A))
36	35	imp 377	. . . . . . . . 9 |- ((A C_ {B, C} /\ -. (A = (/) \/ A = {B})) -> C e. A)
37	36	adantr 425	. . . . . . . 8 |- (((A C_ {B, C} /\ -. (A = (/) \/ A = {B})) /\ -. A = {C}) -> C e. A)
38		prssg 3140	. . . . . . . . 9 |- ((B e. A /\ C e. A) -> ((B e. A /\ C e. A) <-> {B, C} C_ A))
39	38	ibi 652	. . . . . . . 8 |- ((B e. A /\ C e. A) -> {B, C} C_ A)
40	20, 37, 39	syl11anc 524	. . . . . . 7 |- (((A C_ {B, C} /\ -. (A = (/) \/ A = {B})) /\ -. A = {C}) -> {B, C} C_ A)
41	1, 40	eqssd 2633	. . . . . 6 |- (((A C_ {B, C} /\ -. (A = (/) \/ A = {B})) /\ -. A = {C}) -> A = {B, C})
42	41	ex 402	. . . . 5 |- ((A C_ {B, C} /\ -. (A = (/) \/ A = {B})) -> (-. A = {C} -> A = {B, C}))
43	42	orrd 250	. . . 4 |- ((A C_ {B, C} /\ -. (A = (/) \/ A = {B})) -> (A = {C} \/ A = {B, C}))
44	43	ex 402	. . 3 |- (A C_ {B, C} -> (-. (A = (/) \/ A = {B}) -> (A = {C} \/ A = {B, C})))
45	44	orrd 250	. 2 |- (A C_ {B, C} -> ((A = (/) \/ A = {B}) \/ (A = {C} \/ A = {B, C})))
46		0ss 2900	. . . . 5 |- (/) C_ {B, C}
47		sseq1 2637	. . . . 5 |- (A = (/) -> (A C_ {B, C} <-> (/) C_ {B, C}))
48	46, 47	mpbiri 211	. . . 4 |- (A = (/) -> A C_ {B, C})
49		snsspr1 3135	. . . . 5 |- {B} C_ {B, C}
50		sseq1 2637	. . . . 5 |- (A = {B} -> (A C_ {B, C} <-> {B} C_ {B, C}))
51	49, 50	mpbiri 211	. . . 4 |- (A = {B} -> A C_ {B, C})
52	48, 51	jaoi 368	. . 3 |- ((A = (/) \/ A = {B}) -> A C_ {B, C})
53		snsspr2 3137	. . . . 5 |- {C} C_ {B, C}
54		sseq1 2637	. . . . 5 |- (A = {C} -> (A C_ {B, C} <-> {C} C_ {B, C}))
55	53, 54	mpbiri 211	. . . 4 |- (A = {C} -> A C_ {B, C})
56		eqimss 2665	. . . 4 |- (A = {B, C} -> A C_ {B, C})
57	55, 56	jaoi 368	. . 3 |- ((A = {C} \/ A = {B, C}) -> A C_ {B, C})
58	52, 57	jaoi 368	. 2 |- (((A = (/) \/ A = {B}) \/ (A = {C} \/ A = {B, C})) -> A C_ {B, C})
59	45, 58	impbii 174	1 |- (A C_ {B, C} <-> ((A = (/) \/ A = {B}) \/ (A = {C} \/ A = {B, C})))

Syntax hints:  -. wn 2   <-> wb 163   \/ wo 239   /\ wa 240   = wceq 1298   e. wcel 1300   \ cdif 2590   C_ wss 2593  (/)c0 2875  {csn 3044  {cpr 3045

This theorem is referenced by:  pwpr 3174  indistop 8918

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-sn 3049  df-pr 3050

Copyright terms: Public domain