Theorem sspr 2466

Description: The subsets of a pair.

Assertion

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

Proof of Theorem sspr

Step	Hyp	Ref	Expression
1		simpll 412	. . . . . . 7 |- (((A (_ {B, C} /\ -. (A = (/) \/ A = {B})) /\ -. A = {C}) -> A (_ {B, C})
2		prssg 2463	. . . . . . . . 9 |- ((B e. A /\ C e. A) -> ((B e. A /\ C e. A) <-> {B, C} (_ A))
3	2	ibi 590	. . . . . . . 8 |- ((B e. A /\ C e. A) -> {B, C} (_ A)
4		difsn 2455	. . . . . . . . . . . . . . . 16 |- (-. B e. A -> (A \ {B}) = A)
5	4	adantl 388	. . . . . . . . . . . . . . 15 |- ((A (_ {B, C} /\ -. B e. A) -> (A \ {B}) = A)
6		ssdif 2162	. . . . . . . . . . . . . . . . 17 |- (A (_ {B, C} -> (A \ {B}) (_ ({B, C} \ {B}))
7		difprsn 2456	. . . . . . . . . . . . . . . . . 18 |- ({B, C} \ {B}) (_ {C}
8	7	a1i 8	. . . . . . . . . . . . . . . . 17 |- (A (_ {B, C} -> ({B, C} \ {B}) (_ {C})
9	6, 8	sstrd 2064	. . . . . . . . . . . . . . . 16 |- (A (_ {B, C} -> (A \ {B}) (_ {C})
10	9	adantr 389	. . . . . . . . . . . . . . 15 |- ((A (_ {B, C} /\ -. B e. A) -> (A \ {B}) (_ {C})
11	5, 10	eqsstr3d 2086	. . . . . . . . . . . . . 14 |- ((A (_ {B, C} /\ -. B e. A) -> A (_ {C})
12	11	ex 373	. . . . . . . . . . . . 13 |- (A (_ {B, C} -> (-. B e. A -> A (_ {C}))
13		sssn 2464	. . . . . . . . . . . . 13 |- (A (_ {C} <-> (A = (/) \/ A = {C}))
14	12, 13	syl6ib 212	. . . . . . . . . . . 12 |- (A (_ {B, C} -> (-. B e. A -> (A = (/) \/ A = {C})))
15	14	con1d 93	. . . . . . . . . . 11 |- (A (_ {B, C} -> (-. (A = (/) \/ A = {C}) -> B e. A))
16	15	imp 350	. . . . . . . . . 10 |- ((A (_ {B, C} /\ -. (A = (/) \/ A = {C})) -> B e. A)
17		pm2.45 277	. . . . . . . . . . . 12 |- (-. (A = (/) \/ A = {B}) -> -. A = (/))
18	17	anim1i 334	. . . . . . . . . . 11 |- ((-. (A = (/) \/ A = {B}) /\ -. A = {C}) -> (-. A = (/) /\ -. A = {C}))
19		ioran 306	. . . . . . . . . . 11 |- (-. (A = (/) \/ A = {C}) <-> (-. A = (/) /\ -. A = {C}))
20	18, 19	sylibr 200	. . . . . . . . . 10 |- ((-. (A = (/) \/ A = {B}) /\ -. A = {C}) -> -. (A = (/) \/ A = {C}))
21	16, 20	sylan2 451	. . . . . . . . 9 |- ((A (_ {B, C} /\ (-. (A = (/) \/ A = {B}) /\ -. A = {C})) -> B e. A)
22	21	anassrs 441	. . . . . . . 8 |- (((A (_ {B, C} /\ -. (A = (/) \/ A = {B})) /\ -. A = {C}) -> B e. A)
23		difsn 2455	. . . . . . . . . . . . . . 15 |- (-. C e. A -> (A \ {C}) = A)
24	23	adantl 388	. . . . . . . . . . . . . 14 |- ((A (_ {B, C} /\ -. C e. A) -> (A \ {C}) = A)
25		prcom 2437	. . . . . . . . . . . . . . . . . 18 |- {B, C} = {C, B}
26	25	sseq2i 2076	. . . . . . . . . . . . . . . . 17 |- (A (_ {B, C} <-> A (_ {C, B})
27		ssdif 2162	. . . . . . . . . . . . . . . . 17 |- (A (_ {C, B} -> (A \ {C}) (_ ({C, B} \ {C}))
28	26, 27	sylbi 199	. . . . . . . . . . . . . . . 16 |- (A (_ {B, C} -> (A \ {C}) (_ ({C, B} \ {C}))
29	28	adantr 389	. . . . . . . . . . . . . . 15 |- ((A (_ {B, C} /\ -. C e. A) -> (A \ {C}) (_ ({C, B} \ {C}))
30		difprsn 2456	. . . . . . . . . . . . . . . 16 |- ({C, B} \ {C}) (_ {B}
31	30	a1i 8	. . . . . . . . . . . . . . 15 |- ((A (_ {B, C} /\ -. C e. A) -> ({C, B} \ {C}) (_ {B})
32	29, 31	sstrd 2064	. . . . . . . . . . . . . 14 |- ((A (_ {B, C} /\ -. C e. A) -> (A \ {C}) (_ {B})
33	24, 32	eqsstr3d 2086	. . . . . . . . . . . . 13 |- ((A (_ {B, C} /\ -. C e. A) -> A (_ {B})
34	33	ex 373	. . . . . . . . . . . 12 |- (A (_ {B, C} -> (-. C e. A -> A (_ {B}))
35		sssn 2464	. . . . . . . . . . . 12 |- (A (_ {B} <-> (A = (/) \/ A = {B}))
36	34, 35	syl6ib 212	. . . . . . . . . . 11 |- (A (_ {B, C} -> (-. C e. A -> (A = (/) \/ A = {B})))
37	36	con1d 93	. . . . . . . . . 10 |- (A (_ {B, C} -> (-. (A = (/) \/ A = {B}) -> C e. A))
38	37	imp 350	. . . . . . . . 9 |- ((A (_ {B, C} /\ -. (A = (/) \/ A = {B})) -> C e. A)
39	38	adantr 389	. . . . . . . 8 |- (((A (_ {B, C} /\ -. (A = (/) \/ A = {B})) /\ -. A = {C}) -> C e. A)
40	3, 22, 39	sylanc 471	. . . . . . 7 |- (((A (_ {B, C} /\ -. (A = (/) \/ A = {B})) /\ -. A = {C}) -> {B, C} (_ A)
41	1, 40	eqssd 2069	. . . . . 6 |- (((A (_ {B, C} /\ -. (A = (/) \/ A = {B})) /\ -. A = {C}) -> A = {B, C})
42	41	ex 373	. . . . 5 |- ((A (_ {B, C} /\ -. (A = (/) \/ A = {B})) -> (-. A = {C} -> A = {B, C}))
43	42	orrd 233	. . . 4 |- ((A (_ {B, C} /\ -. (A = (/) \/ A = {B})) -> (A = {C} \/ A = {B, C}))
44	43	ex 373	. . 3 |- (A (_ {B, C} -> (-. (A = (/) \/ A = {B}) -> (A = {C} \/ A = {B, C})))
45	44	orrd 233	. 2 |- (A (_ {B, C} -> ((A = (/) \/ A = {B}) \/ (A = {C} \/ A = {B, C})))
46		0ss 2291	. . . . 5 |- (/) (_ {B, C}
47		sseq1 2072	. . . . 5 |- (A = (/) -> (A (_ {B, C} <-> (/) (_ {B, C}))
48	46, 47	mpbiri 194	. . . 4 |- (A = (/) -> A (_ {B, C})
49		snsspr 2461	. . . . 5 |- {B} (_ {B, C}
50		sseq1 2072	. . . . 5 |- (A = {B} -> (A (_ {B, C} <-> {B} (_ {B, C}))
51	49, 50	mpbiri 194	. . . 4 |- (A = {B} -> A (_ {B, C})
52	48, 51	jaoi 341	. . 3 |- ((A = (/) \/ A = {B}) -> A (_ {B, C})
53		snsspr 2461	. . . . . 6 |- {C} (_ {C, B}
54		sseq1 2072	. . . . . 6 |- (A = {C} -> (A (_ {C, B} <-> {C} (_ {C, B}))
55	53, 54	mpbiri 194	. . . . 5 |- (A = {C} -> A (_ {C, B})
56		prcom 2437	. . . . 5 |- {C, B} = {B, C}
57	55, 56	syl6ss 2097	. . . 4 |- (A = {C} -> A (_ {B, C})
58		eqimss 2099	. . . 4 |- (A = {B, C} -> A (_ {B, C})
59	57, 58	jaoi 341	. . 3 |- ((A = {C} \/ A = {B, C}) -> A (_ {B, C})
60	52, 59	jaoi 341	. 2 |- (((A = (/) \/ A = {B}) \/ (A = {C} \/ A = {B, C})) -> A (_ {B, C})
61	45, 60	impbi 157	1 |- (A (_ {B, C} <-> ((A = (/) \/ A = {B}) \/ (A = {C} \/ A = {B, C})))

Syntax hints:  -. wn 2   <-> wb 146   \/ wo 222   /\ wa 223   = wceq 953   e. wcel 955   \ cdif 2034   (_ wss 2037  (/)c0 2270  {csn 2399  {cpr 2400

This theorem is referenced by:  indistop 7590

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-sn 2402  df-pr 2403

Copyright terms: Public domain