Theorem ssrnres 4706

Description: Subset of the range of a restriction. (Contributed by NM, 16-Jan-2006.)

Assertion

Ref	Expression
ssrnres	|- (B C_ ran ( C |` A) <-> ran ( C i^i (A X. B)) = B)

Proof of Theorem ssrnres

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss2 3152	. . . . 5 |- ( C i^i (A X. B)) C_ (A X. B)
2		rnss 4507	. . . . 5 |- (( C i^i (A X. B)) C_ (A X. B) -> ran ( C i^i (A X. B)) C_ ran (A X. B))
3	1, 2	ax-mp 7	. . . 4 |- ran ( C i^i (A X. B)) C_ ran (A X. B)
4		rnxpss 4697	. . . 4 |- ran (A X. B) C_ B
5	3, 4	sstri 2948	. . 3 |- ran ( C i^i (A X. B)) C_ B
6		eqss 2954	. . 3 |- ( ran ( C i^i (A X. B)) = B <-> ( ran ( C i^i (A X. B)) C_ B /\ B C_ ran ( C i^i (A X. B))))
7	5, 6	mpbiran 846	. 2 |- ( ran ( C i^i (A X. B)) = B <-> B C_ ran ( C i^i (A X. B)))
8		ssid 2958	. . . . . . . 8 |- A C_ A
9		ssv 2959	. . . . . . . 8 |- B C_ _V
10		xpss12 4388	. . . . . . . 8 |- ((A C_ A /\ B C_ _V) -> (A X. B) C_ (A X. _V))
11	8, 9, 10	mp2an 402	. . . . . . 7 |- (A X. B) C_ (A X. _V)
12		sslin 3157	. . . . . . 7 |- ((A X. B) C_ (A X. _V) -> ( C i^i (A X. B)) C_ ( C i^i (A X. _V)))
13	11, 12	ax-mp 7	. . . . . 6 |- ( C i^i (A X. B)) C_ ( C i^i (A X. _V))
14		df-res 4300	. . . . . 6 |- ( C |` A) = ( C i^i (A X. _V))
15	13, 14	sseqtr4i 2972	. . . . 5 |- ( C i^i (A X. B)) C_ ( C |` A)
16		rnss 4507	. . . . 5 |- (( C i^i (A X. B)) C_ ( C |` A) -> ran ( C i^i (A X. B)) C_ ran ( C |` A))
17	15, 16	ax-mp 7	. . . 4 |- ran ( C i^i (A X. B)) C_ ran ( C |` A)
18		sstr 2947	. . . 4 |- ((B C_ ran ( C i^i (A X. B)) /\ ran ( C i^i (A X. B)) C_ ran ( C |` A)) -> B C_ ran ( C |` A))
19	17, 18	mpan2 401	. . 3 |- (B C_ ran ( C i^i (A X. B)) -> B C_ ran ( C |` A))
20		ssel 2933	. . . . . . 7 |- (B C_ ran ( C |` A) -> (y e. B -> y e. ran ( C |` A)))
21		vex 2554	. . . . . . . 8 |- y e. _V
22	21	elrn2 4519	. . . . . . 7 |- (y e. ran ( C |` A) <-> E.x <.x , y >. e. ( C |` A))
23	20, 22	syl6ib 150	. . . . . 6 |- (B C_ ran ( C |` A) -> (y e. B -> E.x <.x , y >. e. ( C |` A)))
24	23	ancrd 309	. . . . 5 |- (B C_ ran ( C |` A) -> (y e. B -> (E.x <.x , y >. e. ( C |` A) /\ y e. B)))
25	21	elrn2 4519	. . . . . 6 |- (y e. ran ( C i^i (A X. B)) <-> E.x <.x , y >. e. ( C i^i (A X. B)))
26		elin 3120	. . . . . . . 8 |- ( <.x , y >. e. ( C i^i (A X. B)) <-> ( <.x , y >. e. C /\ <.x , y >. e. (A X. B)))
27		opelxp 4317	. . . . . . . . 9 |- ( <.x , y >. e. (A X. B) <-> (x e. A /\ y e. B))
28	27	anbi2i 430	. . . . . . . 8 |- (( <.x , y >. e. C /\ <.x , y >. e. (A X. B)) <-> ( <.x , y >. e. C /\ (x e. A /\ y e. B)))
29	21	opelres 4560	. . . . . . . . . 10 |- ( <.x , y >. e. ( C |` A) <-> ( <.x , y >. e. C /\ x e. A))
30	29	anbi1i 431	. . . . . . . . 9 |- (( <.x , y >. e. ( C |` A) /\ y e. B) <-> (( <.x , y >. e. C /\ x e. A) /\ y e. B))
31		anass 381	. . . . . . . . 9 |- ((( <.x , y >. e. C /\ x e. A) /\ y e. B) <-> ( <.x , y >. e. C /\ (x e. A /\ y e. B)))
32	30, 31	bitr2i 174	. . . . . . . 8 |- (( <.x , y >. e. C /\ (x e. A /\ y e. B)) <-> ( <.x , y >. e. ( C |` A) /\ y e. B))
33	26, 28, 32	3bitri 195	. . . . . . 7 |- ( <.x , y >. e. ( C i^i (A X. B)) <-> ( <.x , y >. e. ( C |` A) /\ y e. B))
34	33	exbii 1493	. . . . . 6 |- (E.x <.x , y >. e. ( C i^i (A X. B)) <-> E.x( <.x , y >. e. ( C |` A) /\ y e. B))
35		19.41v 1779	. . . . . 6 |- (E.x( <.x , y >. e. ( C |` A) /\ y e. B) <-> (E.x <.x , y >. e. ( C |` A) /\ y e. B))
36	25, 34, 35	3bitri 195	. . . . 5 |- (y e. ran ( C i^i (A X. B)) <-> (E.x <.x , y >. e. ( C |` A) /\ y e. B))
37	24, 36	syl6ibr 151	. . . 4 |- (B C_ ran ( C |` A) -> (y e. B -> y e. ran ( C i^i (A X. B))))
38	37	ssrdv 2945	. . 3 |- (B C_ ran ( C |` A) -> B C_ ran ( C i^i (A X. B)))
39	19, 38	impbii 117	. 2 |- (B C_ ran ( C i^i (A X. B)) <-> B C_ ran ( C |` A))
40	7, 39	bitr2i 174	1 |- (B C_ ran ( C |` A) <-> ran ( C i^i (A X. B)) = B)

Syntax hints:   /\ wa 97   <-> wb 98   = wceq 1242  E.wex 1378   e. wcel 1390   _Vcvv 2551   i^i cin 2910   C_ wss 2911   <.cop 3370   X. cxp 4286   ran crn 4289   |` cres 4290

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-opab 3810  df-xp 4294  df-rel 4295  df-cnv 4296  df-dm 4298  df-rn 4299  df-res 4300

This theorem is referenced by:  rninxp  4707